/-- The **identity type** of `A`, based at `a`: an inductive family `Paths a b` with a singleconstructor `refl : Paths a a`. Read an element `p : Paths a b` as a *path* from `a` to `b`.Unlike Lean's `Eq`, which lives in `Prop`, this type lives in `Type u`, so its elements are dataand can, a priori, be distinct. -/inductive Paths {A : Type u} (a : A) : A → Type u | refl : Paths a a
/-- **Path induction** (the `J` eliminator, in Paulin-Mohring's based form). To construct anelement of `C b p` for *every* `b` and every path `p : Paths a b`, it suffices to construct onefor `b = a` and `p = refl`. Pattern matching on `refl` with the endpoint `b` free is exactlythis rule; everything below is built from `J` alone. -/def J {A : Type u} {a : A} (C : (b : A) → Paths a b → Sort v) (c : C a refl) : {b : A} → (p : Paths a b) → C b p | _, refl => c
/-- The inverse of a path, by path induction: the inverse of `refl` is `refl`. -/def inv {A : Type u} {a b : A} (p : Paths a b) : Paths b a := J (fun b _ => Paths b a) refl p
/-- Concatenation of paths, by path induction on the second path: `p ⬝ refl = p`. -/def concat {A : Type u} {a b c : A} (p : Paths a b) (q : Paths b c) : Paths a c := J (fun c _ => Paths a c) p q
/-- **Functions act on paths**: `ap f : Paths a b → Paths (f a) (f b)`. Every function isautomatically "continuous" in HoTT, because it must respect path induction. -/def ap {A : Type u} {B : Type v} (f : A → B) {a b : A} (p : Paths a b) : Paths (f a) (f b) := J (fun b _ => Paths (f a) (f b)) refl p
/-- **Transport**: a path `p : Paths a b` in the base gives a function `P a → P b` between thefibres of any type family `P`. Geometrically: lifting a path to a fibration. Logically: theindiscernibility of identicals (Leibniz's law). -/def transport {A : Type u} (P : A → Type v) {a b : A} (p : Paths a b) : P a → P b := J (fun b _ => P a → P b) id p
Paths.refl_concatdefProved here from basic factsNo axioms
refl_concatLean 4Proved here from basic factsFormally verified
/-- Left unit law, `refl ⬝ p = p`, as a **path** between paths, constructed by path induction on`p`. (The right unit law `p ⬝ refl = p` holds by definition of `concat`.) In HoTT a proof of anequation is an element of an identity type, so this is a `def`: Lean reserves `theorem` forstatements in `Prop`, and `Paths` lives in `Type`. -/def refl_concat {A : Type u} {a b : A} (p : Paths a b) : Paths (concat refl p) p := J (fun _ p => Paths (concat refl p) p) refl p
Paths.concat_invdefProved here from basic factsNo axioms
concat_invLean 4Proved here from basic factsFormally verified
/-- Inverse law: `p ⬝ p⁻¹ = refl`, as a path, by path induction on `p`. -/def concat_inv {A : Type u} {a b : A} (p : Paths a b) : Paths (concat p (inv p)) refl := J (fun _ p => Paths (concat p (inv p)) refl) refl p
Paths.concat_assocdefProved here from basic factsNo axioms
concat_assocLean 4Proved here from basic factsFormally verified
/-- Associativity: `(p ⬝ q) ⬝ r = p ⬝ (q ⬝ r)`, as a path, by path induction on `r` (both sidesthen reduce to `p ⬝ q`). In HoTT these laws are themselves paths, and they satisfy furtherlaws (the pentagon, …) up to higher paths: every type is a weak ∞-groupoid. -/def concat_assoc {A : Type u} {a b c d : A} (p : Paths a b) (q : Paths b c) (r : Paths c d) : Paths (concat (concat p q) r) (concat p (concat q r)) := J (fun _ r => Paths (concat (concat p q) r) (concat p (concat q r))) refl r
Paths.transport_concatdefProved here from basic factsNo axioms
transport_concatLean 4Proved here from basic factsFormally verified
/-- Transport is functorial: transporting along `p ⬝ q` is transporting along `p` and then along`q`. (A path, by induction on `q`.) This is what makes `transport` into a functor from thepath groupoid of `A` to types. -/def transport_concat {A : Type u} (P : A → Type v) {a b c : A} (p : Paths a b) (q : Paths b c) (x : P a) : Paths (transport P (concat p q) x) (transport P q (transport P p x)) := J (fun _ q => Paths (transport P (concat p q) x) (transport P q (transport P p x))) refl q
/-- The canonical map from paths between types to equivalences, `idtoeqv`: by path induction itsends `refl` to the identity equivalence. **Voevodsky's univalence axiom** says that this map isitself an equivalence, for all types `A` and `B` in a universe. -/def idtoeqv {A B : Type u} (p : Paths A B) : A ≃ B := J (fun B _ => A ≃ B) (Equiv.refl A) p
Paths.paths_subsingletontheoremProved here from basic factsNo axioms
paths_subsingletonLean 4Proved here from basic factsFormally verified
/-- **Uniqueness of identity proofs holds in Lean**, even for our `Type`-valued `Paths`: any twopaths `p q : Paths a b` are equal. Proof: `Paths a b` is a *retract* of Lean's `a = b` (map a pathto an equality, and back, and path induction shows the round trip is the identity), and `a = b`is a proposition with at most one proof (Lean has definitional proof irrelevance). A retract ofa type with at most one element has at most one element. In HoTT this fails: the type of pathsfrom a point to itself in the circle is `ℤ`. -/theorem paths_subsingleton {A : Type u} {a b : A} (p q : Paths a b) : p = q := by -- From paths to Lean equalities, and back. let toEq : {b : A} → Paths a b → a = b := fun p => J (fun b _ => a = b) rfl p let ofEq : {b : A} → a = b → Paths a b := fun h => h ▸ refl -- The round trip is the identity (path induction, with a motive in `Prop`). have round : ∀ {b : A} (p : Paths a b), ofEq (toEq p) = p := by intro b p exact J (fun _ p => ofEq (toEq p) = p) rfl p -- `toEq p` and `toEq q` are proofs of the same proposition, hence equal. calc p = ofEq (toEq p) := (round p).symm _ = ofEq (toEq q) := rfl _ = q := round q
Paths.univalence_failstheoremProved here from basic factsQuot.sound
univalence_failsLean 4Proved here from basic factsFormally verified
/-- **The univalence axiom is false in Lean.** The map `idtoeqv : Paths Bool Bool → (Bool ≃ Bool)`is not surjective: there are two equivalences `Bool ≃ Bool` (the identity and negation), but atmost one path `Bool = Bool` (`paths_subsingleton`). So univalence cannot be added to Lean as anaxiom without making Lean inconsistent; HoTT needs a type theory *without* uniqueness of identityproofs. -/theorem univalence_fails : ¬ Function.Surjective (idtoeqv : Paths Bool Bool → (Bool ≃ Bool)) := by intro hsurj obtain ⟨p, hp⟩ := hsurj (Equiv.refl Bool) obtain ⟨q, hq⟩ := hsurj Equiv.boolNot -- `p = q`, so the identity and negation would be the same equivalence. have hpq : p = q := paths_subsingleton p q have h : Equiv.refl Bool = Equiv.boolNot := by rw [← hp, ← hq, hpq] -- Evaluate both at `true`. have h' : true = false := congrArg (fun e : Bool ≃ Bool => e true) h exact Bool.noConfusion h'
funext_librarytheoremApplies a library theoremQuot.sound
funext_libraryLean 4Applies a library theoremFormally verified
/-- **Function extensionality**: pointwise equal functions are equal. In HoTT it is a theoremdeduced from univalence (Voevodsky); in Lean it is a theorem deduced from quotient types(`Quot.sound`). This applies core Lean's `funext`. -/theorem funext_library {α : Type u} {β : α → Type v} {f g : (x : α) → β x} (h : ∀ x, f x = g x) : f = g := funext h
bijective_iff_unique_fibrestheoremApplies a library theoremNo axioms
bijective_iff_unique_fibresLean 4Applies a library theoremFormally verified
/-- The set-level shadow of "an equivalence is a map with contractible fibres": a function isbijective exactly when every fibre `{a | f a = b}` has exactly one element. (In HoTT,"contractible" replaces "has exactly one element", and the definition then works for types withhigher paths too.) This applies Mathlib's `Function.bijective_iff_existsUnique`. -/theorem bijective_iff_unique_fibres {α : Type u} {β : Type v} (f : α → β) : Function.Bijective f ↔ ∀ b, ∃! a, f a = b := Function.bijective_iff_existsUnique f
encode_loop_powtheoremProved here from basic factspropext, Classical.choice, Quot.sound
encode_loop_powLean 4Proved here from basic factsFormally verified
/-- **The arithmetic step of encode–decode.** In the HoTT proof, the universal cover of thecircle is the family `code : S¹ → U` with `code(base) = ℤ`, and univalence makes transport along`loop` equal to the successor `succ : ℤ ≃ ℤ`. Since transport turns concatenation intocomposition (`transport_concat`), transport along `loopⁿ` is `succⁿ`, and `encode(loopⁿ)` is`succⁿ(0)`. Here we prove the last step in ordinary Lean: the `n`-th power of the successorpermutation of `ℤ` sends `k` to `k + n`, for every integer `n` (negative powers included). Inparticular `succⁿ(0) = n`. -/theorem encode_loop_pow (n k : ℤ) : ((Equiv.addRight (1 : ℤ)) ^ n) k = k + n := by induction n using Int.induction_on generalizing k with | zero => simp | succ m ih => rw [zpow_add_one, Equiv.Perm.mul_apply, ih] simp only [Equiv.coe_addRight] ring | pred m ih => rw [zpow_sub_one, Equiv.Perm.mul_apply, ih] simp only [Equiv.Perm.inv_def, Equiv.addRight_symm, Equiv.coe_addRight] ring
/-- The inverse law `p ⬝ p⁻¹ = refl`, as a path between paths, by path induction. Hint: use`J` with the motive `fun _ p => Paths (concat p (inv p)) refl`; when `p` is `refl`, both sidescompute to `refl`, so the base case is `refl`. -/def concat_inv {A : Type} {a b : A} (p : Paths a b) : Paths (concat p (inv p)) Paths.refl := sorry
Show the compiled solution
concat_invLean 4Proved here from basic factsFormally verified
/-- Inverse law: `p ⬝ p⁻¹ = refl`, as a path, by path induction on `p`. -/def concat_inv {A : Type u} {a b : A} (p : Paths a b) : Paths (concat p (inv p)) refl := J (fun _ p => Paths (concat p (inv p)) refl) refl p
/-- Univalence is false in Lean. Hint: if `idtoeqv` were surjective, pick paths `p` and `q` with`idtoeqv p = Equiv.refl Bool` and `idtoeqv q = Equiv.boolNot`; `paths_subsingleton p q` gives`p = q`; evaluate the two equivalences at `true` to get `true = false`. -/theorem univalence_fails : ¬ Function.Surjective (idtoeqv : Paths Bool Bool → (Bool ≃ Bool)) := by sorry
Show the compiled solution
univalence_failsLean 4Proved here from basic factsFormally verified
/-- **The univalence axiom is false in Lean.** The map `idtoeqv : Paths Bool Bool → (Bool ≃ Bool)`is not surjective: there are two equivalences `Bool ≃ Bool` (the identity and negation), but atmost one path `Bool = Bool` (`paths_subsingleton`). So univalence cannot be added to Lean as anaxiom without making Lean inconsistent; HoTT needs a type theory *without* uniqueness of identityproofs. -/theorem univalence_fails : ¬ Function.Surjective (idtoeqv : Paths Bool Bool → (Bool ≃ Bool)) := by intro hsurj obtain ⟨p, hp⟩ := hsurj (Equiv.refl Bool) obtain ⟨q, hq⟩ := hsurj Equiv.boolNot -- `p = q`, so the identity and negation would be the same equivalence. have hpq : p = q := paths_subsingleton p q have h : Equiv.refl Bool = Equiv.boolNot := by rw [← hp, ← hq, hpq] -- Evaluate both at `true`. have h' : true = false := congrArg (fun e : Bool ≃ Bool => e true) h exact Bool.noConfusion h'