Skip to content

Commit

Permalink
refl → idp & map → ap & something in Hopf.lean
Browse files Browse the repository at this point in the history
  • Loading branch information
@forked-from-1kasper
forked-from-1kasper committed Nov 4, 2023
1 parent ead4cbb commit fb21f36
Show file tree
Hide file tree
Showing 61 changed files with 865 additions and 778 deletions.
57 changes: 29 additions & 28 deletions GroundZero/Algebra/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ import GroundZero.Types.Ens

open GroundZero.Types GroundZero.Structures
open GroundZero.HITs.Interval (happly)
open GroundZero.Types.Id (ap)
open GroundZero.Types.Equiv
open GroundZero

Expand Down Expand Up @@ -75,12 +76,12 @@ namespace GroundZero.Algebra
respects g → respects f → respects (g ∘ f) :=
begin
intros p q; apply Prod.mk <;> intros;
{ transitivity; apply Id.map g; apply q.1;
{ transitivity; apply ap g; apply q.1;
transitivity; apply p.1;
apply Id.map; apply vect.comp };
apply ap; apply vect.comp };
{ transitivity; apply q.2;
transitivity; apply p.2;
apply Id.map; apply vect.comp }
apply ap; apply vect.comp }
end

hott def Hom (Γ Λ : Alg deg) :=
Expand All @@ -96,8 +97,8 @@ namespace GroundZero.Algebra
hott def Hom.id (Γ : Alg deg) : Hom Γ Γ :=
begin
existsi Proto.idfun; apply Prod.mk <;> intros i v <;> symmetry;
apply Id.map (Γ.op i); apply vect.id;
apply Id.map (Γ.rel i); apply vect.id
apply Id.ap (Γ.op i); apply vect.id;
apply Id.ap (Γ.rel i); apply vect.id
end

noncomputable hott def Hom.funext {Γ Λ : Alg deg} :
Expand Down Expand Up @@ -139,7 +140,7 @@ namespace GroundZero.Algebra
end

noncomputable hott def Iso.eqIffEqEqv {Γ Λ : Alg deg} (φ ψ : Iso Γ Λ) : φ.eqv = ψ.eqv → φ = ψ :=
begin intro p; apply Iso.ext; apply happly; apply Id.map Sigma.fst p end
begin intro p; apply Iso.ext; apply happly; apply Id.ap Sigma.fst p end

hott def Iso.hom {Γ Λ : Alg deg} (φ : Iso Γ Λ) : Hom Γ Λ :=
⟨φ.ap, φ.2.1⟩
Expand All @@ -156,8 +157,8 @@ namespace GroundZero.Algebra
hott def Iso.refl (Γ : Alg deg) : Iso Γ Γ :=
begin
fapply Iso.ofEquiv; reflexivity; apply Prod.mk <;> intros i v;
{ apply Id.map (Γ.op i); symmetry; apply vect.id };
{ apply Id.map (Γ.rel i); symmetry; apply vect.id }
{ apply Id.ap (Γ.op i); symmetry; apply vect.id };
{ apply Id.ap (Γ.rel i); symmetry; apply vect.id }
end

