From d8c41ea2910d81d3c1bf6c2762663473368016ab Mon Sep 17 00:00:00 2001 From: Siegmentation Fault Date: Fri, 29 Mar 2024 14:47:15 +0700 Subject: [PATCH] update --- GroundZero/Algebra/Category.lean | 2 +- GroundZero/Algebra/EilenbergMacLane.lean | 2 +- GroundZero/Algebra/Geometry.lean | 4 +- GroundZero/Algebra/Group/Alternating.lean | 2 +- GroundZero/Algebra/Group/Finite.lean | 13 +- GroundZero/Algebra/Group/Free.lean | 2 +- GroundZero/Algebra/Group/Isomorphism.lean | 7 +- GroundZero/Algebra/Orgraph.lean | 6 +- GroundZero/Algebra/Reals.lean | 11 +- GroundZero/Exercises/Chap2.lean | 8 +- GroundZero/Exercises/Chap3.lean | 30 +- GroundZero/Exercises/Chap4.lean | 16 +- GroundZero/HITs/Circle.lean | 16 +- GroundZero/HITs/Coequalizer.lean | 2 +- GroundZero/HITs/Colimit.lean | 2 +- GroundZero/HITs/Generalized.lean | 2 +- GroundZero/HITs/Join.lean | 41 +- GroundZero/HITs/Merely.lean | 2 +- GroundZero/HITs/Pushout.lean | 2 +- GroundZero/HITs/Quotient.lean | 2 +- GroundZero/HITs/Reals.lean | 5 +- GroundZero/HITs/Setquot.lean | 4 +- GroundZero/HITs/Suspension.lean | 7 +- GroundZero/HITs/Trunc.lean | 2 +- GroundZero/HITs/Wedge.lean | 2 +- GroundZero/Meta/HottTheory.lean | 14 +- GroundZero/Meta/Notation.lean | 2 +- GroundZero/Meta/Tactic.lean | 20 +- GroundZero/Proto.lean | 6 +- GroundZero/Structures.lean | 7 +- GroundZero/Theorems/Classical.lean | 5 +- GroundZero/Theorems/Funext.lean | 2 +- GroundZero/Theorems/Nat.lean | 8 +- GroundZero/Theorems/Univalence.lean | 6 +- GroundZero/Types/Coproduct.lean | 11 +- GroundZero/Types/Ens.lean | 4 +- GroundZero/Types/Id.lean | 2 +- GroundZero/Types/Lost.lean | 3 +- GroundZero/Types/Nat.lean | 9 +- GroundZero/Types/Unit.lean | 2 +- pictures/dependency-map.svg | 974 +++++++++++----------- 41 files changed, 630 insertions(+), 637 deletions(-) diff --git a/GroundZero/Algebra/Category.lean b/GroundZero/Algebra/Category.lean index aceef2d..522fe11 100644 --- a/GroundZero/Algebra/Category.lean +++ b/GroundZero/Algebra/Category.lean @@ -35,7 +35,7 @@ namespace Precategory | Arity.left => λ (a, _), dom a | Arity.right => λ (a, _), cod a | Arity.bottom => λ _, bot, - λ z, Empty.elim z)⟩ + λ z, explode z)⟩ variable (𝒞 : Precategory.{u}) diff --git a/GroundZero/Algebra/EilenbergMacLane.lean b/GroundZero/Algebra/EilenbergMacLane.lean index d19ebdd..df684b4 100644 --- a/GroundZero/Algebra/EilenbergMacLane.lean +++ b/GroundZero/Algebra/EilenbergMacLane.lean @@ -33,7 +33,7 @@ namespace K1 (groupoidπ : Π x, groupoid (C x)) : Π x, C x := λ x, Quot.withUseOf (loopπ, mulπ, groupoidπ) (Opaque.ind (λ ★, baseπ) x) x - attribute [eliminator] ind + attribute [induction_eliminator] ind hott axiom rec {C : Type v} (baseπ : C) (loopπ : G.carrier → baseπ = baseπ) (mulπ : Π x y, loopπ (G.φ x y) = loopπ x ⬝ loopπ y) diff --git a/GroundZero/Algebra/Geometry.lean b/GroundZero/Algebra/Geometry.lean index 756e01c..65d1d2f 100644 --- a/GroundZero/Algebra/Geometry.lean +++ b/GroundZero/Algebra/Geometry.lean @@ -9,7 +9,7 @@ namespace GroundZero.Algebra universe u v hott def Pregeometry : Type (max u v + 1) := - @Alg.{0, 0, u, v} 𝟎 𝟐 (Coproduct.elim Empty.elim (Bool.rec 3 4)) + @Alg.{0, 0, u, v} 𝟎 𝟐 (Coproduct.elim explode (Bool.rec 3 4)) namespace Pregeometry def between (G : Pregeometry) (a b c : G.carrier) := @@ -77,4 +77,4 @@ namespace GroundZero.Algebra Ens.parallel (geodesic G a₂ b₂) (geodesic G a₃ b₃) → Ens.parallel (geodesic G a₁ b₁) (geodesic G a₂ b₂)) end Pregeometry -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Alternating.lean b/GroundZero/Algebra/Group/Alternating.lean index 3a7843f..efc3eea 100644 --- a/GroundZero/Algebra/Group/Alternating.lean +++ b/GroundZero/Algebra/Group/Alternating.lean @@ -28,7 +28,7 @@ namespace Group inductive D₃.carrier | R₀ | R₁ | R₂ | S₀ | S₁ | S₂ - attribute [eliminator] D₃.carrier.casesOn + attribute [induction_eliminator] D₃.carrier.casesOn open D₃.carrier diff --git a/GroundZero/Algebra/Group/Finite.lean b/GroundZero/Algebra/Group/Finite.lean index 5d3b57d..8b2ad11 100644 --- a/GroundZero/Algebra/Group/Finite.lean +++ b/GroundZero/Algebra/Group/Finite.lean @@ -4,6 +4,7 @@ import GroundZero.Theorems.Nat open GroundZero.Types.Equiv (transport) open GroundZero.Types.Id (ap) open GroundZero.Types +open GroundZero.Proto namespace GroundZero universe u v w @@ -28,7 +29,7 @@ namespace Types.Coproduct Σ (x : A), Π y, ¬(x = f y) hott def Diff.inl : Diff (@Sum.inl A B) → B := - λ | ⟨Sum.inl x, p⟩ => Proto.Empty.elim (p x Id.refl) + λ | ⟨Sum.inl x, p⟩ => explode (p x Id.refl) | ⟨Sum.inr x, p⟩ => x hott def Empty.lift : Proto.Empty.{u} → Proto.Empty.{v} := @@ -41,7 +42,7 @@ namespace Types.Coproduct begin existsi Diff.inl; apply Prod.mk <;> existsi Diff.inr; { intro ⟨x, p⟩; induction x using Sum.casesOn; - { apply Proto.Empty.elim; fapply p; assumption; reflexivity }; + { apply explode; fapply p; assumption; reflexivity }; { fapply Types.Sigma.prod; reflexivity; { apply Structures.piProp; intro; apply Structures.notIsProp } } }; @@ -78,7 +79,7 @@ namespace Types.Coproduct begin existsi zero; apply Prod.mk <;> existsi Sum.inr <;> intro x; { induction x using Sum.casesOn; - apply Proto.Empty.elim; assumption; + apply explode; assumption; reflexivity }; { reflexivity } end @@ -87,9 +88,9 @@ end Types.Coproduct namespace Types.Product hott def destroy : 𝟎 × A ≃ 𝟎 := begin existsi Prod.fst; apply Prod.mk <;> - existsi Proto.Empty.elim <;> intro x; - apply Proto.Empty.elim x.1; - apply Proto.Empty.elim x + existsi explode <;> intro x; + apply explode x.1; + apply explode x end hott def split : (A + B) × C → (A × C) + (B × C) diff --git a/GroundZero/Algebra/Group/Free.lean b/GroundZero/Algebra/Group/Free.lean index 1ea7ef8..b093e4b 100644 --- a/GroundZero/Algebra/Group/Free.lean +++ b/GroundZero/Algebra/Group/Free.lean @@ -61,7 +61,7 @@ namespace Group def rec (G : Group) (f : ε → G.carrier) (x : F.carrier ε) : G.carrier := Exp.eval G f x.value - @[eliminator] def ind {π : F.carrier ε → Type v} + @[induction_eliminator] def ind {π : F.carrier ε → Type v} (setπ : Π x, Structures.hset (π x)) (u : π unit) (η : Π x, π (elem x)) (m : Π {x y}, π x → π y → π (mul x y)) diff --git a/GroundZero/Algebra/Group/Isomorphism.lean b/GroundZero/Algebra/Group/Isomorphism.lean index 18573c1..cc274c7 100644 --- a/GroundZero/Algebra/Group/Isomorphism.lean +++ b/GroundZero/Algebra/Group/Isomorphism.lean @@ -60,11 +60,10 @@ namespace Group noncomputable hott def ker.decodeSigma {φ : Hom G H} : Π (x : im.carrier φ), fib ker.encode x := begin - intro ⟨x, (p : ∥_∥)⟩; induction p; case elemπ z => - { existsi ker.incl z.1; fapply Types.Sigma.prod; + apply Sigma.Ind; intro x; fapply Merely.ind; + { intro z; existsi ker.incl z.1; fapply Types.Sigma.prod; apply z.2; apply HITs.Merely.uniq }; - case uniqπ p q => - { fapply Types.Sigma.prod; + { intro w p q; fapply Types.Sigma.prod; { apply ker.encodeInj; transitivity; exact p.2; symmetry; exact q.2 }; { apply Ens.hset; apply H.hset } } diff --git a/GroundZero/Algebra/Orgraph.lean b/GroundZero/Algebra/Orgraph.lean index 30030d0..e474a69 100644 --- a/GroundZero/Algebra/Orgraph.lean +++ b/GroundZero/Algebra/Orgraph.lean @@ -39,7 +39,7 @@ namespace GroundZero.Algebra class order (Γ : Orgraph) extends reflexive Γ, antisymmetric Γ, transitive Γ def Overring.κ (T : Overring) : Orgraph := - ⟨T.1, (λ z, nomatch z, T.2.2)⟩ + ⟨T.1, (λ z, explode z, T.2.2)⟩ class connected (Γ : Orgraph) := (total : Π x y, ∥Γ.ρ x y + Γ.ρ y x∥) @@ -91,7 +91,7 @@ namespace GroundZero.Algebra begin fapply GroundZero.HITs.Merely.rec _ _ (@connected.total T.κ _ _ _); change T.carrier; exact 0; change T.carrier; exact 1; apply T.κ.prop; - { intro z; induction z using Sum.casesOn; assumption; apply Empty.elim; + { intro z; induction z using Sum.casesOn; assumption; apply explode; apply @field.nontrivial T.τ _; apply @antisymmetric.asymm T.κ; assumption; apply Equiv.transport; apply ring.minusOneSqr; apply orfield.leOverMul <;> @@ -198,7 +198,7 @@ namespace GroundZero.Algebra { intro ih; induction ih; assumption; match @Classical.lem _ (a = b) (T.hset _ _) with | Sum.inl r₁ => _ | Sum.inr r₂ => _; apply eqImplReflRel T.κ; symmetry; apply ap T.τ.neg r₁; - apply Empty.elim; apply (_ : T.σ 0 0).1; reflexivity; + apply explode; apply (_ : T.σ 0 0).1; reflexivity; apply Equiv.transportconst; apply Equiv.bimap; apply @Group.mulRightInv T.τ⁺; exact a; apply @Group.mulRightInv T.τ⁺; exact b; diff --git a/GroundZero/Algebra/Reals.lean b/GroundZero/Algebra/Reals.lean index 6b8b56f..b7305f1 100644 --- a/GroundZero/Algebra/Reals.lean +++ b/GroundZero/Algebra/Reals.lean @@ -4,6 +4,7 @@ import GroundZero.Theorems.Nat open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Theorems +open GroundZero.Proto open GroundZero.Types open GroundZero.HITs @@ -69,7 +70,7 @@ namespace GroundZero.Algebra noncomputable hott def N.incl.lt : Π (n m : ℕ), (n ≤ m : Type) → R.ρ (N.incl n) (N.incl m) | Nat.zero, Nat.zero => λ _, @reflexive.refl R.κ _ (N.incl 0) | Nat.zero, Nat.succ m => λ _, @transitive.trans R.κ _ (N.incl 0) (N.incl m) (N.incl (m + 1)) (lt 0 m (Nat.max.zeroLeft m)) (leAddOne (N.incl m)) - | Nat.succ n, Nat.zero => λ p, GroundZero.Proto.Empty.elim (Nat.max.neZero p) + | Nat.succ n, Nat.zero => λ p, explode (Nat.max.neZero p) | Nat.succ n, Nat.succ m => λ p, orfield.leOverAdd (N.incl n) (N.incl m) 1 (lt n m (ap Nat.pred p)) noncomputable hott def R.complete (φ : R.subset) (H : φ.inh) (G : @majorized R.κ φ) : @@ -138,8 +139,8 @@ namespace GroundZero.Algebra begin intros p q; match p, q with | Sum.inl p₁, Sum.inl q₁ => { apply ap; apply R.κ.prop } - | Sum.inl p₁, Sum.inr q₂ => { apply GroundZero.Proto.Empty.elim; apply R.notNotTotal x y <;> assumption } - | Sum.inr p₂, Sum.inl q₁ => { apply GroundZero.Proto.Empty.elim; apply R.notNotTotal x y <;> assumption } + | Sum.inl p₁, Sum.inr q₂ => { apply explode; apply R.notNotTotal x y <;> assumption } + | Sum.inr p₂, Sum.inl q₁ => { apply explode; apply R.notNotTotal x y <;> assumption } | Sum.inr (p, p'), Sum.inr (q, q') => { apply ap; apply Product.prod; apply notIsProp; apply R.κ.prop } end @@ -162,7 +163,7 @@ namespace GroundZero.Algebra noncomputable hott def abs.pos {x : ℝ} (p : R.ρ 0 x) : abs x = x := begin change Coproduct.elim _ _ _ = _; induction R.total 0 x; - reflexivity; apply GroundZero.Proto.Empty.elim; + reflexivity; apply explode; apply R.notNotTotal 0 x <;> assumption end @@ -307,7 +308,7 @@ namespace GroundZero.Algebra intro p; induction R.total 0 x; case inl q₁ => { apply q₁ }; case inr q₂ => - { apply GroundZero.Proto.Empty.elim; apply (strictIneqAdd R q₂ q₂).1; + { apply explode; apply (strictIneqAdd R q₂ q₂).1; apply @antisymmetric.asymm R.κ; apply ineqAdd <;> exact q₂.2; apply Equiv.transport (R.ρ · (x + x)); symmetry; apply R.τ⁺.mulOne; exact p } end diff --git a/GroundZero/Exercises/Chap2.lean b/GroundZero/Exercises/Chap2.lean index 4b30a62..c681f8d 100644 --- a/GroundZero/Exercises/Chap2.lean +++ b/GroundZero/Exercises/Chap2.lean @@ -133,8 +133,8 @@ namespace «2.8» hott definition ρ : Π {x y : A + B}, Coproduct.code x y → Coproduct.code (φ g h x) (φ g h y) | Sum.inl _, Sum.inl _, p => ap _ p - | Sum.inr _, Sum.inl _, p => Empty.elim p - | Sum.inl _, Sum.inr _, p => Empty.elim p + | Sum.inr _, Sum.inl _, p => explode p + | Sum.inl _, Sum.inr _, p => explode p | Sum.inr _, Sum.inr _, p => ap _ p hott definition mapPathSum (x y : A + B) : Π p, @@ -148,8 +148,8 @@ namespace «2.8» | Sum.inr x, Sum.inr y => _; { intro (p : x = y); induction p; reflexivity }; - { intro; apply Empty.elim; assumption }; - { intro; apply Empty.elim; assumption }; + { intro; apply explode; assumption }; + { intro; apply explode; assumption }; { intro (p : x = y); induction p; reflexivity } end end «2.8» diff --git a/GroundZero/Exercises/Chap3.lean b/GroundZero/Exercises/Chap3.lean index 7135dff..4e7bd09 100644 --- a/GroundZero/Exercises/Chap3.lean +++ b/GroundZero/Exercises/Chap3.lean @@ -96,11 +96,11 @@ namespace «3.9» hott definition lemTrue (x : A) : lem A H = Sum.inl x := match lem A H with | Sum.inl y => ap Sum.inl (H y x) - | Sum.inr φ => Empty.elim (φ x) + | Sum.inr φ => explode (φ x) hott definition lemFalse (φ : ¬A) : lem A H = Sum.inr φ := match lem A H with - | Sum.inl x => Empty.elim (φ x) + | Sum.inl x => explode (φ x) | Sum.inr ψ => ap Sum.inr (Structures.notIsProp ψ φ) end @@ -113,7 +113,7 @@ namespace «3.9» hott lemma propsetInhIsProp (A : Prop) : prop A.1 := A.2 hott lemma Ωlinv (lem : LEM₋₁) : Ωelim lem ∘ Ωintro ~ idfun - | false => ap (Coproduct.elim _ _) (lemFalse Empty.elim) + | false => ap (Coproduct.elim _ _) (lemFalse explode) | true => ap (Coproduct.elim _ _) (lemTrue ★) noncomputable hott lemma Ωrinv (lem : LEM₋₁) : Ωintro ∘ Ωelim lem ~ idfun := @@ -125,7 +125,7 @@ namespace «3.9» fapply Sigma.mk; exact x; intro y; apply w.2; transitivity; apply ap; apply ap (Bool.elim _ _); apply ap (Coproduct.elim _ _); - apply lemFalse φ; symmetry; apply ua; apply uninhabitedType; exact Empty.elim ∘ φ + apply lemFalse φ; symmetry; apply ua; apply uninhabitedType; exact explode ∘ φ end noncomputable hott theorem lemImplPropEqvBool (lem : LEM₋₁) : Prop u ≃ 𝟐 := @@ -159,7 +159,7 @@ namespace «3.10» begin intro b; transitivity; apply ap Ωintro; apply Ωlinv; apply Equiv.propset.Id; symmetry; apply ua; induction b using Bool.casesOn; - { apply uninhabitedType; exact Empty.elim ∘ Resize.elim }; + { apply uninhabitedType; exact explode ∘ Resize.elim }; { apply Structures.contrEquivUnit; existsi Resize.intro ★; intro (Resize.intro b); apply ap; apply Structures.unitIsProp } end @@ -212,7 +212,7 @@ end «3.11» namespace «3.12» hott lemma implOfSum {A : Type u} {B : Type v} : (¬A) + B → A → B - | Sum.inl φ => Empty.elim ∘ φ + | Sum.inl φ => explode ∘ φ | Sum.inr b => λ _, b hott theorem WC (lem : LEM₋₁ u) : Π (A : Type u), ∥(∥A∥ → A)∥ := @@ -233,7 +233,7 @@ namespace «3.13» hott lemma LEMinfImplDNInf (lem : LEM∞ u) {A : Type u} : ∥A∥ → A := match lem A with | Sum.inl a => λ _, a - | Sum.inr φ => λ w, Empty.elim (@merelyImplDn A w φ) + | Sum.inr φ => λ w, explode (@merelyImplDn A w φ) -- see lemma 3.8.2 hott theorem LEMinfImplCartesian (lem : LEM∞ v) (A : Type u) (B : A → Type v) : @@ -251,7 +251,7 @@ namespace «3.13» hott lemma LEMinfDual (lem : LEM∞ v) {A : Type u} {B : A → Type v} : ¬(Σ x, ¬B x) → Π x, B x := λ φ x, match lem (B x) with | Sum.inl b => b - | Sum.inr ψ => Empty.elim (φ ⟨x, ψ⟩) + | Sum.inr ψ => explode (φ ⟨x, ψ⟩) end «3.13» -- exercise 3.14 @@ -265,7 +265,7 @@ namespace «3.14» λ x φ, φ x hott definition dn.rec (lem : LEM₋₁ v) {A : Type u} {B : Type v} : prop B → (A → B) → (¬¬A → B) := - λ H f, Coproduct.elim (λ b _, b) (λ φ g, Empty.elim (g (φ ∘ f))) (lem B H) + λ H f, Coproduct.elim (λ b _, b) (λ φ g, explode (g (φ ∘ f))) (lem B H) hott definition dn.recβrule (lem : LEM₋₁ v) {A : Type u} {B : Type v} {H : prop B} {f : A → B} (x : A) : dn.rec lem H f (dn.intro x) = f x := @@ -321,7 +321,7 @@ namespace «3.16.1» hott lemma dn.intro (lem : LEM₋₁ v) : (Π x, ¬¬(Y x)) → ¬¬(Π x, Y x) := λ φ f, f (λ x, match lem (Y x) (G x) with | Sum.inl y => y - | Sum.inr g => Empty.elim (φ x g)) + | Sum.inr g => explode (φ x g)) hott theorem dn.comm (lem : LEM₋₁ v) : ¬¬(Π x, Y x) ≃ (Π x, ¬¬(Y x)) := begin @@ -387,7 +387,7 @@ namespace «3.18» apply Prod.mk; intro lem P H nnp; induction lem P H using Sum.casesOn; case inl p => { exact p }; - case inr np => { apply Empty.elim (nnp np) }; + case inr np => { apply explode (nnp np) }; intro dneg P H; apply dneg; apply propEM H; intro npnp; apply npnp; right; intro p; apply npnp; left; exact p @@ -502,7 +502,7 @@ namespace «3.22» @transport _ Y (fin.fsuc m') m (Sigma.prod (idp m.1) (Nat.le.prop _ _ _ _)) (prev m') hott theorem finAC : Π (n : ℕ) (Y : fin n → Type u), (Π x, ∥Y x∥) → ∥Π x, Y x∥ - | Nat.zero, Y, _ => Merely.elem (λ k, Empty.elim (Nat.max.neZero k.2)) + | Nat.zero, Y, _ => Merely.elem (λ k, explode (Nat.max.neZero k.2)) | Nat.succ n, Y, H => Merely.lift₂ (step n Y) (finAC n (Y ∘ fin.fsuc) (λ m, H (fin.fsuc m))) (H (fin.fmax n)) end «3.22» @@ -513,7 +513,7 @@ namespace «3.23» open GroundZero.HITs hott definition choice {A : Type u} (G : dec A) : A → Type u := - λ x, Coproduct.elim (x = ·) (λ φ, Empty.elim (φ x)) G + λ x, Coproduct.elim (x = ·) (λ φ, explode (φ x)) G hott definition decMerely {A : Type u} (G : dec A) : Type u := Σ x, choice G x @@ -522,7 +522,7 @@ namespace «3.23» begin intro x; induction G using Sum.casesOn; case inl y => { existsi y; apply idp }; - case inr φ => { apply Empty.elim (φ x) } + case inr φ => { apply explode (φ x) } end hott definition decMerely.uniq {A : Type u} (G : dec A) : prop (decMerely G) := @@ -533,7 +533,7 @@ namespace «3.23» { transitivity; apply transportCompositionRev; apply Equiv.rewriteComp; symmetry; apply Id.cancelInvComp } }; - case inr φ => { intro w₁ w₂; apply Empty.elim (φ w₁.1) } + case inr φ => { intro w₁ w₂; apply explode (φ w₁.1) } end hott definition decMerely.dec {A : Type u} (G : dec A) : dec (@decMerely A G) := diff --git a/GroundZero/Exercises/Chap4.lean b/GroundZero/Exercises/Chap4.lean index 8718466..695f926 100644 --- a/GroundZero/Exercises/Chap4.lean +++ b/GroundZero/Exercises/Chap4.lean @@ -443,8 +443,8 @@ namespace «4.8» { intro w; existsi Bool.elim w.1.1 w.1.2; intro b₁ b₂ p; match b₁, b₂ with | false, false => { reflexivity } - | false, true => { apply Empty.elim; apply w.2; exact p } - | true, false => { apply Empty.elim; apply w.2; exact p⁻¹ } + | false, true => { apply explode; apply w.2; exact p } + | true, false => { apply explode; apply w.2; exact p⁻¹ } | true, true => { reflexivity } }; apply Prod.mk; { intro w; apply Sigma.prod; apply notIsProp; reflexivity }; @@ -469,12 +469,12 @@ namespace «4.8» | false, false => { fapply Sigma.mk; intro; reflexivity; apply Prod.mk; { intro; apply contrImplProp; apply w.2.2.1 }; { intro; apply boolIsSet } } - | false, true => { fapply Sigma.mk; intro p; apply Empty.elim; apply w.2.1 p; apply Prod.mk; - { intro p; apply Empty.elim; apply w.2.1 p }; - { intro; apply Empty.elim; apply ffNeqTt; assumption } } - | true, false => { fapply Sigma.mk; intro p; apply Empty.elim; apply w.2.1 p⁻¹; apply Prod.mk; - { intro p; apply Empty.elim; apply w.2.1 p⁻¹ }; - { intro; apply Empty.elim; apply ffNeqTt; symmetry; assumption } } + | false, true => { fapply Sigma.mk; intro p; apply explode; apply w.2.1 p; apply Prod.mk; + { intro p; apply explode; apply w.2.1 p }; + { intro; apply explode; apply ffNeqTt; assumption } } + | true, false => { fapply Sigma.mk; intro p; apply explode; apply w.2.1 p⁻¹; apply Prod.mk; + { intro p; apply explode; apply w.2.1 p⁻¹ }; + { intro; apply explode; apply ffNeqTt; symmetry; assumption } } | true, true => { fapply Sigma.mk; intro; reflexivity; apply Prod.mk; { intro; apply contrImplProp; apply w.2.2.2 }; { intro; apply boolIsSet } } }; diff --git a/GroundZero/HITs/Circle.lean b/GroundZero/HITs/Circle.lean index 6bdf00a..360c51f 100644 --- a/GroundZero/HITs/Circle.lean +++ b/GroundZero/HITs/Circle.lean @@ -26,7 +26,7 @@ section open Suspension (north south rec ind) hott lemma suspEmpty : ∑ 𝟎 ≃ 𝟐 := - Equiv.intro (rec false true Empty.elim) + Equiv.intro (rec false true explode) (λ | false => north | true => south) (ind (idp north) (idp south) (λ ε, nomatch ε)) (λ | false => idp false | true => idp true) @@ -153,7 +153,7 @@ namespace Circle hott definition ind {B : S¹ → Type u} (b : B base) (ℓ : b =[loop] b) : Π (x : S¹), B x := ind₂ b (transport B seg₁ b) (idp _) (depPathTransSymm ℓ) - attribute [eliminator] ind + attribute [induction_eliminator] ind hott definition indβrule₁ {B : S¹ → Type u} (b : B base) (ℓ : b =[loop] b) : ind b ℓ base = b := idp b @@ -844,11 +844,11 @@ namespace Circle hott theorem plusEqZeroRight {n : ℕ} : Π {m : ℕ}, n + m = 0 → m = 0 | Nat.zero, _ => idp 0 - | Nat.succ _, H => Empty.elim (succNeqZero H) + | Nat.succ _, H => explode (succNeqZero H) hott theorem multEqOneRight : Π (n m : ℕ), n * m = 1 → m = 1 - | n, Nat.zero, H => Empty.elim (succNeqZero H⁻¹) - | Nat.zero, Nat.succ m, H => Empty.elim (succNeqZero (H⁻¹ ⬝ Theorems.Nat.zeroMul _)) + | n, Nat.zero, H => explode (succNeqZero H⁻¹) + | Nat.zero, Nat.succ m, H => explode (succNeqZero (H⁻¹ ⬝ Theorems.Nat.zeroMul _)) | Nat.succ n, Nat.succ m, H => (H⁻¹ ⬝ ap (λ k, Nat.succ k * Nat.succ m) (plusEqZeroRight (Theorems.Nat.succInj H)) ⬝ Theorems.Nat.oneMul _)⁻¹ @@ -1013,7 +1013,7 @@ namespace Circle hott theorem absOneDec : Π (z : ℤ), abs z = 1 → (z = 1) + (z = -1) | Integer.pos n, H => Coproduct.inl (ap Integer.pos H) | Integer.neg Nat.zero, _ => Coproduct.inr (idp _) - | Integer.neg (Nat.succ n), H => Empty.elim (succNeqZero (Theorems.Nat.succInj H)) + | Integer.neg (Nat.succ n), H => explode (succNeqZero (Theorems.Nat.succInj H)) hott corollary absOneImplSqrEqOne (z : ℤ) (H : abs z = 1) : z * z = 1 := match absOneDec z H with @@ -1146,11 +1146,11 @@ namespace Circle intro w; apply neqZeroImplNeqMinus; exact H; exact w.1⁻¹ ⬝ w.2; { intro G; induction i using Sum.casesOn; { left; apply ap pos; exact G }; - { induction j using Nat.casesOn; left; apply Empty.elim; apply H; reflexivity; + { induction j using Nat.casesOn; left; apply explode; apply H; reflexivity; right; apply ap Sum.inr; apply Theorems.Nat.succInj; exact G } }; { intro G; induction G using Sum.casesOn; transitivity; apply ap abs; assumption; reflexivity; transitivity; apply ap abs; assumption; - induction j using Nat.casesOn; apply Empty.elim; + induction j using Nat.casesOn; apply explode; apply H; reflexivity; reflexivity } end diff --git a/GroundZero/HITs/Coequalizer.lean b/GroundZero/HITs/Coequalizer.lean index e4d3869..8314ffa 100644 --- a/GroundZero/HITs/Coequalizer.lean +++ b/GroundZero/HITs/Coequalizer.lean @@ -28,7 +28,7 @@ namespace Coeq (ρ : Π x, i (f x) =[resp x] i (g x)) : Π x, C x := begin fapply Quotient.ind; apply i; intros x y H; induction H using rel.casesOn; apply ρ end - attribute [eliminator] ind + attribute [induction_eliminator] ind hott definition indβrule (C : Coeq f g → Type w) (i : Π x, C (iota x)) (ρ : Π x, i (f x) =[resp x] i (g x)) (x : A) : apd (ind C i ρ) (resp x) = ρ x := diff --git a/GroundZero/HITs/Colimit.lean b/GroundZero/HITs/Colimit.lean index d7ce714..0f396c8 100644 --- a/GroundZero/HITs/Colimit.lean +++ b/GroundZero/HITs/Colimit.lean @@ -39,7 +39,7 @@ namespace Colimit { intros u v H; induction H; apply glueπ } end - attribute [eliminator] ind + attribute [induction_eliminator] ind hott definition rec {B : Type v} (inclπ : Π (n : ℕ), A n → B) (glueπ : Π (n : ℕ) (x : A n), inclπ (n + 1) (f n x) = inclπ n x) : Colimit A f → B := diff --git a/GroundZero/HITs/Generalized.lean b/GroundZero/HITs/Generalized.lean index d2441f8..d9ac84c 100644 --- a/GroundZero/HITs/Generalized.lean +++ b/GroundZero/HITs/Generalized.lean @@ -26,7 +26,7 @@ namespace Generalized (glueπ : Π a b, inclπ a =[glue a b] inclπ b) : Π x, B x := begin fapply Quotient.ind; exact inclπ; { intros u v H; induction H; apply glueπ } end - attribute [eliminator] ind + attribute [induction_eliminator] ind hott definition rec {A : Type u} {B : Type v} (inclπ : A → B) (glueπ : Π a b, inclπ a = inclπ b) : {A} → B := diff --git a/GroundZero/HITs/Join.lean b/GroundZero/HITs/Join.lean index b49d4fd..bdea3d2 100644 --- a/GroundZero/HITs/Join.lean +++ b/GroundZero/HITs/Join.lean @@ -1,7 +1,10 @@ import GroundZero.HITs.Suspension -open GroundZero.Types.Equiv (pathoverOfEq) +open GroundZero.Types.Id (ap) +open GroundZero.Types.Equiv open GroundZero.Types +open GroundZero.Proto +open Prod (pr₁ pr₂) /- Join. @@ -10,34 +13,40 @@ open GroundZero.Types namespace GroundZero.HITs -universe u v w -def Join (A : Type u) (B : Type v) := -@Pushout A B (A × B) Prod.pr₁ Prod.pr₂ +universe u v w u' v' w' + +hott definition Join (A : Type u) (B : Type v) := +@Pushout A B (A × B) pr₁ pr₂ + +infixl:70 " ∗ " => Join namespace Join variable {A : Type u} {B : Type v} - def inl : A → Join A B := Pushout.inl - def inr : B → Join A B := Pushout.inr + hott definition inl : A → A ∗ B := Pushout.inl + hott definition inr : B → A ∗ B := Pushout.inr - hott def push (a : A) (b : B) : inl a = inr b := + hott definition glue (a : A) (b : B) : inl a = inr b := Pushout.glue (a, b) - hott def ind {C : Join A B → Type w} + hott definition ind {C : A ∗ B → Type w} (inlπ : Π (x : A), C (inl x)) (inrπ : Π (x : B), C (inr x)) - (pushπ : Π (a : A) (b : B), inlπ a =[push a b] inrπ b) : Π x, C x := + (pushπ : Π (a : A) (b : B), inlπ a =[glue a b] inrπ b) : Π x, C x := Pushout.ind inlπ inrπ (λ w, pushπ w.1 w.2) - attribute [eliminator] ind + attribute [induction_eliminator] ind + + hott definition rec {C : Type w} (f : A → C) (g : B → C) (H : Π a b, f a = g b) : A ∗ B → C := + Pushout.rec f g (λ w, H w.1 w.2) - hott def rec {C : Type w} (inlπ : A → C) (inrπ : B → C) - (pushπ : Π a b, inlπ a = inrπ b) : Join A B → C := - Pushout.rec inlπ inrπ (λ w, pushπ w.1 w.2) + hott definition recβrule {C : Type w} (f : A → C) (g : B → C) (H : Π a b, f a = g b) (a : A) (b : B) : + ap (rec f g H) (glue a b) = H a b := + by apply Pushout.recβrule - hott def fromSusp : ∑ A → Join 𝟐 A := - Suspension.rec (inl false) (inl true) (λ x, push false x ⬝ (push true x)⁻¹) + hott definition fromSusp : ∑ A → 𝟐 ∗ A := + Suspension.rec (inl false) (inl true) (λ x, glue false x ⬝ (glue true x)⁻¹) - hott def toSusp : Join 𝟐 A → ∑ A := + hott definition toSusp : 𝟐 ∗ A → ∑ A := rec (λ | false => Suspension.north | true => Suspension.south) (λ _, Suspension.south) diff --git a/GroundZero/HITs/Merely.lean b/GroundZero/HITs/Merely.lean index 38cf7a3..b981cdc 100644 --- a/GroundZero/HITs/Merely.lean +++ b/GroundZero/HITs/Merely.lean @@ -46,7 +46,7 @@ namespace Merely Colimit.ind (resp elemπ uniqπ) (λ _ _, uniqπ _ _ _) end - attribute [eliminator] ind + attribute [induction_eliminator] ind hott definition rec {A : Type u} {B : Type v} (H : prop B) (f : A → B) : ∥A∥ → B := ind f (λ _, H) diff --git a/GroundZero/HITs/Pushout.lean b/GroundZero/HITs/Pushout.lean index dbfbdcf..2786673 100644 --- a/GroundZero/HITs/Pushout.lean +++ b/GroundZero/HITs/Pushout.lean @@ -43,7 +43,7 @@ namespace Pushout { intros u v H; induction H using rel.casesOn; apply glueπ } end - attribute [eliminator] ind + attribute [induction_eliminator] ind hott definition rec {D : Type w} (inlπ : A → D) (inrπ : B → D) (glueπ : Π x, inlπ (f x) = inrπ (g x)) : Pushout f g → D := diff --git a/GroundZero/HITs/Quotient.lean b/GroundZero/HITs/Quotient.lean index d6fc2b1..2219b44 100644 --- a/GroundZero/HITs/Quotient.lean +++ b/GroundZero/HITs/Quotient.lean @@ -25,7 +25,7 @@ namespace Quotient (f : A → B) (H : Π x y, R x y → f x = f y) : Quotient R → B := λ x, Quot.withUseOf H (Quot.lift f (λ a b, λ (rel.line ε), elimEq (H a b ε)) x.elim) x.elim - @[eliminator] hott axiom ind {A : Type u} {R : A → A → Type v} {B : Quotient R → Type w} + @[induction_eliminator] hott axiom ind {A : Type u} {R : A → A → Type v} {B : Quotient R → Type w} (f : Π x, B (elem x)) (ε : Π x y H, f x =[line H] f y) : Π x, B x := λ x, Quot.withUseOf ε (@Quot.hrecOn A (rel R) (B ∘ Resize.intro) x.elim f (λ a b, λ (rel.line H), HEq.fromPathover (line H) (ε a b H))) x.elim diff --git a/GroundZero/HITs/Reals.lean b/GroundZero/HITs/Reals.lean index 03b30dc..240e344 100644 --- a/GroundZero/HITs/Reals.lean +++ b/GroundZero/HITs/Reals.lean @@ -7,6 +7,7 @@ open GroundZero.HITs.Circle open GroundZero.Structures open GroundZero.Types.Id open GroundZero.Types +open GroundZero.Proto open GroundZero /- @@ -39,7 +40,7 @@ namespace Reals (sz : Π z, cz z =[glue z] cz (Integer.succ z)) (u : R) : C u := Quotient.ind cz (indρ cz sz) u - attribute [eliminator] ind + attribute [induction_eliminator] ind hott definition indβrule {C : R → Type u} (cz : Π x, C (elem x)) (sz : Π z, cz z =[glue z] cz (Integer.succ z)) @@ -166,7 +167,7 @@ namespace Reals hott lemma lemInfImplDnegInf (H : LEM∞) {A : Type u} (G : ¬¬A) : A := match H A with | Sum.inl x => x - | Sum.inr y => Proto.Empty.elim (G y) + | Sum.inr y => explode (G y) noncomputable hott remark circleNotHset : ¬(hset S¹) := begin intro H; apply Circle.loopNeqRefl; apply H end diff --git a/GroundZero/HITs/Setquot.lean b/GroundZero/HITs/Setquot.lean index 36cd7e3..c2073a6 100644 --- a/GroundZero/HITs/Setquot.lean +++ b/GroundZero/HITs/Setquot.lean @@ -35,7 +35,7 @@ begin { intro; apply zeroEqvSet.left; apply set } end -attribute [eliminator] Setquot.ind +attribute [induction_eliminator] Setquot.ind hott definition Setquot.rec {A : Type u} {R : A → A → Prop u'} {B : Type v} (elemπ : A → B) (lineπ : Π x y, (R x y).fst → elemπ x = elemπ y) (set : hset B) : Setquot R → B := @@ -76,7 +76,7 @@ hott definition Relquot.ind {A : Type u} {s : eqrel A} (set : Π x, hset (π x)) : Π x, π x := Setquot.ind elemπ lineπ set -attribute [eliminator] Relquot.ind +attribute [induction_eliminator] Relquot.ind hott definition Relquot.indProp {A : Type u} {s : eqrel A} {π : Relquot s → Type v} (elemπ : Π x, π (Relquot.elem x)) diff --git a/GroundZero/HITs/Suspension.lean b/GroundZero/HITs/Suspension.lean index 2dcb34a..9af819a 100644 --- a/GroundZero/HITs/Suspension.lean +++ b/GroundZero/HITs/Suspension.lean @@ -13,14 +13,15 @@ open GroundZero.Types namespace GroundZero namespace HITs -hott definition Suspension.{u} (A : Type u) := +universe u v w + +hott definition Suspension (A : Type u) := @Pushout.{0, 0, u} 𝟏 𝟏 A (λ _, ★) (λ _, ★) notation "∑ " => Suspension namespace Suspension -- https://github.com/leanprover/lean2/blob/master/hott/homotopy/susp.hlean - universe u v hott definition north {A : Type u} : ∑ A := Pushout.inl ★ hott definition south {A : Type u} : ∑ A := Pushout.inr ★ @@ -32,7 +33,7 @@ namespace Suspension (m : Π x, n =[merid x] s) : Π x, B x := Pushout.ind (λ ★, n) (λ ★, s) m - attribute [eliminator] ind + attribute [induction_eliminator] ind hott definition rec {A : Type u} {B : Type v} (n s : B) (m : A → n = s) : ∑ A → B := Pushout.rec (λ _, n) (λ _, s) m diff --git a/GroundZero/HITs/Trunc.lean b/GroundZero/HITs/Trunc.lean index f767185..9724835 100644 --- a/GroundZero/HITs/Trunc.lean +++ b/GroundZero/HITs/Trunc.lean @@ -34,7 +34,7 @@ namespace Trunc | −1 => Merely.hprop | succ (succ n) => λ _ _, propIsNType (λ _ _, trustCoherence) n - @[eliminator] hott axiom ind {B : Trunc n A → Type v} (elemπ : Π x, B (elem x)) (uniqπ : Π x, is-n-type (B x)) : Π x, B x := + @[induction_eliminator] hott axiom ind {B : Trunc n A → Type v} (elemπ : Π x, B (elem x)) (uniqπ : Π x, is-n-type (B x)) : Π x, B x := match n with | −2 => λ x, (uniqπ x).1 | −1 => Merely.ind elemπ (λ _, minusOneEqvProp.forward (uniqπ _)) diff --git a/GroundZero/HITs/Wedge.lean b/GroundZero/HITs/Wedge.lean index dce149d..7d010be 100644 --- a/GroundZero/HITs/Wedge.lean +++ b/GroundZero/HITs/Wedge.lean @@ -32,7 +32,7 @@ namespace Wedge (glueπ : inlπ A.2 =[glue] inrπ B.2) : Π x, C x := Pushout.ind inlπ inrπ (λ ★, glueπ) - attribute [eliminator] ind + attribute [induction_eliminator] ind hott definition rec {C : Type u} (inlπ : A.1 → C) (inrπ : B.1 → C) (glueπ : inlπ A.2 = inrπ B.2) : A ∨ B → C := diff --git a/GroundZero/Meta/HottTheory.lean b/GroundZero/Meta/HottTheory.lean index 87e797c..e3d766c 100644 --- a/GroundZero/Meta/HottTheory.lean +++ b/GroundZero/Meta/HottTheory.lean @@ -18,10 +18,6 @@ section def Lean.Expr.forConstsM [Monad M] (e : Expr) (f : Name → M Unit) : M Unit := e.foldConsts (pure ()) (λ n eff => do { f n; eff }) - - @[inline] def Option.forM [Pure M] : Option A → (A → M Unit) → M Unit - | none, _ => pure () - | some x, f => f x end def Lean.ConstantInfo.isAxiomInfo : ConstantInfo → Bool @@ -212,7 +208,7 @@ def defHoTT (tag declMods declId declDef : Syntax) : CommandElabM Name := do { let ns ← getCurrNamespace; let declName := ns ++ declId[0].getId; - withHoTTScope <| declDef.setKind ``Command.«def» + withHoTTScope <| declDef.setKind ``Command.definition |>.setArgs (Array.append #[mkAtom "def ", declId] declDef.getArgs) |> (mkNode ``Command.declaration #[declMods, ·]) |> elabDeclaration; @@ -247,7 +243,7 @@ def abbrevAttrs : Array Attribute := if cmd.isOfKind ``declCheck then do { let #[_, decls] := cmd.getArgs | throwError "invalid “check” statement"; - decls.getArgs.forM (λ stx => resolveGlobalConstNoOverloadWithInfo stx >>= checkAndMark stx) + decls.getArgs.forM (λ stx => resolveGlobalConstNoOverload stx >>= checkAndMark stx) } if cmd.isOfKind ``declAxiom then do { @@ -284,7 +280,7 @@ def abbrevAttrs : Array Attribute := let env ← getEnv; decls.getArgs.forM λ stx => do { - let n ← resolveGlobalConstNoOverloadWithInfo stx; + let n ← resolveGlobalConstNoOverload stx; if ¬(env.constants.find! n).isAxiomInfo then throwErrorAt stx "“{n}” expected to be an axiom."; @@ -296,8 +292,8 @@ def abbrevAttrs : Array Attribute := if cmd.isOfKind ``declImpl then do { let #[_, implOfStx, _, implFnStx] := cmd.getArgs | throwError "invalid “implementation” statement"; - let implOfName ← resolveGlobalConstNoOverloadWithInfo implOfStx; - let implFnName ← resolveGlobalConstNoOverloadWithInfo implFnStx + let implOfName ← resolveGlobalConstNoOverload implOfStx; + let implFnName ← resolveGlobalConstNoOverload implFnStx -- see https://github.com/leanprover/lean4/blob/fcb30c269bdbca7eac75fc5c5d62841db3d2f592/src/Lean/Compiler/ImplementedByAttr.lean#L13-L30 if implOfName = implFnName then { diff --git a/GroundZero/Meta/Notation.lean b/GroundZero/Meta/Notation.lean index fc5a3c0..88a6d71 100644 --- a/GroundZero/Meta/Notation.lean +++ b/GroundZero/Meta/Notation.lean @@ -203,7 +203,7 @@ def parseSubChar : Lean.Syntax → Char | `(subscriptChar| ₓ) => 'x' | _ => 'a' def parseIdent (φ : Lean.Syntax → Char) (stx : Array Lean.Syntax) := -String.mk (Array.map φ stx).toList +String.mk (Array.map φ stx).toList |> Lean.Name.str Lean.Name.anonymous def parseSubIdent := parseIdent parseSubChar def parseSupIdent := parseIdent parseSupChar diff --git a/GroundZero/Meta/Tactic.lean b/GroundZero/Meta/Tactic.lean index d81727a..8d13ff3 100644 --- a/GroundZero/Meta/Tactic.lean +++ b/GroundZero/Meta/Tactic.lean @@ -31,13 +31,6 @@ section (intro (a : A) (b : B) (c : C) : ρ a b → η b c → μ a c) end --- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Lean/Expr/Basic.lean#L100-L109 -def Lean.Expr.constName (e : Expr) : Name := -e.constName?.getD Name.anonymous - -def Lean.Expr.getAppFnArgs (e : Expr) : Name × Array Expr := -withApp e λ e a => (e.constName, a) - namespace GroundZero.Meta.Tactic -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Ring.lean#L411-L419 @@ -70,17 +63,6 @@ section elab "transitivity" : tactic => applyOnBinRel `transitivity `Transitive end --- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Basic.lean --- Author: Mario Carneiro -syntax "iterate" (ppSpace num)? ppSpace tacticSeq : tactic -macro_rules - | `(tactic|iterate $seq:tacticSeq) => - `(tactic|try ($seq:tacticSeq); iterate $seq:tacticSeq) - | `(tactic|iterate $n $seq:tacticSeq) => - match n.raw.toNat with - | 0 => `(tactic| skip) - | n + 1 => `(tactic|($seq:tacticSeq); iterate $(quote n) $seq:tacticSeq) - elab "fapply " e:term : tactic => Elab.Tactic.evalApplyLikeTactic (MVarId.apply (cfg := {newGoals := Meta.ApplyNewGoals.all})) e @@ -191,4 +173,4 @@ elab (priority := high) "calc " ε:term " : " τ:term σ:(calcLHS " : " term)* : return η -end GroundZero.Meta.Tactic \ No newline at end of file +end GroundZero.Meta.Tactic diff --git a/GroundZero/Proto.lean b/GroundZero/Proto.lean index 165d356..2011927 100644 --- a/GroundZero/Proto.lean +++ b/GroundZero/Proto.lean @@ -8,7 +8,7 @@ hott definition idfun {A : Sort u} : A → A := inductive Empty : Type u -attribute [eliminator] Empty.casesOn +attribute [induction_eliminator] Empty.casesOn hott definition Iff (A : Type u) (B : Type v) := (A → B) × (B → A) @@ -35,7 +35,7 @@ notation "𝟎" => Empty notation "𝟐" => Bool notation "ℕ" => Nat -hott definition Empty.elim {A : Sort u} (xs : 𝟎) : A := +hott definition explode {A : Sort u} (xs : 𝟎) : A := nomatch xs hott definition Bool.elim {A : Sort u} : A → A → 𝟐 → A := @@ -47,7 +47,7 @@ notation (priority := low) "⊥" => Bottom inductive Identity (A : Type u) | elem : A → Identity A -attribute [eliminator] Identity.casesOn +attribute [induction_eliminator] Identity.casesOn hott definition Identity.elim {A : Type u} : Identity A → A | Identity.elem a => a diff --git a/GroundZero/Structures.lean b/GroundZero/Structures.lean index 48909e9..6dced66 100644 --- a/GroundZero/Structures.lean +++ b/GroundZero/Structures.lean @@ -487,7 +487,7 @@ end hott lemma lemToDoubleNeg {A : Type u} : dec A → (¬¬A → A) | Sum.inl x => λ _, x -| Sum.inr t => λ g, Proto.Empty.elim (g t) +| Sum.inr t => λ g, explode (g t) hott theorem Hedberg {A : Type u} : dec⁼ A → hset A := begin intro H; apply doubleNegEq; intros x y; apply lemToDoubleNeg; apply H x y end @@ -790,12 +790,11 @@ macro "DNEG₋₁" n:level : term => `(DNEGprop.{$n}) namespace Structures open GroundZero.Types.Coproduct (inl inr) open GroundZero.Types.Id (ap) - open GroundZero.Proto hott theorem propSum {A : Type u} {B : Type v} (H₁ : prop A) (H₂ : prop B) (G : ¬(A × B)) : prop (A + B) | inl _, inl _ => ap inl (H₁ _ _) - | inr x, inl y => Empty.elim (G (y, x)) - | inl x, inr y => Empty.elim (G (x, y)) + | inr x, inl y => explode (G (y, x)) + | inl x, inr y => explode (G (x, y)) | inr _, inr _ => ap inr (H₂ _ _) hott corollary propEM {A : Type u} (H : prop A) : prop (A + ¬A) := diff --git a/GroundZero/Theorems/Classical.lean b/GroundZero/Theorems/Classical.lean index 817ed11..90bf852 100644 --- a/GroundZero/Theorems/Classical.lean +++ b/GroundZero/Theorems/Classical.lean @@ -4,6 +4,7 @@ open GroundZero.Types.Equiv (transport) open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types +open GroundZero.Proto namespace GroundZero universe u v w @@ -82,7 +83,7 @@ end noncomputable hott definition dneg.decode {A : Type u} (H : prop A) : ¬¬A → A := λ G, match lem H with | Sum.inl z => z -| Sum.inr φ => Proto.Empty.elim (G φ) +| Sum.inr φ => explode (G φ) hott definition dneg.encode {A : Type u} : A → ¬¬A := λ x p, p x @@ -99,7 +100,7 @@ section noncomputable hott definition Contrapos.elim : (¬B → ¬A) → (A → B) := λ f p, match lem H with | Sum.inl z => z - | Sum.inr φ => Proto.Empty.elim (f φ p) + | Sum.inr φ => explode (f φ p) noncomputable hott definition Contrapos : (A → B) ↔ (¬B → ¬A) := ⟨Contrapos.intro, Contrapos.elim H⟩ diff --git a/GroundZero/Theorems/Funext.lean b/GroundZero/Theorems/Funext.lean index f4d0311..643417b 100644 --- a/GroundZero/Theorems/Funext.lean +++ b/GroundZero/Theorems/Funext.lean @@ -38,7 +38,7 @@ namespace Interval | true, false, _ => HEq.symm s | true, true, _ => HEq.refl b₁) - @[eliminator] hott axiom ind {B : I → Type u} (b₀ : B i₀) (b₁ : B i₁) (s : b₀ =[seg] b₁) (x : I) : B x := + @[induction_eliminator] hott axiom ind {B : I → Type u} (b₀ : B i₀) (b₁ : B i₁) (s : b₀ =[seg] b₁) (x : I) : B x := Quot.withUseOf s (hrec B b₀ b₁ (HEq.fromPathover seg s) x) x hott opaque axiom indβrule {B : I → Type u} (b₀ : B i₀) (b₁ : B i₁) diff --git a/GroundZero/Theorems/Nat.lean b/GroundZero/Theorems/Nat.lean index 72d091b..8a0a046 100644 --- a/GroundZero/Theorems/Nat.lean +++ b/GroundZero/Theorems/Nat.lean @@ -154,7 +154,7 @@ namespace Nat hott lemma max.zero : Π n, max n 0 = 0 → n = 0 | Nat.zero, _ => idp _ - | Nat.succ n, p => Empty.elim (max.neZero p) + | Nat.succ n, p => explode (max.neZero p) hott corollary le.prop (n m : ℕ) : prop (n ≤ m) := natIsSet _ _ @@ -207,7 +207,7 @@ namespace Nat hott lemma minMax : Π (m n : ℕ), max m n = n → min m n = m | Nat.zero, Nat.zero, p => idp _ - | Nat.succ m, Nat.zero, p => Empty.elim (max.neZero p) + | Nat.succ m, Nat.zero, p => explode (max.neZero p) | Nat.zero, Nat.succ n, p => idp _ | Nat.succ m, Nat.succ n, p => ap Nat.succ (minMax m n (ap Nat.pred p)) @@ -246,12 +246,12 @@ namespace Nat begin intros p q; apply le.neSucc n; transitivity; exact q; exact p end hott lemma le.ofNotLe (m n : ℕ) (H : ¬(n + 1 ≤ m)) : m ≤ n := - match le.dec m n with | Sum.inl r₁ => r₁ | Sum.inr r₂ => Empty.elim (H r₂) + match le.dec m n with | Sum.inl r₁ => r₁ | Sum.inr r₂ => explode (H r₂) hott lemma le.neqSucc {n m : ℕ} (p : n ≠ m + 1) (q : n ≤ m + 1) : n ≤ m := match le.dec n m with | Sum.inl r₁ => r₁ - | Sum.inr r₂ => Empty.elim (p (le.asymm q r₂)) + | Sum.inr r₂ => explode (p (le.asymm q r₂)) hott lemma le.leSucc : Π (n : ℕ), n ≤ n + 1 | Nat.zero => idp _ diff --git a/GroundZero/Theorems/Univalence.lean b/GroundZero/Theorems/Univalence.lean index 5dcc222..f5ec900 100644 --- a/GroundZero/Theorems/Univalence.lean +++ b/GroundZero/Theorems/Univalence.lean @@ -90,7 +90,7 @@ namespace Equiv noncomputable hott definition J {A B : Type u} (e : A ≃ B) : C A B e := transport (λ (w : Σ B, A ≃ B), C A w.1 w.2) ((univAlt A).2 ⟨B, e⟩) (Cidp A) - attribute [eliminator] J + attribute [induction_eliminator] J noncomputable hott lemma Jβrule (A : Type u) : J Cidp (ideqv A) = Cidp A := begin @@ -208,13 +208,13 @@ begin | Sum.inr p₂, Sum.inl q₁ => _ | Sum.inl p₁, Sum.inr q₂ => _ | Sum.inr p₂, Sum.inr q₂ => _; - { apply Proto.Empty.elim; apply ffNeqTt; + { apply explode; apply ffNeqTt; apply eqvInj ⟨φ, H⟩; exact p₁ ⬝ q₁⁻¹ }; { transitivity; apply ap (bool.encode · x); apply p₂; symmetry; induction x using Bool.casesOn <;> assumption }; { transitivity; apply ap (bool.encode · x); apply p₁; symmetry; induction x using Bool.casesOn <;> assumption }; - { apply Proto.Empty.elim; apply ffNeqTt; + { apply explode; apply ffNeqTt; apply eqvInj ⟨φ, H⟩; exact p₂ ⬝ q₂⁻¹ } } end diff --git a/GroundZero/Types/Coproduct.lean b/GroundZero/Types/Coproduct.lean index c956a17..aec2922 100644 --- a/GroundZero/Types/Coproduct.lean +++ b/GroundZero/Types/Coproduct.lean @@ -1,6 +1,7 @@ import GroundZero.Types.Equiv open GroundZero.Types.Id (ap) +open GroundZero.Proto namespace GroundZero.Types universe u v w w' @@ -9,7 +10,7 @@ hott definition Coproduct (A : Type u) (B : Type v) := Sum A B infixl:65 " + " => Coproduct -attribute [eliminator] Sum.casesOn +attribute [induction_eliminator] Sum.casesOn namespace Coproduct variable {A : Type u} {B : Type v} @@ -44,7 +45,7 @@ namespace Coproduct hott definition decode {a₀ : A} : Π {x : A + B} (c : code a₀ x), inl a₀ = x | inl a, c => ap inl c - | inr b, c => Proto.Empty.elim c + | inr b, c => explode c hott statement decodeEncode {a₀ : A} {x : A + B} (p : inl a₀ = x) : decode (encode p) = p := @@ -78,7 +79,7 @@ namespace Coproduct Equiv.transport (code b₀) p (idp b₀) hott definition decode {b₀ : B} : Π {x : A + B} (c : code b₀ x), inr b₀ = x - | inl a, c => Proto.Empty.elim c + | inl a, c => explode c | inr b, c => ap inr c hott statement decodeEncode {b₀ : B} {x : A + B} @@ -111,8 +112,8 @@ namespace Coproduct hott definition pathSum {A B : Type u} (z₁ z₂ : A + B) (p : code z₁ z₂) : z₁ = z₂ := begin induction z₁ using Sum.casesOn <;> induction z₂ using Sum.casesOn; - apply ap; assumption; apply Proto.Empty.elim p; - apply Proto.Empty.elim p; apply ap; assumption + apply ap; assumption; apply explode p; + apply explode p; apply ap; assumption end end Coproduct diff --git a/GroundZero/Types/Ens.lean b/GroundZero/Types/Ens.lean index ad28aea..859d4dd 100644 --- a/GroundZero/Types/Ens.lean +++ b/GroundZero/Types/Ens.lean @@ -62,8 +62,8 @@ begin intro; apply id end hott lemma Ens.ssubset.trans {A : Type u} {a b c : Ens A} : a ⊆ b → b ⊆ c → a ⊆ c := λ G H x p, H x (G x p) -instance {A : Type u} : @Reflexive (Ens A) (· ⊆ ·) := ⟨Ens.ssubset.refl⟩ -instance {A : Type u} : @Transitive (Ens A) (· ⊆ ·) := ⟨@Ens.ssubset.trans A⟩ +instance {A : Type u} : @Reflexive (Ens A) Ens.ssubset := ⟨Ens.ssubset.refl⟩ +instance {A : Type u} : @Transitive (Ens A) Ens.ssubset := ⟨@Ens.ssubset.trans A⟩ hott definition Ens.parallel {A : Type u} (a b : Ens A) := a ∩ b ⊆ ∅ diff --git a/GroundZero/Types/Id.lean b/GroundZero/Types/Id.lean index db08fdb..ffa0494 100644 --- a/GroundZero/Types/Id.lean +++ b/GroundZero/Types/Id.lean @@ -16,7 +16,7 @@ end inductive Id {A : Type u} : A → A → Type u | idp (a : A) : Id a a -attribute [eliminator] Id.casesOn +attribute [induction_eliminator] Id.casesOn export Id (idp) infix:50 (priority := high) " = " => Id diff --git a/GroundZero/Types/Lost.lean b/GroundZero/Types/Lost.lean index 507b331..b6ea96e 100644 --- a/GroundZero/Types/Lost.lean +++ b/GroundZero/Types/Lost.lean @@ -1,4 +1,5 @@ import GroundZero.Types.Equiv +open GroundZero.Proto namespace GroundZero.Types @@ -7,7 +8,7 @@ universe u hott definition uninhabitedType {A : Type u} (f : A → 𝟎) : A ≃ 𝟎 := begin apply Sigma.mk f; apply Qinv.toBiinv; - apply Sigma.mk (@Proto.Empty.elim A); + apply Sigma.mk (@explode A); apply Prod.mk <;> intro x; induction x; induction f x end diff --git a/GroundZero/Types/Nat.lean b/GroundZero/Types/Nat.lean index 93d120b..0834fd8 100644 --- a/GroundZero/Types/Nat.lean +++ b/GroundZero/Types/Nat.lean @@ -2,6 +2,7 @@ import GroundZero.Structures open GroundZero.Types.Equiv (transport) open GroundZero.Types.Id (ap) +open GroundZero.Proto open GroundZero.Types open GroundZero @@ -73,8 +74,8 @@ transport (code m) p (r m) hott definition decode : Π {m n : ℕ}, code m n → m = n | Nat.zero, Nat.zero, p => idp 0 -| Nat.succ m, Nat.zero, p => Proto.Empty.elim p -| Nat.zero, Nat.succ n, p => Proto.Empty.elim p +| Nat.succ m, Nat.zero, p => explode p +| Nat.zero, Nat.succ n, p => explode p | Nat.succ m, Nat.succ n, p => ap Nat.succ (decode p) hott lemma decodeEncodeIdp : Π m, decode (encode (idp m)) = idp m @@ -86,8 +87,8 @@ begin induction p; apply decodeEncodeIdp end hott lemma encodeDecode : Π {m n : ℕ} (p : code m n), encode (decode p) = p | Nat.zero, Nat.zero, ★ => idp ★ -| Nat.succ m, Nat.zero, p => Proto.Empty.elim p -| Nat.zero, Nat.succ n, p => Proto.Empty.elim p +| Nat.succ m, Nat.zero, p => explode p +| Nat.zero, Nat.succ n, p => explode p | Nat.succ m, Nat.succ n, p => begin transitivity; symmetry; diff --git a/GroundZero/Types/Unit.lean b/GroundZero/Types/Unit.lean index 046cccf..509ca5b 100644 --- a/GroundZero/Types/Unit.lean +++ b/GroundZero/Types/Unit.lean @@ -6,7 +6,7 @@ universe u inductive Unit : Type u | star : Unit -attribute [eliminator] Unit.casesOn +attribute [induction_eliminator] Unit.casesOn notation "𝟏" => Unit notation "★" => Unit.star diff --git a/pictures/dependency-map.svg b/pictures/dependency-map.svg index 7d9ce3e..6ea4c5e 100644 --- a/pictures/dependency-map.svg +++ b/pictures/dependency-map.svg @@ -4,1462 +4,1462 @@ - + dependencyMap - + Algebra/Basic - -Algebra/Basic + +Algebra/Basic Algebra/Category - -Algebra/Category + +Algebra/Category Algebra/Basic->Algebra/Category - - + + Algebra/Geometry - -Algebra/Geometry + +Algebra/Geometry Algebra/Basic->Algebra/Geometry - - + + Algebra/Group/Basic - -Algebra/Group/Basic + +Algebra/Group/Basic Algebra/Basic->Algebra/Group/Basic - - + + Algebra/Monoid - -Algebra/Monoid + +Algebra/Monoid Algebra/Basic->Algebra/Monoid - - + + Algebra/Group/Automorphism - -Algebra/Group/Automorphism + +Algebra/Group/Automorphism Algebra/Group/Basic->Algebra/Group/Automorphism - - + + Algebra/EilenbergMacLane - -Algebra/EilenbergMacLane + +Algebra/EilenbergMacLane Algebra/Group/Basic->Algebra/EilenbergMacLane - - + + Algebra/Group/Absolutizer - -Algebra/Group/Absolutizer + +Algebra/Group/Absolutizer Algebra/Group/Basic->Algebra/Group/Absolutizer - - + + Algebra/Group/Finite - -Algebra/Group/Finite + +Algebra/Group/Finite Algebra/Group/Basic->Algebra/Group/Finite - - + + Algebra/Group/Free - -Algebra/Group/Free + +Algebra/Group/Free Algebra/Group/Basic->Algebra/Group/Free - - + + Algebra/Group/Homotopy - -Algebra/Group/Homotopy + +Algebra/Group/Homotopy Algebra/Group/Basic->Algebra/Group/Homotopy - - + + Algebra/Group/Periodic - -Algebra/Group/Periodic + +Algebra/Group/Periodic Algebra/Group/Basic->Algebra/Group/Periodic - - + + Algebra/Group/Product - -Algebra/Group/Product + +Algebra/Group/Product Algebra/Group/Basic->Algebra/Group/Product - - + + Algebra/Group/Subgroup - -Algebra/Group/Subgroup + +Algebra/Group/Subgroup Algebra/Group/Basic->Algebra/Group/Subgroup - - + + Algebra/Group/Action - -Algebra/Group/Action + +Algebra/Group/Action Algebra/Transformational - -Algebra/Transformational + +Algebra/Transformational Algebra/Group/Action->Algebra/Transformational - - + + Algebra/Group/Semidirect - -Algebra/Group/Semidirect + +Algebra/Group/Semidirect Algebra/Group/Automorphism->Algebra/Group/Semidirect - - + + Algebra/Group/Presentation - -Algebra/Group/Presentation + +Algebra/Group/Presentation Algebra/Group/Free->Algebra/Group/Presentation - - + + Algebra/Group/Product->Algebra/Transformational - - + + Algebra/Group/Factor - -Algebra/Group/Factor + +Algebra/Group/Factor Algebra/Group/Subgroup->Algebra/Group/Factor - - + + Algebra/Group/Differential - -Algebra/Group/Differential + +Algebra/Group/Differential Algebra/Group/Subgroup->Algebra/Group/Differential - - + + Algebra/Group/Lemmas - -Algebra/Group/Lemmas + +Algebra/Group/Lemmas Algebra/Group/Subgroup->Algebra/Group/Lemmas - - + + Algebra/Group/Symmetric - -Algebra/Group/Symmetric + +Algebra/Group/Symmetric Algebra/Group/Subgroup->Algebra/Group/Symmetric - - + + Algebra/Group/Alternating - -Algebra/Group/Alternating + +Algebra/Group/Alternating Algebra/Group/Factor->Algebra/Group/Alternating - - + + Algebra/Group/Isomorphism - -Algebra/Group/Isomorphism + +Algebra/Group/Isomorphism Algebra/Group/Factor->Algebra/Group/Isomorphism - - + + Algebra/Ring - -Algebra/Ring + +Algebra/Ring Algebra/Group/Factor->Algebra/Ring - - + + Algebra/Group/Isomorphism->Algebra/Group/Presentation - - + + Algebra/Orgraph - -Algebra/Orgraph + +Algebra/Orgraph Algebra/Ring->Algebra/Orgraph - - + + Algebra/Boolean - -Algebra/Boolean + +Algebra/Boolean Algebra/Ring->Algebra/Boolean - - + + Algebra/Group/Symmetric->Algebra/Group/Action - - + + Algebra/Group/Symmetric->Algebra/Group/Isomorphism - - + + Algebra/Group/Limited - -Algebra/Group/Limited + +Algebra/Group/Limited Algebra/Group/Symmetric->Algebra/Group/Limited - - + + Algebra/Group/Z - -Algebra/Group/Z + +Algebra/Group/Z Algebra/Group/Symmetric->Algebra/Group/Z - - + + Algebra/Reals - -Algebra/Reals + +Algebra/Reals Algebra/Orgraph->Algebra/Reals - - + + Algebra/Reals->Algebra/Group/Limited - - + + HITs/Topologization - -HITs/Topologization + +HITs/Topologization Algebra/Reals->HITs/Topologization - - + + Cubical/Path - -Cubical/Path + +Cubical/Path Cubical/Connection - -Cubical/Connection + +Cubical/Connection Cubical/Path->Cubical/Connection - - + + Cubical/V - -Cubical/V + +Cubical/V Cubical/Path->Cubical/V - - + + Cubical/Example - -Cubical/Example + +Cubical/Example Cubical/V->Cubical/Example - - + + Exercises/Chap1 - -Exercises/Chap1 + +Exercises/Chap1 Exercises/Chap3 - -Exercises/Chap3 + +Exercises/Chap3 Exercises/Chap1->Exercises/Chap3 - - + + Exercises/Chap2 - -Exercises/Chap2 + +Exercises/Chap2 Exercises/Chap4 - -Exercises/Chap4 + +Exercises/Chap4 Exercises/Chap2->Exercises/Chap4 - - + + Exercises/Chap5 - -Exercises/Chap5 + +Exercises/Chap5 Exercises/Chap4->Exercises/Chap5 - - + + HITs/Circle - -HITs/Circle + +HITs/Circle HITs/Circle->Algebra/Group/Z - - + + HITs/Circle->Exercises/Chap4 - - + + HITs/Moebius - -HITs/Moebius + +HITs/Moebius HITs/Circle->HITs/Moebius - - + + HITs/Reals - -HITs/Reals + +HITs/Reals HITs/Circle->HITs/Reals - - + + HITs/Sphere - -HITs/Sphere + +HITs/Sphere HITs/Circle->HITs/Sphere - - + + Theorems/Hopf - -Theorems/Hopf + +Theorems/Hopf HITs/Circle->Theorems/Hopf - - + + Types/CellComplex - -Types/CellComplex + +Types/CellComplex HITs/Sphere->Types/CellComplex - - + + HITs/Coequalizer - -HITs/Coequalizer + +HITs/Coequalizer HITs/Flattening - -HITs/Flattening + +HITs/Flattening HITs/Coequalizer->HITs/Flattening - - + + HITs/Colimit - -HITs/Colimit + +HITs/Colimit HITs/Merely - -HITs/Merely + +HITs/Merely HITs/Colimit->HITs/Merely - - + + Theorems/Equiv - -Theorems/Equiv + +Theorems/Equiv HITs/Merely->Theorems/Equiv - - + + HITs/Simplicial - -HITs/Simplicial + +HITs/Simplicial HITs/Merely->HITs/Simplicial - - + + HITs/Trunc - -HITs/Trunc + +HITs/Trunc HITs/Merely->HITs/Trunc - - + + Theorems/Functions - -Theorems/Functions + +Theorems/Functions HITs/Merely->Theorems/Functions - - + + HITs/Generalized - -HITs/Generalized + +HITs/Generalized HITs/Generalized->HITs/Merely - - + + HITs/Interval - -HITs/Interval + +HITs/Interval HITs/Interval->Cubical/Path - - + + Cubical/Cubes - -Cubical/Cubes + +Cubical/Cubes HITs/Interval->Cubical/Cubes - - + + HITs/Interval->Theorems/Equiv - - + + Theorems/Fibration - -Theorems/Fibration + +Theorems/Fibration HITs/Interval->Theorems/Fibration - - + + Theorems/Equiv->Exercises/Chap3 - - + + Theorems/Equiv->Exercises/Chap4 - - + + Theorems/Pullback - -Theorems/Pullback + +Theorems/Pullback Theorems/Equiv->Theorems/Pullback - - + + Theorems/Univalence - -Theorems/Univalence + +Theorems/Univalence Theorems/Equiv->Theorems/Univalence - - + + Types/Precategory - -Types/Precategory + +Types/Precategory Theorems/Equiv->Types/Precategory - - + + Theorems/Fibration->Theorems/Hopf - - + + HITs/Trunc->Algebra/Monoid - - + + HITs/Trunc->Algebra/EilenbergMacLane - - + + HITs/Trunc->Algebra/Group/Homotopy - - + + HITs/Trunc->HITs/Sphere - - + + HITs/Setquot - -HITs/Setquot + +HITs/Setquot HITs/Trunc->HITs/Setquot - - + + Theorems/Connectedness - -Theorems/Connectedness + +Theorems/Connectedness HITs/Trunc->Theorems/Connectedness - - + + Theorems/Functions->Exercises/Chap4 - - + + Modal/Etale - -Modal/Etale + +Modal/Etale Theorems/Functions->Modal/Etale - - + + Theorems/Functions->Theorems/Univalence - - + + Theorems/Functions->Types/Precategory - - + + HITs/Pushout - -HITs/Pushout + +HITs/Pushout HITs/Suspension - -HITs/Suspension + +HITs/Suspension HITs/Pushout->HITs/Suspension - - + + HITs/Wedge - -HITs/Wedge + +HITs/Wedge HITs/Pushout->HITs/Wedge - - + + HITs/Suspension->Algebra/EilenbergMacLane - - + + HITs/Suspension->HITs/Circle - - + + HITs/Join - -HITs/Join + +HITs/Join HITs/Suspension->HITs/Join - - + + HITs/Quotient - -HITs/Quotient + +HITs/Quotient HITs/Quotient->HITs/Coequalizer - - + + HITs/Quotient->HITs/Colimit - - + + HITs/Quotient->HITs/Generalized - - + + HITs/Quotient->HITs/Pushout - - + + HITs/Setquot->Algebra/Group/Action - - + + HITs/Setquot->Algebra/Group/Absolutizer - - + + HITs/Setquot->Algebra/Group/Factor - - + + Meta/Basic - -Meta/Basic + +Meta/Basic Proto - -Proto + +Proto Meta/Basic->Proto - - + + Theorems/Ontological - -Theorems/Ontological + +Theorems/Ontological Proto->Theorems/Ontological - - + + Types/Id - -Types/Id + +Types/Id Proto->Types/Id - - + + Meta/HottTheory - -Meta/HottTheory + +Meta/HottTheory Meta/HottTheory->Meta/Basic - - + + Meta/Notation - -Meta/Notation + +Meta/Notation Meta/Notation->Meta/Basic - - + + Meta/Tactic - -Meta/Tactic + +Meta/Tactic Meta/Tactic->Meta/Basic - - + + Meta/Trust - -Meta/Trust + +Meta/Trust Types/Equiv - -Types/Equiv + +Types/Equiv Meta/Trust->Types/Equiv - - + + Modal/Infinitesimal - -Modal/Infinitesimal + +Modal/Infinitesimal Types/Equiv->Modal/Infinitesimal - - + + Types/Coproduct - -Types/Coproduct + +Types/Coproduct Types/Equiv->Types/Coproduct - - + + Types/HEq - -Types/HEq + +Types/HEq Types/Equiv->Types/HEq - - + + Types/Lost - -Types/Lost + +Types/Lost Types/Equiv->Types/Lost - - + + Types/Sigma - -Types/Sigma + +Types/Sigma Types/Equiv->Types/Sigma - - + + Types/Unit - -Types/Unit + +Types/Unit Types/Equiv->Types/Unit - - + + Modal/Disc - -Modal/Disc + +Modal/Disc Modal/Disc->Modal/Etale - - + + Modal/Infinitesimal->Modal/Disc - - + + Types/Id->Meta/Trust - - + + Structures - -Structures + +Structures Structures->HITs/Merely - - + + Structures->HITs/Interval - - + + Structures->Modal/Disc - - + + Theorems/Weak - -Theorems/Weak + +Theorems/Weak Structures->Theorems/Weak - - + + Types/Nat - -Types/Nat + +Types/Nat Structures->Types/Nat - - + + Theorems/Nat - -Theorems/Nat + +Theorems/Nat Types/Nat->Theorems/Nat - - + + Theorems/Classical - -Theorems/Classical + +Theorems/Classical Theorems/Classical->Algebra/Category - - + + Theorems/Classical->Algebra/Orgraph - - + + Theorems/Pullback->Exercises/Chap2 - - + + Theorems/Univalence->Cubical/V - - + + Theorems/Univalence->Exercises/Chap2 - - + + Theorems/Univalence->HITs/Circle - - + + Theorems/Univalence->HITs/Flattening - - + + Theorems/Univalence->Theorems/Connectedness - - + + Theorems/Univalence->Theorems/Classical - - + + Theorems/Univalence->Theorems/Nat - - + + Types/Ens - -Types/Ens + +Types/Ens Theorems/Univalence->Types/Ens - - + + Types/Category - -Types/Category + +Types/Category Types/Precategory->Types/Category - - + + Theorems/Funext - -Theorems/Funext + +Theorems/Funext Types/Product - -Types/Product + +Types/Product Theorems/Funext->Types/Product - - + + Types/Product->Exercises/Chap1 - - + + Types/Product->Exercises/Chap4 - - + + Types/Product->Structures - - + + Theorems/Nat->Algebra/Group/Finite - - + + Theorems/Nat->Algebra/Group/Lemmas - - + + Theorems/Nat->Algebra/Reals - - + + Theorems/Nat->Exercises/Chap1 - - + + Theorems/Nat->Exercises/Chap4 - - + + HITs/Int - -HITs/Int + +HITs/Int Theorems/Nat->HITs/Int - - + + Types/Integer - -Types/Integer + +Types/Integer Theorems/Nat->Types/Integer - - + + Types/Integer->HITs/Circle - - + + Types/Ens->Algebra/Basic - - + + Types/Setquot - -Types/Setquot + +Types/Setquot Types/Ens->Types/Setquot - - + + Types/Coproduct->Structures - - + + Types/HEq->HITs/Quotient - - + + Types/HEq->Theorems/Funext - - + + Types/Lost->Exercises/Chap3 - - + + Types/Lost->Exercises/Chap5 - - + + Types/Sigma->Exercises/Chap1 - - + + Types/Sigma->Exercises/Chap4 - - + + Types/Sigma->Structures - - + + Types/Unit->HITs/Suspension - - + + Types/Unit->HITs/Wedge - - + + Types/Unit->Structures - - + +