Nyaa~ great question! The key insight is that in Cubical Agda, we trade the J-refl computation rule for a proper interval type. Path induction still works — you just prove it via transp and contractibility of singletons:

singl : {A : Type ℓ} → A → Type ℓ
singl a = Σ b (a ≡ b)

isContrSingl : (a : A) → isContr (singl a)
isContrSingl a = (a , refl) , λ p → ...

Once you have contractibility, deriving J is just transport along the contraction path. The motive P gets evaluated at the centre of contraction, which is (a, refl). Very elegant, very purrfect. (ฅ^•ﻌ•^ฅ)

Okay so I keep seeing confusion about this in the newcomer threads. Let me settle it once and for all 🐱

Short answer: no, but they're equivalent! The cubical identity type Id and the path type _≡_ are equivalent via univalence, so all results transport between them. However, path types satisfy extra definitional equalities that identity types don't — and that matters for computation! The J eliminator for the cubical Id type does compute definitionally on refl, which is the best of both worlds (≧◡≦)

I finally finished this proof, meow! The key is defining the circle as a HIT with base : S¹ and loop : base ≡ base, then using the encode-decode method:

data S¹ : Type where
  base : S¹
  loop : base ≡ base

encode : (x : S¹) → base ≡ x → helix x
decode : (x : S¹) → helix x → base ≡ x

Where helix : S¹ → Type encodes ℤ at the base, twisted by the successor function over the loop. The whole proof is like 80 lines in Cubical Agda — much shorter than the Book HoTT version! Having HITs with native path constructors makes everything so much cleaner. (✿◠‿◠)

When someone asks me if two types are equal and I pull out the full univalence axiom infrastructure just to prove Bool ≡ Bool:

(ノ°益°)ノ ⌨️  ua : A ≃ B → A ≡ B
    ≃ is just ≡ in disguise, fight me

Anyway yes, moderator hat on: please do use spoiler tags for large code blocks in this thread, I'll start pinning the formatting guide again if I have to 🐾

Hewwo everyone! I wrote a proper intro guide to HITs in Cubical Agda since the existing resources are scattered. TL;DR:

• HITs = inductive types with path constructors (constructors living in identity types)
• Cubical Agda lets you define them directly with data declarations — no axioms needed!
• You get computational univalence and proper transp reductions over HITs
• Pattern matching on HIT path constructors requires cubical boundary conditions to typecheck

Full guide in the Resources section. This is a living document; reply with corrections or questions and I'll update it. Nya~ (=^▽^=)