hott def Iso.symm {Γ Λ : Alg deg} : Iso Γ Λ → Iso Λ Γ :=
Expand All @@ -166,10 +167,10 @@ namespace GroundZero.Algebra
existsi f.eqv.left; apply Prod.mk;
{ apply Prod.mk <;> intros i v;
{ symmetry; transitivity; { symmetry; apply f.eqv.leftForward };
transitivity; apply Id.map f.eqv.left; apply f.2.1.1;
apply Id.map (f.eqv.left ∘ Λ.op i); transitivity;
transitivity; apply Id.ap f.eqv.left; apply f.2.1.1;
apply Id.ap (f.eqv.left ∘ Λ.op i); transitivity;
apply vect.comp; apply vect.idfunc; apply μ };
{ transitivity; apply Id.map (Λ.rel i);
{ transitivity; apply Id.ap (Λ.rel i);
transitivity; symmetry; apply vect.idfunc (f.ap ∘ f.eqv.left);
apply μ; symmetry; apply vect.comp; symmetry; apply f.2.1.2 } };
{ apply Prod.mk <;> existsi f.ap; apply μ; apply f.eqv.leftForward }
Expand Down Expand Up @@ -201,7 +202,7 @@ namespace GroundZero.Algebra
intro ⟨A, F⟩ ⟨B, G⟩ C (p : A = B) u; induction p;
have ρ : F = G := ntypeIsProp 0 F G; induction ρ;
transitivity; apply Equiv.transportToTransportconst; transitivity;
apply Id.map (λ p, transportconst (Id.map (C ∘ Sigma.fst) p) u);
apply Id.ap (λ p, transportconst (Id.ap (C ∘ Sigma.fst) p) u);
apply zeroPathRefl; reflexivity
end

Expand All @@ -218,7 +219,7 @@ namespace GroundZero.Algebra
φ.1 ∘ transportconst (ua φ)⁻¹ = id :=
begin
apply Theorems.funext; intro x;
transitivity; apply Id.map φ.1;
transitivity; apply Id.ap φ.1;
transitivity; apply Equiv.substOverInvPath;
apply ua.transportInvRule;
apply Equiv.forwardLeft
Expand All @@ -231,9 +232,9 @@ namespace GroundZero.Algebra
apply transportOverFunctor (λ A, vect A (deg (Sum.inl i))) id;
apply Theorems.funext; intro v;
transitivity; apply ua.transportRule;
transitivity; apply p.1; apply Id.map;
transitivity; apply p.1; apply Id.ap;
transitivity; apply vect.subst;
transitivity; apply Id.map (vect.map · v);
transitivity; apply Id.ap (vect.map · v);
apply equivCompSubst ⟨φ, q⟩; apply vect.id
end

Expand All @@ -243,35 +244,35 @@ namespace GroundZero.Algebra
intro ⟨φ, (p, q)⟩ i; apply Id.trans;
apply transportOverFunctor (λ A, vect A (deg (Sum.inr i))) (λ _, Prop);
apply Theorems.funext; intro v;
transitivity; apply Id.map (subst (ua ⟨φ, q⟩));
transitivity; apply p.2; apply Id.map (Λ.rel i);
transitivity; apply Id.ap (subst (ua ⟨φ, q⟩));
transitivity; apply p.2; apply Id.ap (Λ.rel i);
transitivity; apply vect.subst;
transitivity; apply Id.map (vect.map · v);
transitivity; apply Id.ap (vect.map · v);
apply equivCompSubst ⟨φ, q⟩; apply vect.id; change transport _ _ _ = _;
transitivity; apply Equiv.transportToTransportconst;
transitivity; apply Id.map (transportconst · (Λ.rel i v));
transitivity; apply Id.ap (transportconst · (Λ.rel i v));
apply constmap; reflexivity
end

noncomputable hott def Alg.ua {Γ Λ : Alg deg} (φ : Iso Γ Λ) : Γ = Λ :=
Alg.ext (GroundZero.ua φ.eqv) (uaPreservesOp φ) (uaPreservesRel φ)

hott def Alg.eqcar {Γ Λ : Alg deg} : Γ = Λ → Γ.carrier = Λ.carrier :=
λ p, @Id.map (0-Type) (Type _) _ _ Sigma.fst (Id.map Sigma.fst p)
λ p, @Id.ap (0-Type) (Type _) _ _ Sigma.fst (Id.ap Sigma.fst p)

noncomputable hott def Alg.uaext : Π {Γ Λ : Alg deg} (φ : Iso Γ Λ), GroundZero.ua φ.eqv = Alg.eqcar (Alg.ua φ) :=
begin
intro ⟨⟨A, f⟩, (Γ₁, Γ₂)⟩ ⟨⟨B, g⟩, (Λ₁, Λ₂)⟩ φ;
symmetry; change Id.map _ _ = _; transitivity; apply Id.map;
symmetry; change Id.ap _ _ = _; transitivity; apply Id.ap;
apply Sigma.mapFstOverProd; apply Sigma.mapFstOverProd
end

noncomputable hott def Alg.inj {Γ Λ : Alg deg} {φ ψ : Iso Γ Λ} (p : Alg.ua φ = Alg.ua ψ) : φ = ψ :=
begin
apply Iso.eqIffEqEqv; transitivity; symmetry; apply ua.uaβrule;
transitivity; apply Id.map; apply Alg.uaext;
transitivity; apply Id.map (Equiv.idtoeqv ∘ Alg.eqcar);
exact p; transitivity; apply Id.map Equiv.idtoeqv;
transitivity; apply Id.ap; apply Alg.uaext;
transitivity; apply Id.ap (Equiv.idtoeqv ∘ Alg.eqcar);
exact p; transitivity; apply Id.ap Equiv.idtoeqv;
symmetry; apply Alg.uaext; apply ua.uaβrule
end

Expand All @@ -290,10 +291,10 @@ namespace GroundZero.Algebra
change Sigma.prod _ _ = _;
transitivity; apply transportOverProd;
transitivity; transitivity; apply transportOverProd;
apply ua.reflOnUa; apply Id.map (Sigma.prod Id.refl);
apply ua.reflOnUa; apply Id.ap (Sigma.prod Id.refl);
change _ = Id.refl; apply propIsSet;
apply ntypeIsProp; apply Sigma.prodRefl;
transitivity; apply Id.map (Sigma.prod Id.refl);
transitivity; apply Id.ap (Sigma.prod Id.refl);
change _ = Id.refl; apply Algebra.hset;
apply zeroEqvSet.forward Γ.1.2;
apply Sigma.prodRefl
Expand Down Expand Up @@ -356,7 +357,7 @@ namespace GroundZero.Algebra
Σ e, Π a, M.φ a e = a

hott def isUnital (M : Magma) :=
Σ e, Π a, M.φ e a = a × M.φ a e = a
Σ e, Π a, M.φ e a = a × M.φ a e = a

hott def isLeftInvertible (M : Magma) (e : M.carrier) :=
Σ (ι : M →ᴬ M), Π a, M.φ (ι a) a = e
Expand Down Expand Up @@ -539,4 +540,4 @@ namespace GroundZero.Algebra
end Abelian

notation:51 A " ≅ " B => Iso A.1 B.1
end GroundZero.Algebra
end GroundZero.Algebra
53 changes: 27 additions & 26 deletions GroundZero/Algebra/Category.lean
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
import GroundZero.Theorems.Classical
import GroundZero.Algebra.Basic

open GroundZero.Types.Id (ap)
open GroundZero.Types.Equiv
open GroundZero.Structures
open GroundZero.Theorems
Expand Down Expand Up @@ -173,10 +174,10 @@ namespace Category
begin
intro x; match defDec x with
| Sum.inl p => _ | Sum.inr q => _;
{ transitivity; apply Id.map; exact p;
transitivity; apply Id.map 𝒞.dom; apply bottomDom;
apply Id.map; symmetry; assumption };
{ symmetry; transitivity; apply Id.map 𝒞.dom;
{ transitivity; apply ap; exact p;
transitivity; apply ap 𝒞.dom; apply bottomDom;
apply ap; symmetry; assumption };
{ symmetry; transitivity; apply ap 𝒞.dom;
symmetry; apply domComp; apply mulDom;
apply transport 𝒞.defined (domComp x)⁻¹ q }
end
Expand All @@ -185,36 +186,36 @@ namespace Category
begin
intro x; match defDec x with
| Sum.inl p => _ | Sum.inr q => _;
{ transitivity; apply Id.map; exact p;
transitivity; apply Id.map 𝒞.cod; apply bottomCod;
apply Id.map; symmetry; assumption };
{ symmetry; transitivity; apply Id.map 𝒞.cod;
{ transitivity; apply ap; exact p;
transitivity; apply ap 𝒞.cod; apply bottomCod;
apply ap; symmetry; assumption };
{ symmetry; transitivity; apply ap 𝒞.cod;
symmetry; apply codComp; apply mulCod;
apply transport 𝒞.defined (codComp x)⁻¹ q }
end

hott def codMulCod : Π a, 𝒞.μ (𝒞.cod a) (𝒞.cod a) = 𝒞.cod a :=
begin
intro a; transitivity; apply Id.map (𝒞.μ · (𝒞.cod a));
intro a; transitivity; apply ap (𝒞.μ · (𝒞.cod a));
symmetry; apply codCod; apply codComp
end

hott def domMulDom : Π a, 𝒞.μ (𝒞.dom a) (𝒞.dom a) = 𝒞.dom a :=
begin
intro a; transitivity; apply Id.map (𝒞.μ (𝒞.dom a));
intro a; transitivity; apply ap (𝒞.μ (𝒞.dom a));
symmetry; apply domDom; apply domComp
end

hott def undefDomImplUndef {a : 𝒞.carrier} : 𝒞.dom a = ∄ → a = ∄ :=
begin
intro p; transitivity; apply (domComp a)⁻¹;
transitivity; apply Id.map (𝒞.μ a) p; apply bottomRight
transitivity; apply ap (𝒞.μ a) p; apply bottomRight
end

hott def undefCodImplUndef {a : 𝒞.carrier} : 𝒞.cod a = ∄ → a = ∄ :=
begin
intro p; transitivity; apply (codComp a)⁻¹;
transitivity; apply Id.map (𝒞.μ · a) p; apply bottomLeft
transitivity; apply ap (𝒞.μ · a) p; apply bottomLeft
end

hott def defImplDomDef {a : 𝒞.carrier} : ∃a → ∃(𝒞.dom a) :=
Expand All @@ -226,13 +227,13 @@ namespace Category
hott def domDefImplDef {a : 𝒞.carrier} : ∃(𝒞.dom a) → ∃a :=
begin
apply Classical.Contrapos.intro; intro p;
transitivity; apply Id.map 𝒞.dom p; apply bottomDom
transitivity; apply ap 𝒞.dom p; apply bottomDom
end

hott def codDefImplDef {a : 𝒞.carrier} : ∃(𝒞.cod a) → ∃a :=
begin
apply Classical.Contrapos.intro; intro p;
transitivity; apply Id.map 𝒞.cod p; apply bottomCod
transitivity; apply ap 𝒞.cod p; apply bottomCod
end

hott def codDefImplDomDef {a : 𝒞.carrier} : ∃(𝒞.cod a) → ∃(𝒞.dom a) :=
Expand All @@ -253,7 +254,7 @@ namespace Category
hott def idEndo (a : 𝒞.carrier) : 𝒞.id a → 𝒞.endo a :=
begin
intro p; change _ = _; symmetry; transitivity;
apply Id.map; exact p; apply codDom
apply ap; exact p; apply codDom
end

hott def following.domImplTotal {f g : 𝒞.carrier} :
Expand All @@ -276,19 +277,19 @@ namespace Category
begin
apply Prod.mk; { intro p; transitivity; exact p; apply idEndo a p };
{ intro p; change _ = _; transitivity; exact p; symmetry;
transitivity; apply Id.map; exact p; apply domCod }
transitivity; apply ap; exact p; apply domCod }
end

hott def mulDefImplLeftDef {a b : 𝒞.carrier} : ∃(𝒞.μ a b) → ∃a :=
begin
apply Classical.Contrapos.intro; intro p; transitivity;
apply Id.map (𝒞.μ · b); exact p; apply bottomLeft
apply ap (𝒞.μ · b); exact p; apply bottomLeft
end

hott def mulDefImplRightDef {a b : 𝒞.carrier} : ∃(𝒞.μ a b) → ∃b :=
begin
apply Classical.Contrapos.intro; intro p; transitivity;
apply Id.map (𝒞.μ a); exact p; apply bottomRight
apply ap (𝒞.μ a); exact p; apply bottomRight
end

hott def defImplFollowing {a b : 𝒞.carrier} : ∃(𝒞.μ a b) → 𝒞.following a b :=
Expand Down Expand Up @@ -336,21 +337,21 @@ namespace Category

hott def domHeteroComp {a b : 𝒞.carrier} : ∃(𝒞.μ (𝒞.dom a) b) → 𝒞.μ (𝒞.dom a) b = b :=
begin
intro p; transitivity; apply Id.map (𝒞.μ · b);
intro p; transitivity; apply ap (𝒞.μ · b);
transitivity; apply (domDom a)⁻¹;
apply defImplFollowing p; apply codComp
end

hott def codHeteroComp {a b : 𝒞.carrier} : ∃(𝒞.μ a (𝒞.cod b)) → 𝒞.μ a (𝒞.cod b) = a :=
begin
intro p; transitivity; apply Id.map (𝒞.μ a);
intro p; transitivity; apply ap (𝒞.μ a);
transitivity; apply (codCod b)⁻¹;
symmetry; apply defImplFollowing p; apply domComp
end

hott def idComp {a b : 𝒞.carrier} : ∃(𝒞.μ a b) → 𝒞.id a → 𝒞.μ a b = b :=
begin
intros p q; transitivity; apply Id.map (𝒞.μ · b);
intros p q; transitivity; apply ap (𝒞.μ · b);
exact q; apply domHeteroComp; apply defImplDomCompDef p
end

Expand All @@ -362,7 +363,7 @@ namespace Category
apply defImplDomCompDef; apply Equiv.subst r q;
apply transport (λ z, 𝒞.μ z y = 𝒞.μ z x); exact p;
transitivity; apply mulAssoc; symmetry;
transitivity; apply mulAssoc; apply Id.map; exact r
transitivity; apply mulAssoc; apply ap; exact r
end

hott def retractionImplEpic {a : 𝒞.carrier} : 𝒞.retraction a → 𝒞.epic a :=
Expand All @@ -373,7 +374,7 @@ namespace Category
apply defImplCodCompDef; apply Equiv.subst r q;
apply transport (λ z, 𝒞.μ y z = 𝒞.μ x z); exact p;
transitivity; symmetry; apply mulAssoc;
transitivity; apply Id.map (𝒞.μ · b);
transitivity; apply ap (𝒞.μ · b);
exact Id.inv r; apply mulAssoc
end

Expand Down Expand Up @@ -466,13 +467,13 @@ namespace Category

hott def leftε {a b : Obj 𝒞} (f : 𝒞.Hom a.val b.val) : ε b ∘ f = f :=
begin
apply 𝒞.homext; transitivity; apply Id.map (𝒞.μ · f.ap);
apply 𝒞.homext; transitivity; apply ap (𝒞.μ · f.ap);
symmetry; apply f.2.2; apply codComp
end

hott def rightε {a b : Obj 𝒞} (f : 𝒞.Hom a.val b.val) : f ∘ ε a = f :=
begin
apply 𝒞.homext; transitivity; apply Id.map (𝒞.μ f.ap);
apply 𝒞.homext; transitivity; apply ap (𝒞.μ f.ap);
symmetry; apply f.2.1; apply domComp
end

Expand All @@ -481,4 +482,4 @@ namespace Category
begin apply 𝒞.homext; apply mulAssoc end
end Category

end GroundZero.Algebra
end GroundZero.Algebra
Loading

0 comments on commit fb21f36

Please sign in to comment.