Skip to content

Commit

Permalink
clean up
Browse files Browse the repository at this point in the history
  • Loading branch information
@forked-from-1kasper
forked-from-1kasper committed Dec 26, 2023
1 parent c780447 commit f6903ab
Show file tree
Hide file tree
Showing 10 changed files with 175 additions and 168 deletions.
26 changes: 13 additions & 13 deletions GroundZero/Theorems/Classical.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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;
Expand All @@ -40,17 +40,17 @@ 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;
intro φ; apply propIsSet; apply HITs.Merely.uniq
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 =>
Expand Down Expand Up @@ -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
Expand Down
52 changes: 26 additions & 26 deletions GroundZero/Theorems/Equiv.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -67,15 +67,15 @@ 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
existsi (g ∘ ·); apply Prod.mk <;> intro <;>
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
Expand Down Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -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 };
Expand Down Expand Up @@ -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;
Expand All @@ -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

Expand Down
36 changes: 18 additions & 18 deletions GroundZero/Theorems/Fibration.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading

0 comments on commit f6903ab

Please sign in to comment.