From f6903abe8bf860fa2ad914729677a7d40263f513 Mon Sep 17 00:00:00 2001 From: Siegmentation Fault Date: Tue, 26 Dec 2023 14:40:34 +0700 Subject: [PATCH] clean up --- GroundZero/Theorems/Classical.lean | 26 ++++++------- GroundZero/Theorems/Equiv.lean | 52 +++++++++++++------------- GroundZero/Theorems/Fibration.lean | 36 +++++++++--------- GroundZero/Theorems/Functions.lean | 45 ++++++++++++----------- GroundZero/Theorems/Pullback.lean | 4 +- GroundZero/Theorems/Univalence.lean | 36 +++++++++--------- GroundZero/Types/Category.lean | 40 +++++++++++--------- GroundZero/Types/Coproduct.lean | 35 +++++++++--------- GroundZero/Types/Ens.lean | 57 +++++++++++++++-------------- GroundZero/Types/HEq.lean | 12 +++--- 10 files changed, 175 insertions(+), 168 deletions(-) diff --git a/GroundZero/Theorems/Classical.lean b/GroundZero/Theorems/Classical.lean index 6128325..817ed11 100644 --- a/GroundZero/Theorems/Classical.lean +++ b/GroundZero/Theorems/Classical.lean @@ -15,7 +15,7 @@ axiom choice {A : Type u} (B : A → Type v) (η : Π x, B x → Type w) : (Π (x : A), ∥(Σ (y : B x), η x y)∥) → ∥(Σ (φ : Π x, B x), Π x, η x (φ x))∥ -noncomputable hott def choiceOfRel {A : Type u} {B : Type v} +noncomputable hott lemma choiceOfRel {A : Type u} {B : Type v} (R : A → B → Prop w) (H : hset A) (G : hset B) : (Π x, ∥(Σ y, (R x y).fst)∥) → ∥(Σ (φ : A → B), Π x, (R x (φ x)).fst)∥ := begin @@ -25,7 +25,7 @@ begin { intros x y; apply (R x y).2 } end -noncomputable hott def cartesian {A : Type u} (B : A → Type v) : +noncomputable hott theorem cartesian {A : Type u} (B : A → Type v) : hset A → (Π x, hset (B x)) → (Π x, ∥B x∥) → ∥(Π x, B x)∥ := begin intros p q φ; apply transport; apply ua; @@ -40,9 +40,9 @@ end section variable {A : Type u} (H : prop A) - def inh := Σ (φ : 𝟐 → Prop), ∥(Σ (x : 𝟐), (φ x).fst)∥ + hott definition inh := Σ (φ : 𝟐 → Prop), ∥(Σ (x : 𝟐), (φ x).fst)∥ - noncomputable hott def inh.hset : hset inh := + noncomputable hott lemma inh.hset : hset inh := begin apply hsetRespectsSigma; apply piHset; intro x; apply Theorems.Equiv.propsetIsSet; @@ -50,7 +50,7 @@ section end -- due to http://www.cs.ioc.ee/ewscs/2017/altenkirch/altenkirch-notes.pdf - noncomputable hott def lem {A : Type u} (H : prop A) : A + ¬A := + noncomputable hott theorem lem {A : Type u} (H : prop A) : A + ¬A := begin have f := @choiceOfRel inh 𝟐 (λ φ x, φ.fst x) inh.hset boolIsSet (λ x, HITs.Merely.lift id x.2); induction f; case elemπ w => @@ -79,34 +79,34 @@ section end end -noncomputable hott def dneg.decode {A : Type u} (H : prop A) : ¬¬A → A := +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 φ) -hott def dneg.encode {A : Type u} : A → ¬¬A := +hott definition dneg.encode {A : Type u} : A → ¬¬A := λ x p, p x -noncomputable hott def dneg {A : Type u} (H : prop A) : A ≃ ¬¬A := +noncomputable hott definition dneg {A : Type u} (H : prop A) : A ≃ ¬¬A := propEquivLemma H notIsProp dneg.encode (dneg.decode H) section variable {A : Type u} {B : Type v} (H : prop B) - hott def Contrapos.intro : (A → B) → (¬B → ¬A) := + hott definition Contrapos.intro : (A → B) → (¬B → ¬A) := λ f p a, p (f a) - noncomputable hott def Contrapos.elim : (¬B → ¬A) → (A → B) := + 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) - noncomputable hott def Contrapos : (A → B) ↔ (¬B → ¬A) := + noncomputable hott definition Contrapos : (A → B) ↔ (¬B → ¬A) := ⟨Contrapos.intro, Contrapos.elim H⟩ - noncomputable hott def Contrapos.eq (H : prop B) : (A → B) = (¬B → ¬A) := + noncomputable hott definition Contrapos.eq (H : prop B) : (A → B) = (¬B → ¬A) := begin - apply GroundZero.ua; apply propEquivLemma; + apply ua; apply propEquivLemma; apply piProp; intro; assumption; apply piProp; intro; apply notIsProp; apply Contrapos.intro; apply Contrapos.elim H diff --git a/GroundZero/Theorems/Equiv.lean b/GroundZero/Theorems/Equiv.lean index 7ba6baf..36717ac 100644 --- a/GroundZero/Theorems/Equiv.lean +++ b/GroundZero/Theorems/Equiv.lean @@ -20,17 +20,17 @@ propIsSet HITs.Merely.uniq _ _ _ _ hott lemma propEquiv {A : Type u} (H : prop A) : A ≃ ∥A∥ := propEquivLemma H HITs.Merely.uniq HITs.Merely.elem (HITs.Merely.rec H id) -hott def propFromEquiv {A : Type u} : A ≃ ∥A∥ → prop A := +hott lemma propFromEquiv {A : Type u} : A ≃ ∥A∥ → prop A := begin intro ⟨f, (⟨g, A⟩, _)⟩ a b; transitivity; exact (A a)⁻¹; symmetry; transitivity; exact (A b)⁻¹; apply ap g; exact HITs.Merely.uniq (f b) (f a) end -hott def hmtpyRewrite {A : Type u} (f : A → A) (H : f ~ id) (x : A) : H (f x) = ap f (H x) := +hott definition hmtpyRewrite {A : Type u} (f : A → A) (H : f ~ id) (x : A) : H (f x) = ap f (H x) := begin have p := (Theorems.funext H)⁻¹; induction p; symmetry; apply Equiv.idmap end -hott def qinvImplsIshae {A : Type u} {B : Type v} (f : A → B) : qinv f → ishae f := +hott theorem qinvImplsIshae {A : Type u} {B : Type v} (f : A → B) : qinv f → ishae f := begin intro ⟨g, ⟨ε, η⟩⟩; let ε' := λ b, (ε (f (g b)))⁻¹ ⬝ (ap f (η (g b)) ⬝ ε b); existsi g; existsi η; existsi ε'; intro x; symmetry; transitivity; @@ -39,21 +39,21 @@ begin symmetry; apply @homotopySquare A B (f ∘ g ∘ f) f (λ x, ε (f x)) (g (f x)) x (η x) end -hott def respectsEquivOverFst {A : Type u} {B : Type v} +hott corollary respectsEquivOverFst {A : Type u} {B : Type v} (φ : A ≃ B) (C : A → Type w) : (Σ x, C x) ≃ (Σ x, C (φ.left x)) := begin fapply Sigma.replaceIshae; apply qinvImplsIshae; existsi φ.1; apply Prod.mk; apply φ.leftForward; apply φ.forwardLeft end -hott def fibEq {A : Type u} {B : Type v} (f : A → B) {y : B} {a b : A} - (p : f a = y) (q : f b = y) : (Σ (γ : a = b), ap f γ ⬝ q = p) → @Id (fib f y) ⟨a, p⟩ ⟨b, q⟩ := +hott definition fibEq {A : Type u} {B : Type v} (f : A → B) {y : B} {a b : A} (p : f a = y) (q : f b = y) : + (Σ (γ : a = b), ap f γ ⬝ q = p) → @Id (fib f y) ⟨a, p⟩ ⟨b, q⟩ := begin intro ⟨γ, r⟩; fapply Sigma.prod; exact γ; transitivity; apply transportOverContrMap; transitivity; apply ap (· ⬝ p); apply Id.mapInv; apply rewriteComp; exact r⁻¹ end -hott def ishaeImplContrFib {A : Type u} {B : Type v} +hott theorem ishaeImplContrFib {A : Type u} {B : Type v} (f : A → B) : ishae f → Π y, contr (fib f y) := begin intro ⟨g, η, ε, τ⟩ y; existsi ⟨g y, ε y⟩; intro ⟨x, p⟩; apply fibEq; @@ -67,7 +67,7 @@ begin symmetry; apply idmap; apply homotopySquare end -hott def compQinv₁ {A : Type u} {B : Type v} {C : Type w} +hott lemma compQinv₁ {A : Type u} {B : Type v} {C : Type w} (f : A → B) (g : B → A) (H : isQinv f g) : @qinv (C → A) (C → B) (f ∘ ·) := begin @@ -75,7 +75,7 @@ begin apply Theorems.funext <;> intro; apply H.1; apply H.2 end -hott def compQinv₂ {A : Type u} {B : Type v} {C : Type w} +hott lemma compQinv₂ {A : Type u} {B : Type v} {C : Type w} (f : A → B) (g : B → A) (H : isQinv f g) : @qinv (B → C) (A → C) (· ∘ f) := begin @@ -127,24 +127,24 @@ begin intro x; apply HITs.Merely.uniq } end -hott def lemContrInv {A : Type u} (h : prop A) (x : A) : contr A := ⟨x, h x⟩ +hott lemma lemContrInv {A : Type u} (H : prop A) (x : A) : contr A := ⟨x, H x⟩ -hott def lemContrEquiv {A : Type u} : (prop A) ≃ (A → contr A) := +hott proposition lemContrEquiv {A : Type u} : (prop A) ≃ (A → contr A) := begin apply propEquivLemma; apply propIsProp; apply functionToContr; apply lemContrInv; apply lemContr end -hott def contrToType {A : Type u} {B : A → Type v} +hott definition contrToType {A : Type u} {B : A → Type v} (H : contr A) : (Σ x, B x) → B H.1 := λ w, transport B (H.2 w.1)⁻¹ w.2 -hott def typeToContr {A : Type u} {B : A → Type v} +hott definition typeToContr {A : Type u} {B : A → Type v} (H : contr A) : B H.1 → (Σ x, B x) := λ u, ⟨H.1, u⟩ -- HoTT 3.20 -hott def contrFamily {A : Type u} {B : A → Type v} (H : contr A) : (Σ x, B x) ≃ B H.1 := +hott theorem contrFamily {A : Type u} {B : A → Type v} (H : contr A) : (Σ x, B x) ≃ B H.1 := begin existsi contrToType H; apply Prod.mk <;> existsi @typeToContr A B H <;> intro x; @@ -154,36 +154,36 @@ begin reflexivity } end -hott def propset.Id (A B : Prop) (H : A.1 = B.1) : A = B := +hott lemma propset.Id (A B : Prop) (H : A.1 = B.1) : A = B := Sigma.prod H (propIsProp _ _) -hott def hsetEquiv {A : Type u} {B : Type v} (g : hset B) : hset (A ≃ B) := +hott corollary hsetEquiv {A : Type u} {B : Type v} (g : hset B) : hset (A ≃ B) := begin fapply hsetRespectsSigma; { apply piHset; intro x; assumption }; { intro x; apply propIsSet; apply biinvProp } end -hott def zeroEquiv.hset (A B : 0-Type) : hset (A ≃₀ B) := +hott corollary zeroEquiv.hset (A B : 0-Type) : hset (A ≃₀ B) := begin apply hsetEquiv; apply zeroEqvSet.forward; exact B.2 end -hott def contrQinvFib {A : Type u} {B : Type v} {f : A → B} (e : qinv f) (b : B) : contr (Σ a, b = f a) := +hott lemma contrQinvFib {A : Type u} {B : Type v} {f : A → B} (e : qinv f) (b : B) : contr (Σ a, b = f a) := begin apply contrRespectsEquiv; apply respectsEquivOverFst (Qinv.toEquiv (Qinv.sym e)) (Id b); apply singl.contr end -hott def propQinvFib {A : Type u} {B : Type v} {f : A → B} (e : qinv f) (b : B) : prop (Σ a, b = f a) := +hott lemma propQinvFib {A : Type u} {B : Type v} {f : A → B} (e : qinv f) (b : B) : prop (Σ a, b = f a) := contrImplProp (contrQinvFib e b) -hott def corrRev {A : Type u} {B : Type v} : Corr A B → Corr B A := +hott definition corrRev {A : Type u} {B : Type v} : Corr A B → Corr B A := λ w, ⟨λ a b, w.1 b a, (w.2.2, w.2.1)⟩ -hott def corrOfQinv {A : Type u} {B : Type v} : (Σ f, @qinv A B f) → Corr A B := +hott definition corrOfQinv {A : Type u} {B : Type v} : (Σ f, @qinv A B f) → Corr A B := begin intro w; existsi (λ a b, b = w.1 a); apply Prod.mk <;> intros; apply contrRespectsEquiv; apply Sigma.hmtpyInvEqv; apply singl.contr; apply contrQinvFib; exact w.2 end -hott def qinvOfCorr {A : Type u} {B : Type v} : Corr A B → (Σ f, @qinv A B f) := +hott definition qinvOfCorr {A : Type u} {B : Type v} : Corr A B → (Σ f, @qinv A B f) := begin intro w; fapply Sigma.mk; intro a; apply (w.2.1 a).1.1; fapply Sigma.mk; intro b; apply (w.2.2 b).1.1; apply Prod.mk; @@ -198,10 +198,10 @@ section example : (qinvOfCorr (corrOfQinv e)).2.1 = e.2.1 := by reflexivity end -hott def pathOver {A : Type u} (B : A → Type v) {a b : A} (p : a = b) (u : B a) (v : B b) := +hott definition pathOver {A : Type u} (B : A → Type v) {a b : A} (p : a = b) (u : B a) (v : B b) := Σ (φ : Π x y, x = y → B x → B y), φ a b p u = v × Π x, φ x x (idp x) ~ idfun -hott def pathOverCharacterization {A : Type u} {B : A → Type v} {a b : A} +hott theorem pathOverCharacterization {A : Type u} {B : A → Type v} {a b : A} (p : a = b) (u : B a) (v : B b) : (u =[p] v) ≃ pathOver B p u v := begin fapply Sigma.mk; { intro q; existsi @transport A B; apply Prod.mk; exact q; intro; apply idp }; @@ -231,7 +231,7 @@ begin { induction p; reflexivity } end -hott def replaceIshaeUnderPi {A : Type u} {B : Type v} {C : A → Type w} +hott theorem replaceIshaeUnderPi {A : Type u} {B : Type v} {C : A → Type w} (g : B → A) (e : ishae g) : (Π x, C x) ≃ (Π x, C (g x)) := begin fapply Sigma.mk; intro φ x; exact φ (g x); fapply Qinv.toBiinv; @@ -242,7 +242,7 @@ begin { intro φ; apply Theorems.funext; intro; apply apd } end -hott def replaceQinvUnderPi {A : Type u} {B : Type v} {C : A → Type w} +hott corollary replaceQinvUnderPi {A : Type u} {B : Type v} {C : A → Type w} (g : B → A) : qinv g → (Π x, C x) ≃ (Π x, C (g x)) := replaceIshaeUnderPi g ∘ qinvImplsIshae g diff --git a/GroundZero/Theorems/Fibration.lean b/GroundZero/Theorems/Fibration.lean index b7d0a07..52c8278 100644 --- a/GroundZero/Theorems/Fibration.lean +++ b/GroundZero/Theorems/Fibration.lean @@ -6,39 +6,39 @@ open GroundZero.Structures namespace GroundZero.Theorems.Fibration universe u v - hott def forward {A : Type u} {B : A → Type v} (x : A) : - Types.fib (@Sigma.fst A B) x → B x := + hott definition forward {A : Type u} {B : A → Type v} (x : A) : + fib (@Sigma.fst A B) x → B x := λ ⟨⟨y, u⟩, H⟩, transport B H u - hott def left {A : Type u} {B : A → Type v} (x : A) (u : B x) : - Types.fib (@Sigma.fst A B) x := + hott definition left {A : Type u} {B : A → Type v} (x : A) (u : B x) : + fib (@Sigma.fst A B) x := ⟨⟨x, u⟩, idp _⟩ - hott def fiberOver {A : Type u} {B : A → Type v} (x : A) : - Types.fib (@Sigma.fst A B) x ≃ B x := + hott definition fiberOver {A : Type u} {B : A → Type v} (x : A) : + fib (@Sigma.fst A B) x ≃ B x := begin existsi forward x; apply Prod.mk <;> existsi (@left A B x); { intro ⟨⟨y, u⟩, (H : y = x)⟩; induction H; apply idp }; { intro; reflexivity } end - inductive leg {A : Type u} : A → Type u - | lam (f : I → A) : leg (f 0) + inductive Left {A : Type u} : A → Type u + | lam (f : I → A) : Left (f 0) - inductive post {A : Type u} : A → Type u - | lam (f : I → A) : post (f 1) + inductive Right {A : Type u} : A → Type u + | lam (f : I → A) : Right (f 1) - hott def liftingProperty {A : Type u} {B : Type v} (p : A → B) := - Π x, leg (p x) → leg x + hott definition hasLifting {A : Type u} {B : Type v} (f : A → B) := + Π x, Left (f x) → Left x - hott def Fibration (A : Type u) (B : Type v) := - Σ (p : A → B), liftingProperty p + hott definition Fibration (A : Type u) (B : Type v) := + Σ (f : A → B), hasLifting f infix:60 " ↠ " => Fibration - hott def lifting {A : Type u} {B : A → Type v} (f : I → A) (u : B (f 0)) : @leg (Sigma B) ⟨f 0, u⟩ := - @leg.lam (Sigma B) (λ i, ⟨f i, @Interval.ind (B ∘ f) u (transport (B ∘ f) seg u) (idp _) i⟩) + hott definition lifting {A : Type u} {B : A → Type v} (f : I → A) (u : B (f 0)) : @Left (Σ x, B x) ⟨f 0, u⟩ := + @Left.lam (Sigma B) (λ i, ⟨f i, transport (B ∘ f) (Interval.contrLeft i) u⟩) - hott def typeFamily {A : Type u} (B : A → Type v) : (Σ x, B x) ↠ A := - begin existsi Sigma.fst; intro ⟨x, u⟩ f; apply @leg.casesOn A (λ x f, Π u, @leg (Σ x, B x) ⟨x, u⟩) x f; apply lifting end + hott definition typeFamily {A : Type u} (B : A → Type v) : (Σ x, B x) ↠ A := + begin existsi Sigma.fst; intro ⟨x, u⟩ f; apply @Left.casesOn A (λ x f, Π u, @Left (Σ x, B x) ⟨x, u⟩) x f; apply lifting end end GroundZero.Theorems.Fibration diff --git a/GroundZero/Theorems/Functions.lean b/GroundZero/Theorems/Functions.lean index e5dfee7..1429325 100644 --- a/GroundZero/Theorems/Functions.lean +++ b/GroundZero/Theorems/Functions.lean @@ -7,28 +7,28 @@ open GroundZero.Structures namespace GroundZero.Theorems.Functions universe u v -hott def injective {A : Type u} {B : Type v} (f : A → B) := +hott definition injective {A : Type u} {B : Type v} (f : A → B) := Π x y, f x = f y → x = y -hott def surjective {A : Type u} {B : Type v} (f : A → B) := +hott definition surjective {A : Type u} {B : Type v} (f : A → B) := Π b, ∥Σ a, f a = b∥ -hott def Surjection (A : Type u) (B : Type v) := +hott definition Surjection (A : Type u) (B : Type v) := Σ (f : A → B), surjective f infixr:70 " ↠ " => Surjection instance (A : Type u) (B : Type v) : CoeFun (A ↠ B) (λ _, A → B) := ⟨Sigma.fst⟩ -hott def fibInh {A : Type u} {B : Type v} (f : A → B) := +hott definition fibInh {A : Type u} {B : Type v} (f : A → B) := λ b, ∥fib f b∥ -hott def Ran {A : Type u} {B : Type v} (f : A → B) := +hott definition Ran {A : Type u} {B : Type v} (f : A → B) := total (fibInh f) -hott def cut {A : Type u} {B : Type v} (f : A → B) : A → Ran f := +hott definition cut {A : Type u} {B : Type v} (f : A → B) : A → Ran f := λ x, ⟨f x, |⟨x, idp (f x)⟩|⟩ -hott def cutIsSurj {A : Type u} {B : Type v} (f : A → B) : surjective (cut f) := +hott lemma cutIsSurj {A : Type u} {B : Type v} (f : A → B) : surjective (cut f) := begin intro ⟨x, (H : ∥_∥)⟩; induction H; case elemπ G => @@ -37,23 +37,23 @@ begin apply Merely.uniq end -hott def Ran.subset {A : Type u} {B : Type v} (f : A → B) : Ran f → B := +hott definition Ran.subset {A : Type u} {B : Type v} (f : A → B) : Ran f → B := Sigma.fst -hott def Ran.incl {A : Type u} {B : Type v} {f : A → B} (H : surjective f) : B → Ran f := +hott definition Ran.incl {A : Type u} {B : Type v} {f : A → B} (H : surjective f) : B → Ran f := λ x, ⟨x, H x⟩ -hott def surjImplRanEqv {A : Type u} {B : Type v} (f : A → B) (H : surjective f) : Ran f ≃ B := +hott lemma surjImplRanEqv {A : Type u} {B : Type v} (f : A → B) (H : surjective f) : Ran f ≃ B := begin existsi Sigma.fst; fapply Prod.mk <;> existsi Ran.incl H; { intro ⟨_, _⟩; fapply Sigma.prod; reflexivity; apply Merely.uniq }; { intro; reflexivity } end -hott def ranConst {A : Type u} (a : A) {B : Type v} (b : B) : Ran (Function.const A b) := +hott definition ranConst {A : Type u} (a : A) {B : Type v} (b : B) : Ran (Function.const A b) := ⟨b, |⟨a, idp b⟩|⟩ -hott def ranConstEqv {A : Type u} (a : A) {B : Type v} +hott lemma ranConstEqv {A : Type u} (a : A) {B : Type v} (H : hset B) (b : B) : Ran (Function.const A b) ≃ 𝟏 := begin existsi (λ _, ★); fapply Prod.mk <;> existsi (λ _, ranConst a b); @@ -63,10 +63,10 @@ begin { intro ★; reflexivity } end -hott def isEmbedding {A : Type u} {B : Type v} (f : A → B) := +hott definition isEmbedding {A : Type u} {B : Type v} (f : A → B) := Π x y, @Equiv.biinv (x = y) (f x = f y) (ap f) -hott def Embedding (A : Type u) (B : Type v) := +hott definition Embedding (A : Type u) (B : Type v) := Σ (f : A → B), isEmbedding f infix:55 " ↪ " => Embedding @@ -74,27 +74,28 @@ infix:55 " ↪ " => Embedding section variable {A : Type u} {B : Type v} (f : A ↪ B) - def Embedding.ap : A → B := f.1 - def Embedding.eqv (x y : A) : (x = y) ≃ (f.ap x = f.ap y) := + hott abbreviation Embedding.ap : A → B := f.1 + + hott abbreviation Embedding.eqv (x y : A) : (x = y) ≃ (f.ap x = f.ap y) := ⟨Id.ap f.ap, f.2 x y⟩ end -hott def ntypeOverEmbedding {A : Type u} {B : Type v} (f : A ↪ B) (n : ℕ₋₂) : +hott theorem ntypeOverEmbedding {A : Type u} {B : Type v} (f : A ↪ B) (n : ℕ₋₂) : is-(hlevel.succ n)-type B → is-(hlevel.succ n)-type A := begin intros H x y; apply ntypeRespectsEquiv; apply Equiv.symm; existsi ap f.1; apply f.2; apply H end -hott def eqvMapForward {A : Type u} {B : Type v} (e : A ≃ B) +hott definition eqvMapForward {A : Type u} {B : Type v} (e : A ≃ B) (x y : A) (p : e x = e y) : x = y := (e.leftForward x)⁻¹ ⬝ (@ap B A _ _ e.left p) ⬝ (e.leftForward y) -hott def sigmaPropEq {A : Type u} {B : A → Type v} +hott lemma sigmaPropEq {A : Type u} {B : A → Type v} (H : Π x, prop (B x)) {x y : Sigma B} (p : x.1 = y.1) : x = y := begin fapply Sigma.prod; exact p; apply H end -hott def propSigmaEquiv {A : Type u} {B : A → Type v} (H : Π x, prop (B x)) +hott lemma propSigmaEquiv {A : Type u} {B : A → Type v} (H : Π x, prop (B x)) (x y : Σ x, B x) : (x = y) ≃ (x.1 = y.1) := begin apply Equiv.trans; apply Sigma.sigmaPath; @@ -104,7 +105,7 @@ begin apply Equiv.trans; apply Sigma.const; apply unitProdEquiv end -hott def propSigmaEmbedding {A : Type u} {B : A → Type v} +hott definition propSigmaEmbedding {A : Type u} {B : A → Type v} (H : Π x, prop (B x)) : (Σ x, B x) ↪ A := begin existsi Sigma.fst; intro x y; @@ -112,7 +113,7 @@ begin apply Theorems.funext; intro p; induction p; reflexivity end -hott def isConnected (A : Type u) := +hott definition isConnected (A : Type u) := Σ (x : A), Π y, ∥x = y∥ end GroundZero.Theorems.Functions diff --git a/GroundZero/Theorems/Pullback.lean b/GroundZero/Theorems/Pullback.lean index bfd60e6..fc1fa01 100644 --- a/GroundZero/Theorems/Pullback.lean +++ b/GroundZero/Theorems/Pullback.lean @@ -13,7 +13,7 @@ namespace GroundZero.Theorems section variable {P : Type k} {A : Type u} {B : Type v} {C : Type w} (η : hcommSquare P A B C) - hott def terminalPullback : pullback (𝟏 → C) (λ f, η.right ∘ f) (λ g, η.bot ∘ g) ≃ pullback C η.right η.bot := + hott lemma terminalPullback : pullback (𝟏 → C) (λ f, η.right ∘ f) (λ g, η.bot ∘ g) ≃ pullback C η.right η.bot := begin fapply Sigma.mk; { intro w; existsi (w.1.1 ★, w.1.2 ★); apply happly w.2 ★ }; apply Qinv.toBiinv; fapply Sigma.mk; { intro w; existsi (λ _, w.1.1, λ _, w.1.2); apply funext; intro; apply w.2 }; apply Prod.mk <;> intro w; @@ -27,7 +27,7 @@ end section variable {P : Type k} {A : Type u} {B : Type v} {C : Type w} (η : pullbackSquare P A B C) - hott def pullbackCorner : P ≃ pullback C η.1.right η.1.bot := + hott theorem pullbackCorner : P ≃ pullback C η.1.right η.1.bot := begin apply Equiv.trans; apply Structures.terminalArrow; apply Equiv.trans; fapply Sigma.mk; exact η.1.induced 𝟏; diff --git a/GroundZero/Theorems/Univalence.lean b/GroundZero/Theorems/Univalence.lean index e587a85..5dcc222 100644 --- a/GroundZero/Theorems/Univalence.lean +++ b/GroundZero/Theorems/Univalence.lean @@ -87,7 +87,7 @@ contrImplProp (univAlt A) namespace Equiv variable {C : Π (A B : Type u), A ≃ B → Type v} (Cidp : Π (A : Type u), C A A (ideqv A)) - noncomputable hott def J {A B : Type u} (e : A ≃ B) : C A B e := + 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 @@ -99,7 +99,7 @@ namespace Equiv end end Equiv -hott def isZero : ℕ → 𝟐 +hott definition isZero : ℕ → 𝟐 | Nat.zero => true | Nat.succ _ => false @@ -109,11 +109,11 @@ ffNeqTt (ap isZero h)⁻¹ hott lemma succNeqZero {n : ℕ} : ¬(Nat.succ n = 0) := λ h, ffNeqTt (ap isZero h) -hott def negNeg : Π x, not (not x) = x +hott definition negNeg : Π x, not (not x) = x | true => idp true | false => idp false -hott def negBoolEquiv : 𝟐 ≃ 𝟐 := +hott definition negBoolEquiv : 𝟐 ≃ 𝟐 := ⟨not, (⟨not, negNeg⟩, ⟨not, negNeg⟩)⟩ noncomputable hott theorem universeNotASet : ¬(hset Type) := @@ -157,11 +157,11 @@ end section variable {C : 𝟐 → Type u} - hott def familyOnBool.sec (w : C false × C true) : Π b, C b + hott definition familyOnBool.sec (w : C false × C true) : Π b, C b | false => w.1 | true => w.2 - hott def familyOnBool.ret (φ : Π b, C b) : C false × C true := + hott definition familyOnBool.ret (φ : Π b, C b) : C false × C true := (φ false, φ true) hott theorem familyOnBool : (C false × C true) ≃ Π b, C b := @@ -176,29 +176,29 @@ end namespace Theorems.Equiv -noncomputable hott def propEqProp {A B : Type u} (G : prop B) : prop (A = B) := +noncomputable hott definition propEqProp {A B : Type u} (G : prop B) : prop (A = B) := begin apply propRespectsEquiv.{u, u + 1}; apply Equiv.symm; apply univalence; apply propEquivProp G end -noncomputable hott def propsetIsSet : hset propset := +noncomputable hott theorem propsetIsSet : hset propset := begin intro ⟨x, H⟩ ⟨y, G⟩; apply transport (λ π, Π (p q : π), p = q); - symmetry; apply GroundZero.ua; apply Sigma.sigmaPath; + symmetry; apply ua; apply Sigma.sigmaPath; intro ⟨p, p'⟩ ⟨q, q'⟩; fapply Sigma.prod; { apply propEqProp; exact G }; { apply propIsSet; apply propIsProp } end -hott def bool.decode : 𝟐 ≃ 𝟐 → 𝟐 := +hott definition bool.decode : 𝟐 ≃ 𝟐 → 𝟐 := λ e, e false -hott def bool.encode : 𝟐 → 𝟐 ≃ 𝟐 +hott definition bool.encode : 𝟐 → 𝟐 ≃ 𝟐 | false => ideqv 𝟐 | true => negBoolEquiv -hott def boolEquivEqvBool : (𝟐 ≃ 𝟐) ≃ 𝟐 := +hott exercise boolEquivEqvBool : (𝟐 ≃ 𝟐) ≃ 𝟐 := begin existsi bool.decode; fapply Qinv.toBiinv; existsi bool.encode; apply Prod.mk; { intro x; induction x using Bool.casesOn <;> reflexivity }; @@ -221,13 +221,13 @@ end section variable {A : Type u} {B : Type v} - hott def corrOfBiinv : A ≃ B → Corr A B := + hott definition corrOfBiinv : A ≃ B → Corr A B := λ e, @corrOfQinv A B ⟨e.1, Qinv.ofBiinv e.1 e.2⟩ - hott def biinvOfCorr : Corr A B → A ≃ B := + hott definition biinvOfCorr : Corr A B → A ≃ B := λ c, Qinv.toEquiv (qinvOfCorr c).2 - hott def corrLem (R : A → B → Type w) (φ : A → B) (ρ : Π x, R x (φ x)) + hott lemma corrLem (R : A → B → Type w) (φ : A → B) (ρ : Π x, R x (φ x)) (H : Π x y, R x y → φ x = y) (c : Π (x : A) (y : B) (w : R x y), ρ x =[H x y w] w) (x : A) (y : B) : (φ x = y) ≃ (R x y) := begin @@ -239,7 +239,7 @@ section { intro p; induction p; apply Id.invComp } end - noncomputable hott def corrBiinvIdfun : corrOfBiinv ∘ @biinvOfCorr A B ~ idfun := + noncomputable hott lemma corrBiinvIdfun : corrOfBiinv ∘ @biinvOfCorr A B ~ idfun := begin intro w; fapply Sigma.prod; apply Theorems.funext; intro x; apply Theorems.funext; intro y; @@ -252,10 +252,10 @@ section apply productProp <;> { apply piProp; intros; apply contrIsProp } end - hott def biinvCorrIdfun : biinvOfCorr ∘ @corrOfBiinv A B ~ idfun := + hott proposition biinvCorrIdfun : biinvOfCorr ∘ @corrOfBiinv A B ~ idfun := begin intro e; fapply equivHmtpyLem; intro; reflexivity end - noncomputable hott def biinvEquivCorr : Corr A B ≃ (A ≃ B) := + noncomputable hott theorem biinvEquivCorr : Corr A B ≃ (A ≃ B) := begin existsi biinvOfCorr; fapply Qinv.toBiinv; existsi corrOfBiinv; apply Prod.mk; apply biinvCorrIdfun; apply corrBiinvIdfun diff --git a/GroundZero/Types/Category.lean b/GroundZero/Types/Category.lean index 94259c5..be9f492 100644 --- a/GroundZero/Types/Category.lean +++ b/GroundZero/Types/Category.lean @@ -5,47 +5,51 @@ open GroundZero.Structures namespace GroundZero.Types universe u v -def Category (A : Type u) := +hott definition Category (A : Type u) := Σ (𝒞 : Precategory A), Π a b, biinv (@Precategory.idtoiso A 𝒞 a b) namespace Category variable {A : Type u} (𝒞 : Category A) - def hom := 𝒞.1.hom - def set : Π (x y : A), hset (hom 𝒞 x y) := 𝒞.1.set + hott abbreviation hom := 𝒞.1.hom - def id : Π {a : A}, hom 𝒞 a a := 𝒞.1.id - def comp {A : Type u} {𝒞 : Category A} {a b c : A} + hott definition set : Π (x y : A), hset (hom 𝒞 x y) := 𝒞.1.set + + attribute [irreducible] set + + hott abbreviation id : Π {a : A}, hom 𝒞 a a := 𝒞.1.id + + hott abbreviation comp {A : Type u} {𝒞 : Category A} {a b c : A} (f : hom 𝒞 b c) (g : hom 𝒞 a b) : hom 𝒞 a c := 𝒞.1.comp f g - + local infix:60 " ∘ " => comp - def idLeft : Π {a b : A} (f : hom 𝒞 a b), f = id 𝒞 ∘ f := 𝒞.1.idLeft - def idRight : Π {a b : A} (f : hom 𝒞 a b), f = f ∘ id 𝒞 := 𝒞.1.idRight - def assoc : Π {a b c d : A} (f : hom 𝒞 a b) (g : hom 𝒞 b c) (h : hom 𝒞 c d), h ∘ (g ∘ f) = (h ∘ g) ∘ f := 𝒞.1.assoc + hott abbreviation idLeft : Π {a b : A} (f : hom 𝒞 a b), f = id 𝒞 ∘ f := 𝒞.1.idLeft + hott abbreviation idRight : Π {a b : A} (f : hom 𝒞 a b), f = f ∘ id 𝒞 := 𝒞.1.idRight + hott abbreviation assoc : Π {a b c d : A} (f : hom 𝒞 a b) (g : hom 𝒞 b c) (h : hom 𝒞 c d), h ∘ (g ∘ f) = (h ∘ g) ∘ f := 𝒞.1.assoc - def iso (a b : A) := Precategory.iso 𝒞.1 a b + hott abbreviation iso (a b : A) := Precategory.iso 𝒞.1 a b - hott def idtoiso {a b : A} : a = b → iso 𝒞 a b := + hott abbreviation idtoiso {a b : A} : a = b → iso 𝒞 a b := Precategory.idtoiso 𝒞.1 - hott def univalence {a b : A} : (a = b) ≃ (iso 𝒞 a b) := + hott definition univalence {a b : A} : (a = b) ≃ (iso 𝒞 a b) := ⟨idtoiso 𝒞, 𝒞.snd a b⟩ - hott def ua {a b : A} : iso 𝒞 a b → a = b := + hott definition ua {a b : A} : iso 𝒞 a b → a = b := (univalence 𝒞).left - hott def uaβrule₁ {a b : A} (φ : iso 𝒞 a b) : idtoiso 𝒞 (ua 𝒞 φ) = φ := + hott definition uaβrule₁ {a b : A} (φ : iso 𝒞 a b) : idtoiso 𝒞 (ua 𝒞 φ) = φ := (univalence 𝒞).forwardLeft φ - hott def uaβrule₂ {a b : A} (φ : a = b) : ua 𝒞 (idtoiso 𝒞 φ) = φ := + hott definition uaβrule₂ {a b : A} (φ : a = b) : ua 𝒞 (idtoiso 𝒞 φ) = φ := (univalence 𝒞).leftForward φ - def Mor {A : Type u} (𝒞 : Category A) := Σ (x y : A), hom 𝒞 x y + hott definition Mor {A : Type u} (𝒞 : Category A) := Σ (x y : A), hom 𝒞 x y - def twoOutOfThree {a b c : A} (g : hom 𝒞 b c) (f : hom 𝒞 a b) (K : Π (x y : A), hom 𝒞 x y → Type v) := + hott definition twoOutOfThree {a b c : A} (g : hom 𝒞 b c) (f : hom 𝒞 a b) (K : Π (x y : A), hom 𝒞 x y → Type v) := (K a b f → K b c g → K a c (g ∘ f)) × (K a c (g ∘ f) → K b c g → K a b f) × (K a b f → K a c (g ∘ f) → K b c g) end Category -end GroundZero.Types \ No newline at end of file +end GroundZero.Types diff --git a/GroundZero/Types/Coproduct.lean b/GroundZero/Types/Coproduct.lean index 6f34dbe..c956a17 100644 --- a/GroundZero/Types/Coproduct.lean +++ b/GroundZero/Types/Coproduct.lean @@ -5,7 +5,8 @@ open GroundZero.Types.Id (ap) namespace GroundZero.Types universe u v w w' -def Coproduct (A : Type u) (B : Type v) := Sum A B +hott definition Coproduct (A : Type u) (B : Type v) := Sum A B + infixl:65 " + " => Coproduct attribute [eliminator] Sum.casesOn @@ -13,35 +14,35 @@ attribute [eliminator] Sum.casesOn namespace Coproduct variable {A : Type u} {B : Type v} - @[match_pattern] def inl : A → A + B := Sum.inl - @[match_pattern] def inr : B → A + B := Sum.inr + @[match_pattern] hott abbreviation inl : A → A + B := Sum.inl + @[match_pattern] hott abbreviation inr : B → A + B := Sum.inr - hott def elim {C : Type w} (g₀ : A → C) (g₁ : B → C) : A + B → C + hott definition elim {C : Type w} (g₀ : A → C) (g₁ : B → C) : A + B → C | inl a => g₀ a | inr b => g₁ b - hott def bimap {C : Type w} {C' : Type w'} (f : A → C) (g : B → C') : A + B → C + C' := + hott definition bimap {C : Type w} {C' : Type w'} (f : A → C) (g : B → C') : A + B → C + C' := elim (Sum.inl ∘ f) (Sum.inr ∘ g) - hott def inv : A + B → B + A + hott definition inv : A + B → B + A | inl x => inr x | inr x => inl x - hott def symm : A + B ≃ B + A := + hott definition symm : A + B ≃ B + A := begin existsi inv; apply Qinv.toBiinv; existsi inv; apply Prod.mk <;> { intro x; induction x using Sum.casesOn <;> reflexivity } end namespace inl - hott def code (a₀ : A) : A + B → Type u + hott definition code (a₀ : A) : A + B → Type u | inl a => a₀ = a | inr b => 𝟎 - hott def encode {a₀ : A} {x : A + B} (p : inl a₀ = x) : code a₀ x := + hott definition encode {a₀ : A} {x : A + B} (p : inl a₀ = x) : code a₀ x := Equiv.transport (code a₀) p (idp a₀) - hott def decode {a₀ : A} : Π {x : A + B} (c : code a₀ x), inl a₀ = x + 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 @@ -61,22 +62,22 @@ namespace Coproduct apply Prod.mk; apply encodeDecode; apply decodeEncode end - hott def inj' (x y : A) : @Id (A + B) (inl x) (inl y) ≃ (x = y) := + hott corollary inj' (x y : A) : @Id (A + B) (inl x) (inl y) ≃ (x = y) := recognize x (inl y) - hott def inlInr (x : A) (y : B) : @Id (A + B) (inl x) (inr y) ≃ 𝟎 := + hott corollary inlInr (x : A) (y : B) : @Id (A + B) (inl x) (inr y) ≃ 𝟎 := recognize x (inr y) end inl namespace inr - hott def code (b₀ : B) : A + B → Type v + hott definition code (b₀ : B) : A + B → Type v | inl a => 𝟎 | inr b => b₀ = b - hott def encode {b₀ : B} {x : A + B} (p : inr b₀ = x) : code b₀ x := + hott definition encode {b₀ : B} {x : A + B} (p : inr b₀ = x) : code b₀ x := Equiv.transport (code b₀) p (idp b₀) - hott def decode {b₀ : B} : Π {x : A + B} (c : code b₀ x), inr b₀ = x + hott definition decode {b₀ : B} : Π {x : A + B} (c : code b₀ x), inr b₀ = x | inl a, c => Proto.Empty.elim c | inr b, c => ap inr c @@ -96,10 +97,10 @@ namespace Coproduct apply Prod.mk; apply encodeDecode; apply decodeEncode end - hott def inj' (x y : B) : @Id (A + B) (inr x) (inr y) ≃ (x = y) := + hott corollary inj' (x y : B) : @Id (A + B) (inr x) (inr y) ≃ (x = y) := recognize x (inr y) - hott def inrInl (x : B) (y : A) : @Id (A + B) (inr x) (inl y) ≃ 𝟎 := + hott corollary inrInl (x : B) (y : A) : @Id (A + B) (inr x) (inl y) ≃ 𝟎 := recognize x (inl y) end inr diff --git a/GroundZero/Types/Ens.lean b/GroundZero/Types/Ens.lean index d51f7aa..ad28aea 100644 --- a/GroundZero/Types/Ens.lean +++ b/GroundZero/Types/Ens.lean @@ -6,70 +6,71 @@ namespace GroundZero namespace Types universe u v w -def Ens (A : Type u) : Type (max u (v + 1)) := +hott definition Ens (A : Type u) : Type (max u (v + 1)) := Σ (φ : A → Type v), Π x, prop (φ x) -def Ens.contains {A : Type u} (x : A) (s : Ens A) : Type v := s.1 x +hott abbreviation Ens.contains {A : Type u} (x : A) (s : Ens A) : Type v := s.1 x infix:80 (priority := high) " ∈ " => Ens.contains -def Ens.prop {A : Type u} (x : A) (s : Ens A) : prop (x ∈ s) := s.2 x -def Ens.subtype {A : Type u} (s : Ens A) := Σ x, s.1 x +hott definition Ens.prop {A : Type u} (x : A) (s : Ens A) : prop (x ∈ s) := s.2 x +attribute [irreducible] Ens.prop -hott def Ens.univ (A : Type u) : Ens A := +hott abbreviation Ens.subtype {A : Type u} (s : Ens A) := Σ x, s.1 x + +hott definition Ens.univ (A : Type u) : Ens A := ⟨λ _, 𝟏, λ _, unitIsProp⟩ -hott def Ens.empty (A : Type u) : Ens A := +hott definition Ens.empty (A : Type u) : Ens A := ⟨λ _, 𝟎, λ _, emptyIsProp⟩ notation "∅" => Ens.empty _ -hott def Ens.union {A : Type u} (a b : Ens A) : Ens A := +hott definition Ens.union {A : Type u} (a b : Ens A) : Ens A := ⟨λ x, ∥(x ∈ a) + (x ∈ b)∥, λ _, HITs.Merely.uniq⟩ infixl:60 " ∪ " => Ens.union -hott def Ens.sunion {A : Type u} (φ : Ens.{u, v} A → Type w) : Ens A := +hott definition Ens.sunion {A : Type u} (φ : Ens.{u, v} A → Type w) : Ens A := ⟨λ x, ∥(Σ (s : Ens.{u, v} A), x ∈ s × φ s)∥, λ _, HITs.Merely.uniq⟩ -hott def Ens.iunion {A : Type u} {β : Type v} (φ : A → Ens β) : Ens β := +hott definition Ens.iunion {A : Type u} {β : Type v} (φ : A → Ens β) : Ens β := ⟨λ x, ∥(Σ y, x ∈ φ y)∥, λ _, HITs.Merely.uniq⟩ prefix:110 "⋃" => Ens.iunion -hott def Ens.inter {A : Type u} (a b : Ens A) : Ens A := +hott definition Ens.inter {A : Type u} (a b : Ens A) : Ens A := ⟨λ x, x ∈ a × x ∈ b, begin intro; apply Structures.productProp <;> apply Ens.prop end⟩ infixl:60 " ∩ " => Ens.inter -hott def Ens.smallest {A : Type u} (φ : Ens.{u, v} A → Type w) : Ens A := +hott definition Ens.smallest {A : Type u} (φ : Ens.{u, v} A → Type w) : Ens A := ⟨λ x, ∀ (s : Ens.{u, v} A), φ s → x ∈ s, λ y, begin apply Structures.piProp; intro; apply Structures.implProp; apply Ens.prop end⟩ -hott def Ens.infInter {A : Type u} (φ : Ens (Ens A)) : Ens A := Ens.smallest φ.1 +hott definition Ens.infInter {A : Type u} (φ : Ens (Ens A)) : Ens A := Ens.smallest φ.1 -hott def Ens.ssubset {A : Type u} (φ : Ens.{u, v} A) (ψ : Ens.{u, w} A) := +hott definition Ens.ssubset {A : Type u} (φ : Ens.{u, v} A) (ψ : Ens.{u, w} A) := Π x, x ∈ φ → x ∈ ψ infix:50 " ⊆ " => Ens.ssubset -hott def Ens.ssubset.prop {A : Type u} (φ : Ens.{u, v} A) (ψ : Ens.{u, w} A) : Structures.prop (φ ⊆ ψ) := +hott lemma Ens.ssubset.prop {A : Type u} (φ : Ens.{u, v} A) (ψ : Ens.{u, w} A) : Structures.prop (φ ⊆ ψ) := begin apply piProp; intro; apply implProp; apply Ens.prop end -hott def Ens.ssubset.refl {A : Type u} (φ : Ens A) : φ ⊆ φ := +hott lemma Ens.ssubset.refl {A : Type u} (φ : Ens A) : φ ⊆ φ := begin intro; apply id end -hott def Ens.ssubset.trans {A : Type u} {a b c : Ens A} : a ⊆ b → b ⊆ c → a ⊆ c := +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⟩ -hott def Ens.parallel {A : Type u} (a b : Ens A) := a ∩ b ⊆ ∅ +hott definition Ens.parallel {A : Type u} (a b : Ens A) := a ∩ b ⊆ ∅ -hott def Ens.image {A : Type u} {β : Type v} (φ : Ens A) (f : A → β) : Ens β := +hott definition Ens.image {A : Type u} {β : Type v} (φ : Ens A) (f : A → β) : Ens β := ⟨λ y, ∥(Σ x, f x = y × x ∈ φ)∥, λ _, HITs.Merely.uniq⟩ -noncomputable hott def Ens.ext {A : Type u} {φ ψ : Ens A} - (H : Π x, x ∈ φ ↔ x ∈ ψ) : φ = ψ := +noncomputable hott definition Ens.ext {A : Type u} {φ ψ : Ens A} (H : Π x, x ∈ φ ↔ x ∈ ψ) : φ = ψ := begin fapply Sigma.prod; apply Theorems.funext; intro x; { apply ua; apply Structures.propEquivLemma; @@ -77,19 +78,19 @@ begin { apply piProp; intro; apply propIsProp } end -noncomputable hott def Ens.ssubset.asymm {A : Type u} {φ ψ : Ens A} +noncomputable hott definition Ens.ssubset.asymm {A : Type u} {φ ψ : Ens A} (f : φ ⊆ ψ) (g : ψ ⊆ φ) : φ = ψ := Ens.ext (λ x, ⟨f x, g x⟩) -hott def Ens.hset {A : Type u} (s : Ens A) (H : hset A) : hset s.subtype := +hott lemma Ens.hset {A : Type u} (s : Ens A) (H : hset A) : hset s.subtype := begin apply hsetRespectsSigma; apply H; { intro; apply propIsSet; apply s.2 } end -hott def predicate (A : Type u) := A → Prop v +hott definition predicate (A : Type u) := A → Prop v -hott def Ens.eqvPredicate {A : Type u} : Ens A ≃ predicate A := +hott lemma Ens.eqvPredicate {A : Type u} : Ens A ≃ predicate A := begin fapply Sigma.mk; { intros φ x; existsi φ.1 x; apply φ.2 }; apply Qinv.toBiinv; fapply Sigma.mk; { intro φ; existsi (λ x, (φ x).1); intro x; apply (φ x).2 }; fapply Prod.mk <;> intro φ; @@ -97,18 +98,18 @@ begin { fapply Sigma.prod <;> apply Theorems.funext <;> intro x; reflexivity; apply propIsProp } end -noncomputable hott def Ens.isset {A : Type u} : Structures.hset (Ens A) := +noncomputable hott lemma Ens.isset {A : Type u} : Structures.hset (Ens A) := begin apply hsetRespectsEquiv; symmetry; apply Ens.eqvPredicate; apply piHset; intro; apply Theorems.Equiv.propsetIsSet end -hott def Ens.inh {A : Type u} (φ : Ens A) := ∥φ.subtype∥ +hott definition Ens.inh {A : Type u} (φ : Ens A) := ∥φ.subtype∥ -hott def Ens.singleton {A : Type u} (H : Structures.hset A) (x : A) : Ens A := +hott definition Ens.singleton {A : Type u} (H : Structures.hset A) (x : A) : Ens A := ⟨λ y, x = y, @H x⟩ -hott def Ens.singletonInh {A : Type u} (H : Structures.hset A) (x : A) : Ens.inh (Ens.singleton @H x) := +hott definition Ens.singletonInh {A : Type u} (H : Structures.hset A) (x : A) : Ens.inh (Ens.singleton @H x) := HITs.Merely.elem ⟨x, Id.refl⟩ end Types diff --git a/GroundZero/Types/HEq.lean b/GroundZero/Types/HEq.lean index 02e7227..2ec2446 100644 --- a/GroundZero/Types/HEq.lean +++ b/GroundZero/Types/HEq.lean @@ -6,22 +6,22 @@ namespace GroundZero.Types.HEq universe u v -hott def inclusion {A : Type u} {a b : A} (p : a = b) : HEq a b := +hott definition inclusion {A : Type u} {a b : A} (p : a = b) : HEq a b := begin induction p; apply HEq.refl end -hott def map {A : Type u} {B : A → Type v} {a b : A} +hott definition map {A : Type u} {B : A → Type v} {a b : A} (f : Π x, B x) (p : a = b) : HEq (f a) (f b) := begin induction p; apply HEq.refl end -hott def onlyRefl {A : Type u} {a b : A} (p : a = b) : HEq p (idp a) := +hott definition onlyRefl {A : Type u} {a b : A} (p : a = b) : HEq p (idp a) := begin induction p; apply HEq.refl end -hott def eqSubstHEq {A : Type u} {B : A → Type v} {a b : A} +hott definition eqSubstHEq {A : Type u} {B : A → Type v} {a b : A} (p : a = b) (x : B a) : HEq x (transport B p x) := begin induction p; apply HEq.refl end -hott def fromPathover {A : Type u} {B : A → Type v} - {a b : A} (p : a = b) {u : B a} {v : B b} (q : u =[p] v) : HEq u v := +hott definition fromPathover {A : Type u} {B : A → Type v} {a b : A} + (p : a = b) {u : B a} {v : B b} (q : u =[p] v) : HEq u v := begin induction p; induction q; apply HEq.refl end end GroundZero.Types.HEq