🐱 Path Induction (J eliminator) — an intuitive guide with cat-themed examples

🐾 Purrr, hello CGPA! nya~

I've seen a lot of people in #type-theory-help get confused by J — the path induction eliminator. It seems scary, but I promise it's just regular old induction wearing a spooky mask, like a cat in a ghost costume. 👻🐱

This tutorial is going to:

• Build intuition for what J actually says
• Show the "teleporting cat" mental model for path induction
• Derive transport, ap, and sym from J in Agda
• Explain based vs. full path induction
• Show why the computation rule matters

Let's go! nya~

§1. What is an Identity Type?

In dependent type theory, the identity type x ≡ y (sometimes written Id A x y or x =ₐ y) is the type whose inhabitants are proofs that x and y are equal. This is propositional equality — it lives inside the type theory rather than being a meta-level judgment.

The key difference from judgemental equality (x ≡ y as definitional reduction) is that propositional equality is a type you can pass around, return from functions, and reason about.

The only built-in constructor for identity types is reflexivity:

-- In Agda (standard library style):
data _≡_ {A : Set} : A → A → Set where
  refl : {x : A} → x ≡ x

refl is the proof that any term equals itself. That's the only constructor. No other constructor can be given a priori.

§2. Path Induction — The Core Idea

Here's the key insight: since refl is the only constructor for _≡_, it is an inductive type, and we can do induction on its elements, just like we do induction on ℕ.

For ℕ, induction says: to prove P n for all n, it suffices to prove P zero and the step case. For identity types, there's only one constructor (refl), so the induction principle says:

This is the J eliminator. Formally, in Agda:

J : {A : Set}
    (C : (x y : A) → x ≡ y → Set)    -- the motive / predicate
    (d : (x : A) → C x x refl)           -- proof in the refl case
    {x y : A} (p : x ≡ y)             -- the actual path
    → C x y p                             -- result
J C d refl = d _                         -- computation rule

§3. Understanding the Motive C

The scariest-looking part of J for beginners is the motive argument C : (x y : A) → x ≡ y → Set. It's a dependent predicate that can mention both endpoints of the path AND the path itself.

For each derivation with J, you need to figure out the right C. This is sometimes called "picking the motive" and it's genuinely the hard part. Let me show you by example.

§4. Deriving transport from J

transport is one of the most fundamental operations you can derive from J. Given a proof that x ≡ y and a value of type P x, transport produces a value of type P y. Conceptually, you "slide" a value along the path.

-- transport : given P x and a path x ≡ y, produce P y
transport : {A : Set}
             (P : A → Set)
             {x y : A}
             (p : x ≡ y)
             → P x
             → P y
transport P p px =
  J (λ x y _ → P x → P y)   -- motive C x y p = (P x → P y)
     (λ _ px → px)               -- refl case: identity function
     p                           -- the path
     px                          -- the value to transport

Notice the motive: C x y _ = P x → P y. When we substitute y := x and p := refl, the motive becomes P x → P x, which is just the identity — trivially provable! The computation rule gives us transport P refl px = px.

§5. Deriving ap (cong) from J

ap (also called cong in Agda's stdlib) says that functions respect propositional equality: if x ≡ y then f x ≡ f y. It's the lifting of a function to paths.

ap : {A B : Set}
     (f : A → B)
     {x y : A}
     (p : x ≡ y)
     → f x ≡ f y
ap f p =
  J (λ x y _ → f x ≡ f y)    -- motive: f x ≡ f y
     (λ _ → refl)               -- refl case: f x ≡ f x by refl
     p

The motive collapses to f x ≡ f x in the refl case, which is immediately refl. 🎉

§6. Deriving sym (path reversal) from J

sym says equality is symmetric: if x ≡ y then y ≡ x. In HoTT terms, you can reverse a path.

sym : {A : Set} {x y : A}
      → x ≡ y
      → y ≡ x
sym p =
  J (λ x y _ → y ≡ x)       -- motive: y ≡ x  (note: reversed!)
     (λ _ → refl)              -- refl case: x ≡ x by refl
     p

The motive C x y _ = y ≡ x reduces to C x x _ = x ≡ x in the refl case, which is refl. The reversal comes "for free" from the motive being backwards!

§7. Bonus: trans (path concatenation)

Path transitivity — if x ≡ y and y ≡ z then x ≡ z — is also derivable:

trans : {A : Set} {x y z : A}
        → x ≡ y
        → y ≡ z
        → x ≡ z
trans p q =
  J (λ x y _ → y ≡ z → x ≡ z)  -- motive: y ≡ z → x ≡ z
     (λ _ q → q)                  -- refl case: identity on q
     p q                          -- apply to q

When p = refl, x = y, so y ≡ z → x ≡ z collapses to x ≡ z → x ≡ z, which is just the identity function applied to q. So trans refl q = q. nya~

§8. Based Path Induction (the "j" rule)

There's a variant of J called based path induction (or the j eliminator with lowercase), where instead of universally quantifying over both endpoints, you fix one endpoint:

-- Based J: fix the left endpoint, vary only the right
J-based : {A : Set} {x : A}
          (C : (y : A) → x ≡ y → Set)   -- motive with x fixed
          (d : C x refl)                    -- proof at (x, refl)
          {y : A} (p : x ≡ y)
          → C y p
J-based C d refl = d

The full J and based J are actually inter-derivable — you can prove each from the other. Based J is sometimes easier to use because you don't need to abstract over the left endpoint.

§9. The Computation Rule (Beta for J)

A crucial property of J is its computation rule: applying J to a refl path reduces definitionally:

This matters a lot in practice. In standard Agda with data _≡_, the above holds definitionally because refl pattern matching reduces immediately. In Cubical Agda with path types, J is defined differently and the computation rule only holds propositionally (up to a path). This is one of the tradeoffs of cubical type theory.

§10. Full Agda Example — Putting It Together

module CatPaths where

open import Agda.Builtin.Equality
  -- imports _≡_ with constructor refl,
  -- and the built-in eliminator J

-- A type of cats (abstract, just for illustration)
postulate
  Cat : Set
  FoodBowl : Cat → Set
  Collar : Cat → Set
  addCollar : Cat → Cat   -- gives cat a collar (returns new cat record)

-- J eliminator (can be defined manually even if built-in exists)
J : {A : Set}
    (C : (x y : A) → x ≡ y → Set)
    → ((x : A) → C x x refl)
    → {x y : A} → x ≡ y
    → C x y
J _ d refl = d _

-- transport: slide a value along a path
transport : {A : Set} (P : A → Set)
             {x y : A} → x ≡ y → P x → P y
transport P p px = J (λ x y _ → P x → P y) (λ _ v → v) p px

-- ap: apply a function to a path
ap : {A B : Set} (f : A → B)
     {x y : A} → x ≡ y → f x ≡ f y
ap f p = J (λ x y _ → f x ≡ f y) (λ _ → refl) p

-- sym: reverse a path
sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym p = J (λ x y _ → y ≡ x) (λ _ → refl) p

-- Useful derived lemma: transport refl is identity
transport-refl : {A : Set} (P : A → Set) {x : A} (v : P x)
                  → transport P refl v ≡ v
transport-refl P v = refl   -- follows from J-β!

-- The cat example: transport a food bowl along an equality
transportBowl : {c₁ c₂ : Cat}
                 → c₁ ≡ c₂
                 → FoodBowl c₁
                 → FoodBowl c₂
transportBowl = transport FoodBowl

-- The collar example: equal cats get equal collars
equalCatsEqualCollars : {c₁ c₂ : Cat}
                          → c₁ ≡ c₂
                          → addCollar c₁ ≡ addCollar c₂
equalCatsEqualCollars = ap addCollar

§11. Common Mistakes & FAQ

Q: Why can't I just pattern match on p : x ≡ y directly without J?
A: In standard Agda, you can pattern match on refl, and Agda's dot patterns (.x) handle the unification. But you need x and y to be free variables — if they're fixed, Agda's K axiom may be invoked. J is the principled way that works in all type theories including HoTT.

Q: When should I use transport vs ap?
A: Use transport P p when you have a dependent type family P : A → Set and need to slide a value. Use ap f p when f : A → B is a function to a fixed type B. ap f p is actually transport (λ y → f x ≡ f y) p refl in disguise.

Q: Is J the same as pattern matching on refl?
A: Essentially yes, in Martin-Löf style type theory with K turned off. J is the formal elimination rule; pattern matching on refl in Agda is syntactic sugar that desugars to J (approximately). In HoTT/cubical settings they differ in their computational content.

That's it for the main tutorial! I'll be around to answer questions. If there's interest I can write a follow-up on heterogeneous paths, PathOver, and how transport interacts with function types. nya~ 🐾