diff --git a/GroundZero/Algebra/Basic.lean b/GroundZero/Algebra/Basic.lean index f7e56d1..086bc4e 100644 --- a/GroundZero/Algebra/Basic.lean +++ b/GroundZero/Algebra/Basic.lean @@ -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 @@ -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) := @@ -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} : @@ -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⟩ @@ -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 Λ Γ := @@ -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 } @@ -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 @@ -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 @@ -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 @@ -243,13 +244,13 @@ 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 @@ -257,21 +258,21 @@ namespace GroundZero.Algebra 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 @@ -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 @@ -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 @@ -539,4 +540,4 @@ namespace GroundZero.Algebra end Abelian notation:51 A " ≅ " B => Iso A.1 B.1 -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Category.lean b/GroundZero/Algebra/Category.lean index 891206f..0a63c53 100644 --- a/GroundZero/Algebra/Category.lean +++ b/GroundZero/Algebra/Category.lean @@ -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 @@ -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 @@ -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) := @@ -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) := @@ -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} : @@ -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 := @@ -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 @@ -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 := @@ -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 @@ -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 @@ -481,4 +482,4 @@ namespace Category begin apply 𝒞.homext; apply mulAssoc end end Category -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/EilenbergMacLane.lean b/GroundZero/Algebra/EilenbergMacLane.lean index b49276e..c60b7ff 100644 --- a/GroundZero/Algebra/EilenbergMacLane.lean +++ b/GroundZero/Algebra/EilenbergMacLane.lean @@ -4,7 +4,7 @@ import GroundZero.HITs.Trunc open GroundZero.Theorems.Functions GroundZero.Theorems.Equiv open GroundZero.Types.Equiv (idtoeqv) -open GroundZero.Types.Id (dotted) +open GroundZero.Types.Id (dotted ap) open GroundZero.ua (uaβrule) open GroundZero.Structures open GroundZero.Types @@ -74,7 +74,7 @@ namespace K1 axiom recβrule {C : Type v} (baseπ : C) (loopπ : G.carrier → baseπ = baseπ) (mulπ : Π x y, loopπ (G.φ x y) = loopπ x ⬝ loopπ y) (groupoidπ : groupoid C) : - Π x, Id.map (rec baseπ loopπ mulπ groupoidπ) (loop x) = loopπ x + Π x, ap (rec baseπ loopπ mulπ groupoidπ) (loop x) = loopπ x attribute [irreducible] K1 @@ -123,7 +123,7 @@ namespace K1 symmetry; apply Group.cancelLeft }; { intros x y; symmetry; transitivity; { symmetry; apply ua.uaTrans }; - apply Id.map ua; fapply Sigma.prod; + apply ap ua; fapply Sigma.prod; { apply Theorems.funext; intro; apply G.mulAssoc }; { apply biinvProp } }; apply G.hset @@ -151,19 +151,19 @@ namespace K1 case loopπ x => { change _ = _; transitivity; apply Equiv.transportCharacterization; apply Theorems.funext; intro y; transitivity; - apply Id.map (λ p, Equiv.transport (λ x, base = x) (loop x) (loop p)); + apply ap (λ p, Equiv.transport (λ x, base = x) (loop x) (loop p)); transitivity; apply Equiv.transportToTransportconst; - transitivity; apply Id.map (Equiv.transportconst · y); - transitivity; apply Id.mapInv; apply Id.map; + transitivity; apply ap (Equiv.transportconst · y); + transitivity; apply Id.mapInv; apply ap; transitivity; apply Equiv.mapOverComp; - transitivity; apply Id.map; unfold code'; apply recβrule; + transitivity; apply ap; unfold code'; apply recβrule; apply Sigma.mapFstOverProd; apply ua.transportInvRule; transitivity; apply Equiv.transportOverInvContrMap; - transitivity; apply Id.map; apply Equiv.idmap; - transitivity; apply Id.map (· ⬝ loop x); apply loop.mul; + transitivity; apply ap; apply Equiv.idmap; + transitivity; apply ap (· ⬝ loop x); apply loop.mul; transitivity; symmetry; apply Id.assoc; - transitivity; apply Id.map; apply Id.map (· ⬝ loop x); apply loop.inv; - transitivity; apply Id.map; apply Id.invComp; apply Id.reflRight }; + transitivity; apply ap; apply ap (· ⬝ loop x); apply loop.inv; + transitivity; apply ap; apply Id.invComp; apply Id.reflRight }; { apply zeroEqvSet.forward; apply piRespectsNType 0; intro; apply zeroEqvSet.left; apply grpd }; { apply oneEqvGroupoid.forward; @@ -178,9 +178,9 @@ namespace K1 induction z; { intro (x : G.carrier); change encode base (loop x) = _; transitivity; apply Equiv.transportToTransportconst; - transitivity; apply Id.map (Equiv.transportconst · G.e); + transitivity; apply ap (Equiv.transportconst · G.e); transitivity; apply Equiv.mapOverComp; - transitivity; apply Id.map; unfold code'; apply recβrule; + transitivity; apply ap; unfold code'; apply recβrule; apply Sigma.mapFstOverProd; transitivity; apply ua.transportRule; apply G.oneMul }; { apply Theorems.funext; intro; apply hsetBase }; diff --git a/GroundZero/Algebra/Group/Absolutizer.lean b/GroundZero/Algebra/Group/Absolutizer.lean index bc43a7f..8a62cb6 100644 --- a/GroundZero/Algebra/Group/Absolutizer.lean +++ b/GroundZero/Algebra/Group/Absolutizer.lean @@ -1,6 +1,7 @@ import GroundZero.Algebra.Group.Basic import GroundZero.HITs.Quotient +open GroundZero.Types.Id (ap) open GroundZero.Types open GroundZero @@ -20,13 +21,13 @@ namespace Group match p with | Sum.inl u => _ | Sum.inr v => _; { left; exact Id.inv u }; { right; transitivity; symmetry; apply invInv; - apply Id.map; exact Id.inv v } }; + apply ap; exact Id.inv v } }; { intros a b c; apply HITs.Merely.lift₂; intros p q; match p, q with | Sum.inl p₁, Sum.inl q₁ => { left; exact p₁ ⬝ q₁ } | Sum.inl p₁, Sum.inr q₂ => { right; exact p₁ ⬝ q₂ } - | Sum.inr p₂, Sum.inl q₁ => { right; exact p₂ ⬝ Id.map _ q₁ } - | Sum.inr p₂, Sum.inr q₂ => { left; exact p₂ ⬝ Id.map _ q₂ ⬝ invInv _ } } + | Sum.inr p₂, Sum.inl q₁ => { right; exact p₂ ⬝ ap _ q₁ } + | Sum.inr p₂, Sum.inr q₂ => { left; exact p₂ ⬝ ap _ q₂ ⬝ invInv _ } } end⟩ notation "⌈" G "⌉" => «Sosnitsky construction» G @@ -43,14 +44,14 @@ namespace Group hott def Absolutizer.even : φ.ap ∘ G.ι ~ φ.ap := begin - intro; apply Id.map φ.1; apply HITs.Quotient.sound; + intro; apply Id.ap φ.1; apply HITs.Quotient.sound; apply HITs.Merely.elem; right; reflexivity end hott def Absolutizer.inv : Absolutizer G := ⟨G.ι ∘ φ.fst, begin - intro; apply Id.map G.ι; + intro; apply Id.ap G.ι; transitivity; apply φ.even; apply φ.2 end⟩ @@ -58,7 +59,7 @@ namespace Group begin intro; transitivity; apply φ.even; apply φ.idem end hott def Absolutizer.comp₂ : φ.inv.ap ∘ φ.ap ~ φ.inv.ap := - begin intro x; apply Id.map G.ι; apply φ.idem end + begin intro x; apply Id.ap G.ι; apply φ.idem end noncomputable hott def Absolutizer.mul : ⌈G⌉ → ⌈G⌉ → ⌈G⌉ := begin @@ -69,14 +70,14 @@ namespace Group case elemπ p => { intro (q : ∥_∥); induction q; case elemπ q => - { apply Id.map HITs.Quotient.elem; apply Equiv.bimap; + { apply Id.ap HITs.Quotient.elem; apply Equiv.bimap; { induction p using Sum.casesOn; - { apply Id.map; assumption }; - { transitivity; apply Id.map; assumption; + { apply Id.ap; assumption }; + { transitivity; apply Id.ap; assumption; apply Absolutizer.even } }; { induction q using Sum.casesOn; - { apply Id.map; assumption }; - { transitivity; apply Id.map; assumption; + { apply Id.ap; assumption }; + { transitivity; apply Id.ap; assumption; apply Absolutizer.even } } }; apply HITs.Quotient.set }; apply Structures.piProp; intro; apply HITs.Quotient.set } @@ -87,4 +88,4 @@ namespace Group end end Group -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Action.lean b/GroundZero/Algebra/Group/Action.lean index b89d026..0c09a06 100644 --- a/GroundZero/Algebra/Group/Action.lean +++ b/GroundZero/Algebra/Group/Action.lean @@ -1,5 +1,7 @@ import GroundZero.Algebra.Group.Symmetric import GroundZero.HITs.Quotient + +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero @@ -27,15 +29,15 @@ namespace Group variable {G : Group} section - variable {A : Type u} + variable {A : Type u} hott def rightAction.associated : (G ⮎ A) → (G ⮌ A) := λ ⟨φ, (p, q)⟩, ⟨λ x g, φ (G.ι g) x, (begin - intro x; transitivity; apply Id.map (φ · x); + intro x; transitivity; apply ap (φ · x); symmetry; apply unitInv; apply p end, begin intros g h x; transitivity; - apply q; apply Id.map (φ · x); + apply q; apply ap (φ · x); symmetry; apply invExplode end)⟩ @@ -70,9 +72,9 @@ namespace Group begin apply HITs.Merely.lift; intro ⟨g, p⟩; existsi G.ι g; - transitivity; apply Id.map; exact Id.inv p; + transitivity; apply ap; exact Id.inv p; transitivity; apply φ.2.2; - transitivity; apply Id.map (φ.1 · a); + transitivity; apply ap (φ.1 · a); apply G.mulLeftInv; apply φ.2.1 end @@ -81,7 +83,7 @@ namespace Group begin apply HITs.Merely.lift₂; intro ⟨g, p⟩ ⟨h, q⟩; existsi G.φ h g; transitivity; symmetry; apply φ.2.2; - transitivity; apply Id.map; exact p; exact q + transitivity; apply ap; exact p; exact q end hott def leftAction.rel {A : Type u} (φ : G ⮎ A) : hrel A := @@ -168,8 +170,8 @@ namespace Group intro H; apply Prod.mk; { intros a b; apply HITs.Merely.elem; exact (H a b).1 }; { intros x g h p; - apply @Id.map (Σ g, φ.fst g x = φ.fst h x) G.carrier - ⟨g, p⟩ ⟨h, Id.refl⟩ Sigma.fst; + apply @ap (Σ g, φ.fst g x = φ.fst h x) G.carrier + ⟨g, p⟩ ⟨h, Id.refl⟩ Sigma.fst; apply contrImplProp; apply H } end @@ -191,4 +193,4 @@ namespace Group end end Group -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 0aff20f..4c8e852 100644 --- a/GroundZero/Algebra/Group/Alternating.lean +++ b/GroundZero/Algebra/Group/Alternating.lean @@ -1,6 +1,7 @@ import GroundZero.Algebra.Group.Factor + open GroundZero.Types.Equiv (biinv transport) -open GroundZero.Types.Id (map) +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero.Proto @@ -60,12 +61,12 @@ namespace Group intros x y; induction x <;> induction y <;> (first | apply Sum.inl; reflexivity | apply Sum.inr; intro H; apply ffNeqTt; symmetry; first - | apply Id.map (D₃.elim true false false false false false) H - | apply Id.map (D₃.elim false true false false false false) H - | apply Id.map (D₃.elim false false true false false false) H - | apply Id.map (D₃.elim false false false true false false) H - | apply Id.map (D₃.elim false false false false false true) H - | apply Id.map (D₃.elim false false false false true false) H); + | apply ap (D₃.elim true false false false false false) H + | apply ap (D₃.elim false true false false false false) H + | apply ap (D₃.elim false false true false false false) H + | apply ap (D₃.elim false false false true false false) H + | apply ap (D₃.elim false false false false false true) H + | apply ap (D₃.elim false false false false true false) H); exact D₃.mul; exact D₃.inv; exact R₀; { intro a b c; induction a <;> induction b <;> induction c <;> reflexivity }; repeat { intro a; induction a <;> reflexivity } @@ -126,4 +127,4 @@ namespace Group end end Group -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Basic.lean b/GroundZero/Algebra/Group/Basic.lean index f32b7bb..5732916 100644 --- a/GroundZero/Algebra/Group/Basic.lean +++ b/GroundZero/Algebra/Group/Basic.lean @@ -1,7 +1,8 @@ import GroundZero.Theorems.Functions import GroundZero.Algebra.Basic + open GroundZero.Types.Equiv (bimap biinv transport) -open GroundZero.Types.Id (map) +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero.Proto @@ -90,52 +91,52 @@ namespace Group hott def unitOfSqr {x : G.carrier} (h : x * x = x) := calc x = e * x : Id.inv (G.oneMul _) - ... = (x⁻¹ * x) * x : Id.map (G.φ · x) (Id.inv (G.mulLeftInv x)) + ... = (x⁻¹ * x) * x : ap (G.φ · x) (Id.inv (G.mulLeftInv x)) ... = x⁻¹ * (x * x) : G.mulAssoc _ _ _ - ... = x⁻¹ * x : Id.map (G.φ x⁻¹) h + ... = x⁻¹ * x : ap (G.φ x⁻¹) h ... = e : G.mulLeftInv _ hott def invEqOfMulEqOne {x y : G.carrier} (h : x * y = e) := calc x⁻¹ = x⁻¹ * e : Id.inv (G.mulOne _) - ... = x⁻¹ * (x * y) : Id.map (G.φ x⁻¹) (Id.inv h) + ... = x⁻¹ * (x * y) : ap (G.φ x⁻¹) (Id.inv h) ... = (x⁻¹ * x) * y : Id.inv (G.mulAssoc _ _ _) - ... = e * y : Id.map (G.φ · y) (G.mulLeftInv x) + ... = e * y : ap (G.φ · y) (G.mulLeftInv x) ... = y : G.oneMul y hott def invInv (x : G.carrier) : x⁻¹⁻¹ = x := invEqOfMulEqOne (G.mulLeftInv x) hott def eqInvOfMulEqOne {x y : G.carrier} (h : x * y = e) : x = y⁻¹ := - Id.inv (invInv x) ⬝ Id.map G.ι (invEqOfMulEqOne h) + Id.inv (invInv x) ⬝ ap G.ι (invEqOfMulEqOne h) hott def mulRightInv (x : G.carrier) := calc - x * x⁻¹ = x⁻¹⁻¹ * x⁻¹ : Id.map (G.φ · x⁻¹) (Id.inv (invInv x)) + x * x⁻¹ = x⁻¹⁻¹ * x⁻¹ : ap (G.φ · x⁻¹) (Id.inv (invInv x)) ... = e : G.mulLeftInv x⁻¹ hott def mulEqOneOfInvEq {x y : G.carrier} (h : x⁻¹ = y) : x * y = e := - Id.inv (Id.map (G.φ x) h) ⬝ (mulRightInv x) + Id.inv (ap (G.φ x) h) ⬝ (mulRightInv x) hott def invInj {x y : G.carrier} (h : x⁻¹ = y⁻¹) : x = y := calc x = x⁻¹⁻¹ : Id.inv (invInv x) - ... = y⁻¹⁻¹ : Id.map G.ι h + ... = y⁻¹⁻¹ : ap G.ι h ... = y : invInv y hott def mulCancelLeft {a b c : G.carrier} (h : c * a = c * b) := calc a = e * a : Id.inv (G.oneMul a) - ... = (c⁻¹ * c) * a : Id.map (G.φ · a) (Id.inv (G.mulLeftInv c)) + ... = (c⁻¹ * c) * a : ap (G.φ · a) (Id.inv (G.mulLeftInv c)) ... = c⁻¹ * (c * a) : G.mulAssoc _ _ _ - ... = c⁻¹ * (c * b) : Id.map (G.φ c⁻¹) h + ... = c⁻¹ * (c * b) : ap (G.φ c⁻¹) h ... = (c⁻¹ * c) * b : Id.inv (G.mulAssoc _ _ _) - ... = e * b : Id.map (G.φ · b) (G.mulLeftInv c) + ... = e * b : ap (G.φ · b) (G.mulLeftInv c) ... = b : G.oneMul b hott def mulCancelRight {a b c : G.carrier} (h : a * c = b * c) := calc a = a * e : Id.inv (G.mulOne a) - ... = a * (c * c⁻¹) : Id.map (G.φ a) (Id.inv (mulRightInv c)) + ... = a * (c * c⁻¹) : ap (G.φ a) (Id.inv (mulRightInv c)) ... = (a * c) * c⁻¹ : Id.inv (G.mulAssoc _ _ _) - ... = (b * c) * c⁻¹ : Id.map (G.φ · c⁻¹) h + ... = (b * c) * c⁻¹ : ap (G.φ · c⁻¹) h ... = b * (c * c⁻¹) : G.mulAssoc _ _ _ - ... = b * e : Id.map (G.φ b) (mulRightInv c) + ... = b * e : ap (G.φ b) (mulRightInv c) ... = b : G.mulOne b hott def unitInv : e = e⁻¹ := @@ -154,16 +155,16 @@ namespace Group invEqOfMulEqOne (calc (x * y) * (y⁻¹ * x⁻¹) = ((x * y) * y⁻¹) * x⁻¹ : Id.inv (G.mulAssoc _ _ _) - ... = (x * (y * y⁻¹)) * x⁻¹ : Id.map (G.φ · x⁻¹) (G.mulAssoc _ _ _) - ... = (x * e) * x⁻¹ : Id.map (λ z, (x * z) * x⁻¹) (mulRightInv _) - ... = x * x⁻¹ : Id.map (G.φ · x⁻¹) (G.mulOne x) + ... = (x * (y * y⁻¹)) * x⁻¹ : ap (G.φ · x⁻¹) (G.mulAssoc _ _ _) + ... = (x * e) * x⁻¹ : ap (λ z, (x * z) * x⁻¹) (mulRightInv _) + ... = x * x⁻¹ : ap (G.φ · x⁻¹) (G.mulOne x) ... = e : mulRightInv _) hott def sqrUnit {x : G.carrier} (p : x * x = e) := calc x = x * e : Id.inv (G.mulOne x) - ... = x * (x * x⁻¹) : Id.map (G.φ x) (Id.inv (mulRightInv x)) + ... = x * (x * x⁻¹) : ap (G.φ x) (Id.inv (mulRightInv x)) ... = (x * x) * x⁻¹ : Id.inv (G.mulAssoc x x x⁻¹) - ... = e * x⁻¹ : Id.map (G.φ · x⁻¹) p + ... = e * x⁻¹ : ap (G.φ · x⁻¹) p ... = x⁻¹ : G.oneMul x⁻¹ hott def sqrUnitImplsAbelian (H : Π x, x * x = e) : G.isCommutative := @@ -186,29 +187,29 @@ namespace Group hott def cancelLeft (a b : G.carrier) := calc a = a * e : Id.inv (G.mulOne a) - ... = a * (b⁻¹ * b) : Id.map (G.φ a) (Id.inv (G.mulLeftInv b)) + ... = a * (b⁻¹ * b) : ap (G.φ a) (Id.inv (G.mulLeftInv b)) ... = (a * b⁻¹) * b : Id.inv (G.mulAssoc a b⁻¹ b) hott def cancelRight (a b : G.carrier) := calc a = a * e : Id.inv (G.mulOne a) - ... = a * (b * b⁻¹) : Id.map (G.φ a) (Id.inv (mulRightInv b)) + ... = a * (b * b⁻¹) : ap (G.φ a) (Id.inv (mulRightInv b)) ... = (a * b) * b⁻¹ : Id.inv (G.mulAssoc a b b⁻¹) hott def revCancelLeft (a b : G.carrier) := calc b = e * b : Id.inv (G.oneMul b) - ... = (a⁻¹ * a) * b : Id.map (G.φ · b) (Id.inv (G.mulLeftInv a)) + ... = (a⁻¹ * a) * b : ap (G.φ · b) (Id.inv (G.mulLeftInv a)) ... = a⁻¹ * (a * b) : G.mulAssoc a⁻¹ a b hott def revCancelRight (a b : G.carrier) := calc b = e * b : Id.inv (G.oneMul b) - ... = (a * a⁻¹) * b : Id.map (G.φ · b) (Id.inv (mulRightInv a)) + ... = (a * a⁻¹) * b : ap (G.φ · b) (Id.inv (mulRightInv a)) ... = a * (a⁻¹ * b) : G.mulAssoc a a⁻¹ b hott def commImplConj {x y : G.carrier} (p : x * y = y * x) : x = x ^ y := calc x = e * x : Id.inv (G.oneMul x) - ... = (y⁻¹ * y) * x : Id.map (G.φ · x) (Id.inv (G.mulLeftInv y)) + ... = (y⁻¹ * y) * x : ap (G.φ · x) (Id.inv (G.mulLeftInv y)) ... = y⁻¹ * (y * x) : G.mulAssoc y⁻¹ y x - ... = y⁻¹ * (x * y) : Id.map (G.φ y⁻¹) (Id.inv p) + ... = y⁻¹ * (x * y) : ap (G.φ y⁻¹) (Id.inv p) ... = (y⁻¹ * x) * y : Id.inv (G.mulAssoc y⁻¹ x y) ... = x ^ y : Id.refl @@ -216,7 +217,7 @@ namespace Group begin transitivity; apply eqInvOfMulEqOne (y := y⁻¹); transitivity; symmetry; apply invExplode; - transitivity; apply Id.map G.ι; exact h; + transitivity; apply ap G.ι; exact h; apply Id.inv unitInv; apply invInv end @@ -246,7 +247,7 @@ namespace Group (p : commutator x y = e) : x * y = y * x := begin symmetry; transitivity; { symmetry; apply invInv }; - transitivity; apply Id.map; apply invExplode; + transitivity; apply ap; apply invExplode; symmetry; apply eqInvOfMulEqOne; exact p end @@ -254,10 +255,10 @@ namespace Group (commutator x y)⁻¹ = commutator y x := begin transitivity; apply invExplode; - transitivity; apply Id.map; apply invExplode; - apply Id.map (λ z, z * (y⁻¹ * x⁻¹)); transitivity; apply invExplode; - transitivity; apply Id.map; apply invInv; - apply Id.map (G.φ · x); apply invInv + transitivity; apply ap; apply invExplode; + apply ap (λ z, z * (y⁻¹ * x⁻¹)); transitivity; apply invExplode; + transitivity; apply ap; apply invInv; + apply ap (G.φ · x); apply invInv end def ldiv (φ : G.subgroup) := λ x y, @leftDiv G x y ∈ φ.set @@ -265,14 +266,14 @@ namespace Group hott def invMulInv (x y : G.carrier) := calc (x⁻¹ * y)⁻¹ = y⁻¹ * x⁻¹⁻¹ : invExplode _ _ - ... = y⁻¹ * x : Id.map (G.φ y⁻¹) (invInv x) + ... = y⁻¹ * x : ap (G.φ y⁻¹) (invInv x) hott def mulInvInv (x y : G.carrier) := calc (x * y⁻¹)⁻¹ = y⁻¹⁻¹ * x⁻¹ : invExplode _ _ - ... = y * x⁻¹ : Id.map (G.φ · x⁻¹) (invInv y) + ... = y * x⁻¹ : ap (G.φ · x⁻¹) (invInv y) hott def divByUnit (x : G.carrier) : x / e = x := - begin change _ * _ = _; transitivity; apply Id.map; symmetry; apply unitInv; apply G.mulOne end + begin change _ * _ = _; transitivity; apply ap; symmetry; apply unitInv; apply G.mulOne end hott def ldivByUnit (x : G.carrier) : leftDiv x e = x⁻¹ := by apply G.mulOne @@ -281,19 +282,19 @@ namespace Group (leftDiv x y) * (leftDiv y z) = (x⁻¹ * y) * (y⁻¹ * z) : Id.refl ... = x⁻¹ * (y * (y⁻¹ * z)) : G.mulAssoc x⁻¹ y (y⁻¹ * z) - ... = x⁻¹ * ((y * y⁻¹) * z) : Id.map (G.φ x⁻¹) (Id.inv (G.mulAssoc y y⁻¹ z)) - ... = x⁻¹ * (e * z) : Id.map (λ g, x⁻¹ * (g * z)) (mulRightInv _) - ... = leftDiv x z : Id.map (G.φ x⁻¹) (G.oneMul z) + ... = x⁻¹ * ((y * y⁻¹) * z) : ap (G.φ x⁻¹) (Id.inv (G.mulAssoc y y⁻¹ z)) + ... = x⁻¹ * (e * z) : ap (λ g, x⁻¹ * (g * z)) (mulRightInv _) + ... = leftDiv x z : ap (G.φ x⁻¹) (G.oneMul z) hott def chainRdiv (x y z : G.carrier) := calc (x / y) * (y / z) = (x * y⁻¹) * (y * z⁻¹) : Id.refl ... = x * (y⁻¹ * (y * z⁻¹)) : G.mulAssoc x y⁻¹ (y * z⁻¹) - ... = x * ((y⁻¹ * y) * z⁻¹) : Id.map (G.φ x) (Id.inv (G.mulAssoc y⁻¹ y z⁻¹)) - ... = x * (e * z⁻¹) : Id.map (λ g, x * (g * z⁻¹)) (G.mulLeftInv _) - ... = x / z : Id.map (G.φ x) (G.oneMul z⁻¹) + ... = x * ((y⁻¹ * y) * z⁻¹) : ap (G.φ x) (Id.inv (G.mulAssoc y⁻¹ y z⁻¹)) + ... = x * (e * z⁻¹) : ap (λ g, x * (g * z⁻¹)) (G.mulLeftInv _) + ... = x / z : ap (G.φ x) (G.oneMul z⁻¹) hott def conjugate.idem (x : G.carrier) := calc - conjugate x x = G.φ G.e x : Id.map (G.φ · x) (G.mulLeftInv x) + conjugate x x = G.φ G.e x : ap (G.φ · x) (G.mulLeftInv x) ... = x : G.oneMul x hott def conjugate.eq {x y : G.carrier} @@ -310,7 +311,7 @@ namespace Group transitivity; { symmetry; apply G.mulAssoc }; transitivity; exact p; transitivity; { transitivity; symmetry; apply G.oneMul; - apply Id.map (G.φ · x); symmetry; apply G.mulLeftInv y }; + apply ap (G.φ · x); symmetry; apply G.mulLeftInv y }; apply G.mulAssoc end @@ -331,17 +332,17 @@ namespace Group begin apply unitOfSqr; apply calc H.φ (φ e) (φ e) = φ (G.e * G.e) : Id.inv (p G.e G.e) - ... = φ G.e : Id.map φ (Id.inv unitSqr) + ... = φ G.e : ap φ (Id.inv unitSqr) end hott def homoRespectsInv {φ : G.carrier → H.carrier} (p : Π a b, φ (a * b) = φ a ∗ φ b) (x : G.carrier) : φ x⁻¹ = H.ι (φ x) := calc φ x⁻¹ = φ x⁻¹ ∗ H.e : Id.inv (H.mulOne (φ x⁻¹)) - ... = φ x⁻¹ ∗ (φ x ∗ H.ι (φ x)) : Id.map (H.φ (φ x⁻¹)) (Id.inv (mulRightInv (φ x))) + ... = φ x⁻¹ ∗ (φ x ∗ H.ι (φ x)) : ap (H.φ (φ x⁻¹)) (Id.inv (mulRightInv (φ x))) ... = φ x⁻¹ ∗ φ x ∗ H.ι (φ x) : Id.inv (H.mulAssoc _ _ _) - ... = φ (x⁻¹ * x) ∗ H.ι (φ x) : Id.map (H.φ · (H.ι (φ x))) (Id.inv (p x⁻¹ x)) - ... = φ G.e ∗ H.ι (φ x) : Id.map (λ y, φ y ∗ H.ι (φ x)) (G.mulLeftInv x) - ... = H.e ∗ H.ι (φ x) : Id.map (H.φ · (H.ι (φ x))) (homoRespectsUnit p) + ... = φ (x⁻¹ * x) ∗ H.ι (φ x) : ap (H.φ · (H.ι (φ x))) (Id.inv (p x⁻¹ x)) + ... = φ G.e ∗ H.ι (φ x) : ap (λ y, φ y ∗ H.ι (φ x)) (G.mulLeftInv x) + ... = H.e ∗ H.ι (φ x) : ap (H.φ · (H.ι (φ x))) (homoRespectsUnit p) ... = H.ι (φ x) : H.oneMul (H.ι (φ x)) hott def mkhomo (φ : G.carrier → H.carrier) @@ -371,7 +372,7 @@ namespace Group hott def homoRespectsDiv (φ : Hom G H) (x y : G.carrier) : φ.1 (x / y) = rightDiv (φ.1 x) (φ.1 y) := calc φ.1 (x / y) = φ.1 x ∗ φ.1 y⁻¹ : homoMul φ x y⁻¹ - ... = φ.1 x ∗ H.ι (φ.1 y) : Id.map (H.φ (φ.1 x)) (homoInv φ y) + ... = φ.1 x ∗ H.ι (φ.1 y) : ap (H.φ (φ.1 x)) (homoInv φ y) hott def Homo.zero : Hom G H := mkhomo (λ _, H.e) (λ _ _, Id.inv (H.oneMul H.e)) @@ -394,7 +395,7 @@ namespace Group hott def Homo.ofPath {G H : Group} (φ : G.carrier = H.carrier) (p : G.φ =[λ G, G → G → G, φ] H.φ) : Hom G H := begin fapply mkhomo; exact @transport _ (λ G, G) G.carrier H.carrier φ; - intros a b; transitivity; apply Id.map; apply bimap; + intros a b; transitivity; apply ap; apply bimap; iterate 2 { symmetry; apply @Equiv.transportForwardAndBack _ (λ G, G) _ _ φ }; transitivity; symmetry; apply Equiv.transportOverOperationPointwise G.φ; apply HITs.Interval.happly; apply HITs.Interval.happly; exact p @@ -484,4 +485,4 @@ namespace Group (begin intro b; induction b using Bool.casesOn <;> reflexivity end) end Group -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Differential.lean b/GroundZero/Algebra/Group/Differential.lean index 5bdbd0e..d115cd7 100644 --- a/GroundZero/Algebra/Group/Differential.lean +++ b/GroundZero/Algebra/Group/Differential.lean @@ -1,4 +1,6 @@ import GroundZero.Algebra.Group.Subgroup + +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero.Proto @@ -18,7 +20,7 @@ namespace Group hott def imImplKer {φ : Hom G G} (H : φ ⋅ φ = 0) : (im φ).set ⊆ (ker φ).set := begin intro x; fapply HITs.Merely.rec; apply G.hset; - intro ⟨y, p⟩; change _ = _; transitivity; apply Id.map _ (Id.inv p); + intro ⟨y, p⟩; change _ = _; transitivity; apply ap _ (Id.inv p); apply @idhom _ _ _ _ _ (φ ⋅ φ) 0; apply H end @@ -55,4 +57,4 @@ namespace Diff Group.imImplKer G.sqr end Diff -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Factor.lean b/GroundZero/Algebra/Group/Factor.lean index f05b1a5..5916369 100644 --- a/GroundZero/Algebra/Group/Factor.lean +++ b/GroundZero/Algebra/Group/Factor.lean @@ -2,7 +2,7 @@ import GroundZero.Algebra.Group.Subgroup import GroundZero.HITs.Quotient open GroundZero.Types.Equiv (biinv transport) -open GroundZero.Types.Id (map) +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero.Proto @@ -61,7 +61,7 @@ namespace Group noncomputable hott def factorSymm (φ : G.subgroup) (ρ : G ⊵ φ) : factorLeft G φ = factorRight G φ := begin - apply map GroundZero.HITs.Quotient; apply GroundZero.eqrel.eq; + apply ap GroundZero.HITs.Quotient; apply GroundZero.eqrel.eq; apply Theorems.funext; intro; apply Theorems.funext; intro; fapply Types.Sigma.prod; change ldiv φ _ _ = rdiv φ _ _; apply HITs.Interval.happly; apply HITs.Interval.happly; @@ -86,26 +86,26 @@ namespace Group apply calc b⁻¹ * (a⁻¹ * c * (d * b⁻¹)) * b = b⁻¹ * (a⁻¹ * c * d * b⁻¹) * b : - Id.map (b⁻¹ * · * b) (Id.inv (G.mulAssoc (a⁻¹ * c) d b⁻¹)) + ap (b⁻¹ * · * b) (Id.inv (G.mulAssoc (a⁻¹ * c) d b⁻¹)) ... = b⁻¹ * (a⁻¹ * c * d * b⁻¹ * b) : G.mulAssoc b⁻¹ (a⁻¹ * c * d * b⁻¹) b ... = b⁻¹ * (a⁻¹ * c * d * (b⁻¹ * b)) : - Id.map (G.φ b⁻¹) (G.mulAssoc (a⁻¹ * c * d) b⁻¹ b) + ap (G.φ b⁻¹) (G.mulAssoc (a⁻¹ * c * d) b⁻¹ b) ... = b⁻¹ * (a⁻¹ * c * d * e) : - @map G.carrier G.carrier _ _ (λ x, b⁻¹ * (a⁻¹ * c * d * x)) (G.mulLeftInv b) + @ap G.carrier G.carrier _ _ (λ x, b⁻¹ * (a⁻¹ * c * d * x)) (G.mulLeftInv b) ... = b⁻¹ * (a⁻¹ * c * d) : - Id.map (b⁻¹ * ·) (G.mulOne (a⁻¹ * c * d)) + ap (b⁻¹ * ·) (G.mulOne (a⁻¹ * c * d)) ... = b⁻¹ * (a⁻¹ * (c * d)) : - Id.map (b⁻¹ * ·) (G.mulAssoc a⁻¹ c d) + ap (b⁻¹ * ·) (G.mulAssoc a⁻¹ c d) ... = (b⁻¹ * a⁻¹) * (c * d) : Id.inv (G.mulAssoc b⁻¹ a⁻¹ (c * d)) ... = leftDiv (a * b) (c * d) : - Id.map (G.φ · (c * d)) (Id.inv (invExplode a b)); + ap (G.φ · (c * d)) (Id.inv (invExplode a b)); apply isNormalSubgroup.conj φ.2; apply φ.1.mul; { exact p }; { apply transport (· ∈ φ.set); apply calc (b * d⁻¹)⁻¹ = d⁻¹⁻¹ * b⁻¹ : invExplode b d⁻¹ - ... = d * b⁻¹ : Id.map (G.φ · b⁻¹) (invInv d); + ... = d * b⁻¹ : ap (G.φ · b⁻¹) (invInv d); apply φ.1.inv; apply (normalSubgroupCosets φ.2).left; exact q } } end @@ -117,9 +117,9 @@ namespace Group { intro x; apply HITs.Quotient.sound; apply transport (· ∈ φ.set); apply calc e = x⁻¹ * x : Id.inv (G.mulLeftInv x) - ... = e * x⁻¹ * x : Id.map (G.φ · x) (Id.inv (G.oneMul x⁻¹)) - ... = e⁻¹ * x⁻¹ * x : Id.map (λ y, y * x⁻¹ * x) unitInv - ... = (x * e)⁻¹ * x : Id.map (G.φ · x) (Id.inv (invExplode x e)); + ... = e * x⁻¹ * x : ap (G.φ · x) (Id.inv (G.oneMul x⁻¹)) + ... = e⁻¹ * x⁻¹ * x : ap (λ y, y * x⁻¹ * x) unitInv + ... = (x * e)⁻¹ * x : ap (G.φ · x) (Id.inv (invExplode x e)); apply φ.1.unit }; { intros; apply HITs.Quotient.set } end @@ -128,7 +128,7 @@ namespace Group begin fapply HITs.Quotient.indProp; { intro; change HITs.Quotient.elem _ = _; - apply map; apply G.oneMul }; + apply ap; apply G.oneMul }; { intros; apply HITs.Quotient.set } end @@ -137,7 +137,7 @@ namespace Group begin intro (x : HITs.Quotient _) (y : HITs.Quotient _) (z : HITs.Quotient _); induction x; induction y; induction z; - apply Id.map Factor.incl; apply G.mulAssoc; + apply ap Factor.incl; apply G.mulAssoc; -- ??? apply HITs.Quotient.set; apply propIsSet; apply HITs.Quotient.set; apply HITs.Quotient.set; apply propIsSet; apply HITs.Quotient.set; @@ -150,7 +150,7 @@ namespace Group { intro x; exact Factor.incl x⁻¹ }; { intros u v H; apply GroundZero.HITs.Quotient.sound; apply transport (· ∈ φ.set); symmetry; - apply map (G.φ · v⁻¹); apply invInv; + apply ap (G.φ · v⁻¹); apply invInv; apply (normalSubgroupCosets φ.2).left; exact H }; { apply GroundZero.HITs.Quotient.set } end @@ -159,7 +159,7 @@ namespace Group Π (x : factorLeft G φ), Factor.mul (Factor.inv x) x = Factor.one := begin intro (x : HITs.Quotient _); induction x; - apply Id.map Factor.incl; apply G.mulLeftInv; + apply ap Factor.incl; apply G.mulLeftInv; apply HITs.Quotient.set; apply propIsSet; apply HITs.Quotient.set end end @@ -186,7 +186,7 @@ namespace Group begin fapply HITs.Quotient.rec; exact f.1; { intros x y q; apply eqOfDivEq; change H.φ _ _ = _; - transitivity; apply Id.map (H.φ · (f.1 y)); + transitivity; apply ap (H.φ · (f.1 y)); symmetry; apply homoInv f; transitivity; symmetry; apply homoMul; apply p; apply q }; apply H.hset @@ -259,4 +259,4 @@ namespace Group end end Group -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Finite.lean b/GroundZero/Algebra/Group/Finite.lean index 98f55e0..fa41cd7 100644 --- a/GroundZero/Algebra/Group/Finite.lean +++ b/GroundZero/Algebra/Group/Finite.lean @@ -2,7 +2,7 @@ import GroundZero.Algebra.Group.Basic import GroundZero.Theorems.Nat open GroundZero.Types.Equiv (transport) -open GroundZero.Types.Id (map) +open GroundZero.Types.Id (ap) open GroundZero.Types namespace GroundZero @@ -15,7 +15,7 @@ namespace Types.Coproduct apply Equiv.trans; apply Types.Coproduct.symm; apply Equiv.trans; apply Types.Nat.equivAddition; assumption; apply Types.Coproduct.symm - end + end hott def eqvVariants (e : C + A ≃ C + B) (x : A) : (Σ y, e (Sum.inr x) = Sum.inr y) + @@ -130,23 +130,23 @@ namespace Algebra namespace Finite hott def plus : Π (n m : ℕ), Finite n + Finite m ≃ Finite (n + m) - | Nat.zero, m => Equiv.trans Types.Coproduct.empty (Equiv.idtoeqv (map Finite (Theorems.Nat.zeroPlus m)⁻¹)) + | Nat.zero, m => Equiv.trans Types.Coproduct.empty (Equiv.idtoeqv (ap Finite (Theorems.Nat.zeroPlus m)⁻¹)) | Nat.succ n, m => calc Finite (Nat.succ n) + Finite m ≃ Finite n + (𝟏 + Finite m) : Types.Coproduct.assoc ... ≃ Finite n + (Finite m + 𝟏) : Types.Coproduct.respectsEquivLeft Types.Coproduct.symm ... ≃ (Finite n + Finite m) + 𝟏 : Equiv.symm Types.Coproduct.assoc ... ≃ Finite (n + m) + 𝟏 : Types.Nat.equivAddition 𝟏 (plus n m) ... ≃ Finite (Nat.succ (n + m)) : Equiv.ideqv _ - ... ≃ Finite (Nat.succ n + m) : Equiv.idtoeqv (map Finite (Theorems.Nat.succPlus n m)⁻¹) + ... ≃ Finite (Nat.succ n + m) : Equiv.idtoeqv (ap Finite (Theorems.Nat.succPlus n m)⁻¹) hott def mul : Π (n m : ℕ), Finite n × Finite m ≃ Finite (n * m) - | Nat.zero, m => Equiv.trans Types.Product.destroy (Equiv.idtoeqv (map Finite (Theorems.Nat.zeroMul m)⁻¹)) + | Nat.zero, m => Equiv.trans Types.Product.destroy (Equiv.idtoeqv (ap Finite (Theorems.Nat.zeroMul m)⁻¹)) | Nat.succ n, m => calc Finite (Nat.succ n) × Finite m ≃ (Finite n × Finite m) + (𝟏 × Finite m) : Types.Product.distribRight ... ≃ Finite (n * m) + (𝟏 × Finite m) : Types.Nat.equivAddition _ (mul n m) ... ≃ Finite (n * m) + Finite m : Types.Coproduct.respectsEquivLeft (Structures.prodUnitEquiv _) ... ≃ Finite (n * m + m) : plus _ _ - ... ≃ Finite (Nat.succ n * m) : Equiv.idtoeqv (map Finite (Theorems.Nat.mulSucc n m)⁻¹) + ... ≃ Finite (Nat.succ n * m) : Equiv.idtoeqv (ap Finite (Theorems.Nat.mulSucc n m)⁻¹) end Finite namespace Group @@ -178,7 +178,7 @@ namespace Group begin apply Ens.ext; intro x; apply Prod.mk; { intro ⟨y, ⟨⟨z, ⟨p, q⟩⟩, r⟩⟩; apply transport (· ∈ coset (G.φ a b) φ.set); - symmetry; transitivity; { transitivity; exact r; apply map (G.φ a); exact q }; + symmetry; transitivity; { transitivity; exact r; apply ap (G.φ a); exact q }; symmetry; apply G.mulAssoc; apply coset.intro p }; { intro ⟨y, p⟩; apply transport (· ∈ coset a (coset b φ.set)); symmetry; transitivity; exact p.2; apply G.mulAssoc; @@ -197,21 +197,21 @@ namespace Group { apply φ.mul; { apply φ.inv; exact p }; exact q }; { transitivity; { symmetry; apply G.oneMul }; symmetry; transitivity; { symmetry; apply G.mulAssoc }; - apply map (G.φ · y); apply mulRightInv } } + apply ap (G.φ · y); apply mulRightInv } } end noncomputable hott def coset.uniq {x g₁ g₂ : G.carrier} : x ∈ coset g₁ φ.set → x ∈ coset g₂ φ.set → coset g₁ φ.set = coset g₂ φ.set := begin intro ⟨x₁, p⟩ ⟨x₂, q⟩; transitivity; - apply map (coset · φ.set); apply calc + apply ap (coset · φ.set); apply calc g₁ = G.φ g₁ G.e : (G.mulOne g₁)⁻¹ - ... = G.φ g₁ (G.φ x₁ (G.ι x₁)) : Id.map (G.φ g₁) (mulRightInv x₁)⁻¹ + ... = G.φ g₁ (G.φ x₁ (G.ι x₁)) : ap (G.φ g₁) (mulRightInv x₁)⁻¹ ... = G.φ (G.φ g₁ x₁) (G.ι x₁) : (G.mulAssoc _ _ _)⁻¹ - ... = G.φ (G.φ g₂ x₂) (G.ι x₁) : Id.map (G.φ · (G.ι x₁)) (p.2⁻¹ ⬝ q.2) + ... = G.φ (G.φ g₂ x₂) (G.ι x₁) : ap (G.φ · (G.ι x₁)) (p.2⁻¹ ⬝ q.2) ... = G.φ g₂ (G.φ x₂ (G.ι x₁)) : G.mulAssoc _ _ _; transitivity; { symmetry; apply coset.assoc }; - apply map; apply @coset.idem.{u, v} G φ; + apply ap; apply @coset.idem.{u, v} G φ; apply φ.mul; exact q.1; apply φ.inv; exact p.1 end end @@ -239,4 +239,4 @@ end Group end Algebra -end GroundZero \ No newline at end of file +end GroundZero diff --git a/GroundZero/Algebra/Group/Free.lean b/GroundZero/Algebra/Group/Free.lean index cfd6bb0..bc65546 100644 --- a/GroundZero/Algebra/Group/Free.lean +++ b/GroundZero/Algebra/Group/Free.lean @@ -1,6 +1,7 @@ import GroundZero.Algebra.Group.Basic + open GroundZero.Types.Equiv (biinv transport) -open GroundZero.Types.Id (map) +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero.Proto @@ -106,23 +107,23 @@ namespace Group mkhomo (rec G f) (recMul f) noncomputable def recβrule₁ {a b c : F.carrier ε} (f : ε → G.carrier) : - Id.map (rec G f) (mulAssoc a b c) = + ap (rec G f) (mulAssoc a b c) = G.mulAssoc (rec G f a) (rec G f b) (rec G f c) := by apply G.hset noncomputable def recβrule₂ {a : F.carrier ε} (f : ε → G.carrier) : - Id.map (rec G f) (oneMul a) = G.oneMul (rec G f a) := + ap (rec G f) (oneMul a) = G.oneMul (rec G f a) := by apply G.hset noncomputable def recβrule₃ {a : F.carrier ε} (f : ε → G.carrier) : - Id.map (rec G f) (mulOne a) = G.mulOne (rec G f a) := + ap (rec G f) (mulOne a) = G.mulOne (rec G f a) := by apply G.hset noncomputable def recβrule₄ {a : F.carrier ε} (f : ε → G.carrier) : - Id.map (rec G f) (mulLeftInv a) = G.mulLeftInv (rec G f a) := + ap (rec G f) (mulLeftInv a) = G.mulLeftInv (rec G f a) := by apply G.hset - noncomputable hott def ind_prop {π : F.carrier ε → Type v} + noncomputable hott def indΩ {π : F.carrier ε → Type v} (propπ : Π x, prop (π x)) (u : π unit) (η : Π {x}, π (elem x)) (m : Π {x y}, π x → π y → π (mul x y)) @@ -139,4 +140,4 @@ namespace Group end F end Group -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Isomorphism.lean b/GroundZero/Algebra/Group/Isomorphism.lean index 9bc249a..2b4836e 100644 --- a/GroundZero/Algebra/Group/Isomorphism.lean +++ b/GroundZero/Algebra/Group/Isomorphism.lean @@ -2,7 +2,7 @@ import GroundZero.Algebra.Group.Symmetric import GroundZero.Algebra.Group.Factor open GroundZero.Types.Equiv (biinv transport) -open GroundZero.Types.Id (map) +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero.Proto @@ -32,7 +32,7 @@ namespace Group apply HITs.Merely.elem; existsi x; reflexivity }; { intro x y (p : _ = _); fapply Sigma.prod; transitivity; symmetry; apply invInv; apply invEqOfMulEqOne; transitivity; - { apply map (H.φ · (φ.1 y)); symmetry; apply homoInv }; + { apply ap (H.φ · (φ.1 y)); symmetry; apply homoInv }; transitivity; { symmetry; apply homoMul }; apply p; apply HITs.Merely.uniq }; { apply Ens.hset; apply H.hset } @@ -45,7 +45,7 @@ namespace Group { fapply @HITs.Quotient.indProp _ _ (λ y, ker.encode _ = ker.encode y → _ = y) <;> intro y; { intro p; apply HITs.Quotient.sound; change _ = _; transitivity; apply homoMul; - transitivity; apply Id.map (H.φ · (φ.1 y)); + transitivity; apply ap (H.φ · (φ.1 y)); apply homoInv; apply mulEqOneOfInvEq; transitivity; apply invInv; apply (Sigma.sigmaEqOfEq p).1 }; @@ -118,4 +118,4 @@ namespace Group ⟨im (S.univ G), S.iso⟩ end Group -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Limited.lean b/GroundZero/Algebra/Group/Limited.lean index b4fc95f..69c301b 100644 --- a/GroundZero/Algebra/Group/Limited.lean +++ b/GroundZero/Algebra/Group/Limited.lean @@ -1,6 +1,7 @@ import GroundZero.Algebra.Group.Symmetric import GroundZero.Algebra.Reals +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero.HITs @@ -31,7 +32,7 @@ namespace GroundZero.Algebra exact b.1 x; apply ineqAdd; apply q.2; apply p.2 }; { intro a; apply Merely.lift; intro p; existsi p.1; intro x; apply Equiv.transport (R.ρ · _); - symmetry; transitivity; apply M.symm; apply Id.map (M.ρ _); + symmetry; transitivity; apply M.symm; apply ap (M.ρ _); symmetry; apply Equiv.forwardRight a; apply p.2 } end @@ -49,7 +50,7 @@ namespace GroundZero.Algebra begin apply sup.ssubset; intro x; apply Merely.lift; intro ⟨y, p⟩; existsi (Lim.ι φ).1.1 y; transitivity; apply M.1.symm; - transitivity; apply Id.map (M.1.ρ · _); + transitivity; apply ap (M.1.ρ · _); apply φ.1.forwardRight; exact p end @@ -106,7 +107,7 @@ namespace GroundZero.Algebra noncomputable hott def Lim.absolute (M : Metric⁎) : absolute (Lim M.1) (ω M) := begin apply (_, (_, _)); intro x; apply Prod.mk; apply ω.unitIfZero; - { intro p; transitivity; exact Id.map (ω M) p; apply ω.unit }; + { intro p; transitivity; exact ap (ω M) p; apply ω.unit }; intro x; symmetry; apply ω.inv; apply ω.mul end diff --git a/GroundZero/Algebra/Group/Periodic.lean b/GroundZero/Algebra/Group/Periodic.lean index b72858f..3052316 100644 --- a/GroundZero/Algebra/Group/Periodic.lean +++ b/GroundZero/Algebra/Group/Periodic.lean @@ -1,4 +1,5 @@ import GroundZero.Algebra.Group.Basic + open GroundZero.Structures open GroundZero.Types open GroundZero @@ -44,4 +45,4 @@ namespace Group P.unitSqr (λ | false => Id.refl | true => Id.refl) end Group -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Presentation.lean b/GroundZero/Algebra/Group/Presentation.lean index b51b5e6..02e3c0f 100644 --- a/GroundZero/Algebra/Group/Presentation.lean +++ b/GroundZero/Algebra/Group/Presentation.lean @@ -2,7 +2,7 @@ import GroundZero.Algebra.Group.Isomorphism import GroundZero.Algebra.Group.Free open GroundZero.Types.Equiv (biinv transport) -open GroundZero.Types.Id (map) +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero.Proto @@ -98,17 +98,17 @@ namespace Group begin intro x; fapply HITs.Merely.rec; apply Ens.prop; intro ⟨(a, b), q⟩; change _ = _; apply calc - f.1 x = f.1 (G.φ (G.φ a b) (G.φ (G.ι a) (G.ι b))) : Id.map f.1 (Id.inv q) + f.1 x = f.1 (G.φ (G.φ a b) (G.φ (G.ι a) (G.ι b))) : ap f.1 (Id.inv q) ... = H.φ (f.1 (G.φ a b)) (f.1 (G.φ (G.ι a) (G.ι b))) : homoMul f _ _ - ... = H.φ (f.1 (G.φ a b)) (H.φ (f.1 (G.ι a)) (f.1 (G.ι b))) : Id.map _ (homoMul f _ _) - ... = H.φ (f.1 (G.φ a b)) (H.φ (f.1 (G.ι b)) (f.1 (G.ι a))) : Id.map _ (ρ _ _) - ... = H.φ (f.1 (G.φ a b)) (f.1 (G.φ (G.ι b) (G.ι a))) : Id.map _ (homoMul f _ _)⁻¹ + ... = H.φ (f.1 (G.φ a b)) (H.φ (f.1 (G.ι a)) (f.1 (G.ι b))) : ap _ (homoMul f _ _) + ... = H.φ (f.1 (G.φ a b)) (H.φ (f.1 (G.ι b)) (f.1 (G.ι a))) : ap _ (ρ _ _) + ... = H.φ (f.1 (G.φ a b)) (f.1 (G.φ (G.ι b) (G.ι a))) : ap _ (homoMul f _ _)⁻¹ ... = f.1 (G.φ (G.φ a b) (G.φ (G.ι b) (G.ι a))) : Id.inv (homoMul f _ _) - ... = f.1 (G.φ (G.φ (G.φ a b) (G.ι b)) (G.ι a)) : Id.map f.1 (Id.inv (G.mulAssoc _ _ _)) - ... = f.1 (G.φ (G.φ a (G.φ b (G.ι b))) (G.ι a)) : @Id.map G.carrier H.carrier _ _ (λ x, f.1 (G.φ x (G.ι a))) (G.mulAssoc a b (G.ι b)) - ... = f.1 (G.φ (G.φ a G.e) (G.ι a)) : @Id.map G.carrier H.carrier _ _ (λ x, f.1 (G.φ (G.φ a x) (G.ι a))) (mulRightInv b) - ... = f.1 (G.φ a (G.ι a)) : @Id.map G.carrier H.carrier _ _ (λ x, f.1 (G.φ x (G.ι a))) (G.mulOne a) - ... = f.1 G.e : Id.map f.1 (mulRightInv a) + ... = f.1 (G.φ (G.φ (G.φ a b) (G.ι b)) (G.ι a)) : ap f.1 (Id.inv (G.mulAssoc _ _ _)) + ... = f.1 (G.φ (G.φ a (G.φ b (G.ι b))) (G.ι a)) : @ap G.carrier H.carrier _ _ (λ x, f.1 (G.φ x (G.ι a))) (G.mulAssoc a b (G.ι b)) + ... = f.1 (G.φ (G.φ a G.e) (G.ι a)) : @ap G.carrier H.carrier _ _ (λ x, f.1 (G.φ (G.φ a x) (G.ι a))) (mulRightInv b) + ... = f.1 (G.φ a (G.ι a)) : @ap G.carrier H.carrier _ _ (λ x, f.1 (G.φ x (G.ι a))) (G.mulOne a) + ... = f.1 G.e : ap f.1 (mulRightInv a) ... = H.e : homoUnit f end end @@ -174,4 +174,4 @@ namespace Group end end Group -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Product.lean b/GroundZero/Algebra/Group/Product.lean index e1f9654..5b80484 100644 --- a/GroundZero/Algebra/Group/Product.lean +++ b/GroundZero/Algebra/Group/Product.lean @@ -1,4 +1,6 @@ import GroundZero.Algebra.Group.Basic + +open GroundZero.Types.Id (ap) open GroundZero.Types namespace GroundZero.Algebra @@ -27,11 +29,11 @@ namespace Group change F.φ (φ.1 _) (ψ.1 _) = F.φ (F.φ _ _) (F.φ _ _); transitivity; apply Equiv.bimap F.φ <;> apply homoMul; transitivity; apply F.mulAssoc; - transitivity; apply Id.map (F.φ (φ.1 _)); + transitivity; apply ap (F.φ (φ.1 _)); transitivity; apply ρ; apply F.mulAssoc; transitivity; symmetry; apply F.mulAssoc; - apply Id.map; apply ρ + apply ap; apply ρ end end Group -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Semidirect.lean b/GroundZero/Algebra/Group/Semidirect.lean index 96bfb81..d624cc1 100644 --- a/GroundZero/Algebra/Group/Semidirect.lean +++ b/GroundZero/Algebra/Group/Semidirect.lean @@ -1,5 +1,6 @@ import GroundZero.Algebra.Group.Automorphism +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero @@ -15,30 +16,30 @@ namespace Group (λ (n₁, h₁) (n₂, h₂) (n₃, h₃), begin apply Product.prod; { transitivity; apply N.mulAssoc; - apply Id.map (N.φ n₁); symmetry; + apply ap (N.φ n₁); symmetry; transitivity; apply isoMul; - apply Id.map; symmetry; + apply ap; symmetry; transitivity; apply HITs.Interval.happly; - apply Id.map; apply homoMul; reflexivity }; + apply ap; apply homoMul; reflexivity }; { apply H.mulAssoc } end) (λ (n, h), begin apply Product.prod; { transitivity; apply N.oneMul; transitivity; apply HITs.Interval.happly; - apply Id.map; apply homoUnit; reflexivity }; + apply ap; apply homoUnit; reflexivity }; { apply H.oneMul } end) (λ (n, h), begin apply Product.prod; - { transitivity; apply Id.map (N.φ n); + { transitivity; apply ap (N.φ n); apply isoUnit (φ.1 h); apply N.mulOne }; { apply H.mulOne } end) (λ ⟨n, h⟩, begin apply Product.prod; { transitivity; symmetry; apply isoMul; - transitivity; apply Id.map; + transitivity; apply ap; apply N.mulLeftInv; apply isoUnit }; { apply H.mulLeftInv } end) @@ -47,4 +48,4 @@ namespace Group notation H " ⋉" "[" φ "] " N => Semidirect (N := N) (H := H) φ end Group -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Subgroup.lean b/GroundZero/Algebra/Group/Subgroup.lean index ae58fc7..99ce523 100644 --- a/GroundZero/Algebra/Group/Subgroup.lean +++ b/GroundZero/Algebra/Group/Subgroup.lean @@ -1,7 +1,7 @@ import GroundZero.Algebra.Group.Basic open GroundZero.Types.Equiv (biinv transport) -open GroundZero.Types.Id (map) +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero.Proto @@ -78,8 +78,8 @@ namespace Group intro h; apply H; apply transport (· ∈ φ.set); apply calc g * (g⁻¹ * n) = (g * g⁻¹) * n : Id.inv (G.mulAssoc g g⁻¹ n) - ... = e * n : Id.map (G.φ · n) (mulRightInv g) - ... = (g⁻¹ * g) * n : Id.map (G.φ · n) (Id.inv (G.mulLeftInv g)) + ... = e * n : ap (G.φ · n) (mulRightInv g) + ... = (g⁻¹ * g) * n : ap (G.φ · n) (Id.inv (G.mulLeftInv g)) ... = g⁻¹ * (g * n) : G.mulAssoc g⁻¹ g n; apply H; assumption end @@ -89,14 +89,14 @@ namespace Group apply Prod.mk <;> intro h; { change (x * y⁻¹) ∈ φ.set; apply transport (· ∈ φ.set); apply calc x * (y⁻¹ * x) * x⁻¹ = x * (y⁻¹ * x * x⁻¹) : G.mulAssoc x (leftDiv y x) x⁻¹ - ... = x * y⁻¹ : Id.map (G.φ x) (Id.inv (cancelRight y⁻¹ x)); + ... = x * y⁻¹ : ap (G.φ x) (Id.inv (cancelRight y⁻¹ x)); apply conjugateEqv H; apply isNormalSubgroup.conj H; apply transport (· ∈ φ.set); apply invMulInv; apply φ.inv; assumption }; { change (x⁻¹ * y) ∈ φ.set; apply transport (· ∈ φ.set); apply calc x⁻¹ * (y * x⁻¹) * x = x⁻¹ * (y * x⁻¹ * x) : G.mulAssoc x⁻¹ (y / x) x - ... = x⁻¹ * y : Id.map (G.φ x⁻¹) (Id.inv (cancelLeft y x)); + ... = x⁻¹ * y : ap (G.φ x⁻¹) (Id.inv (cancelLeft y x)); apply isNormalSubgroup.conj H; apply transport (· ∈ φ.set); apply mulInvInv; apply φ.inv; assumption } end @@ -143,7 +143,7 @@ namespace Group end hott def Subgroup.ext : Π (φ ψ : G.subgroup), φ.set = ψ.set → Subgroup G φ = Subgroup G ψ := - begin intro ⟨φ, p⟩ ⟨ψ, q⟩ r; apply Id.map (Subgroup G); apply subgroup.ext r end + begin intro ⟨φ, p⟩ ⟨ψ, q⟩ r; apply ap (Subgroup G); apply subgroup.ext r end hott def inter (φ ψ : G.subgroup) : subgroup (Subgroup G ψ) := begin @@ -186,13 +186,13 @@ namespace Group intros x h; change _ = _; apply calc φ.1 x⁻¹ = H.ι (φ.1 x) : homoInv φ x - ... = H.ι H.e : Id.map H.ι h + ... = H.ι H.e : ap H.ι h ... = H.e : Id.inv unitInv end), begin intro n g p; have r := Id.inv (homoMul φ n g) ⬝ p; apply calc φ.1 (g * n) = φ.1 g ∗ φ.1 n : homoMul φ g n - ... = φ.1 g ∗ H.ι (φ.1 g) : Id.map (H.φ (φ.1 g)) (eqInvOfMulEqOne r) + ... = φ.1 g ∗ H.ι (φ.1 g) : ap (H.φ (φ.1 g)) (eqInvOfMulEqOne r) ... = H.e : Group.mulRightInv _ end⟩ @@ -215,7 +215,7 @@ namespace Group (begin intro a (p : ∥_∥); induction p; case elemπ p => { apply HITs.Merely.elem; existsi p.1⁻¹; - transitivity; apply homoInv; apply map _ p.2 }; + transitivity; apply homoInv; apply ap _ p.2 }; apply HITs.Merely.uniq end) end @@ -230,23 +230,23 @@ namespace Group { intro; transitivity; apply G.oneMul; symmetry; apply G.mulOne }; { intros a b g h c; symmetry; apply calc G.φ c (G.φ a b) = G.φ (G.φ c a) b : Id.inv (G.mulAssoc _ _ _) - ... = G.φ (G.φ a c) b : Id.map (G.φ · b) (Id.inv (g c)) + ... = G.φ (G.φ a c) b : ap (G.φ · b) (Id.inv (g c)) ... = G.φ a (G.φ c b) : G.mulAssoc _ _ _ - ... = G.φ a (G.φ b c) : Id.map (G.φ a) (Id.inv (h c)) + ... = G.φ a (G.φ b c) : ap (G.φ a) (Id.inv (h c)) ... = G.φ (G.φ a b) c : Id.inv (G.mulAssoc _ _ _) }; { intros a g b; apply calc - G.φ (G.ι a) b = G.φ (G.ι a) (G.ι (G.ι b)) : Id.map (G.φ (G.ι a)) (Id.inv (invInv b)) + G.φ (G.ι a) b = G.φ (G.ι a) (G.ι (G.ι b)) : ap (G.φ (G.ι a)) (Id.inv (invInv b)) ... = G.ι (G.φ (G.ι b) a) : Id.inv (invExplode _ _) - ... = G.ι (G.φ a (G.ι b)) : Id.map G.ι (Id.inv (g (G.ι b))) + ... = G.ι (G.φ a (G.ι b)) : ap G.ι (Id.inv (g (G.ι b))) ... = G.φ (G.ι (G.ι b)) (G.ι a) : invExplode _ _ - ... = G.φ b (G.ι a) : Id.map (G.φ · (G.ι a)) (invInv b) } + ... = G.φ b (G.ι a) : ap (G.φ · (G.ι a)) (invInv b) } end, begin intros g h r z; have p := Id.inv (G.mulAssoc g h g) ⬝ r g; have q := mulCancelLeft p; - transitivity; apply Id.map (G.φ · z); apply q ; - symmetry; transitivity; apply Id.map (G.φ z); + transitivity; apply ap (G.φ · z); apply q ; + symmetry; transitivity; apply ap (G.φ z); apply q; symmetry; apply r end⟩ @@ -267,7 +267,7 @@ namespace Group transitivity; apply G.mulOne; transitivity; symmetry; apply G.oneMul; symmetry; transitivity; symmetry; apply G.mulAssoc; - symmetry; apply Id.map (G.φ · g); assumption + symmetry; apply ap (G.φ · g); assumption end⟩ hott def univ (G : Group) : G.normal := @@ -300,4 +300,4 @@ namespace Group ⟨λ a, ∥(Σ x y, x ∈ φ × y ∈ ψ × x * y = a)∥, λ _, HITs.Merely.uniq⟩ end Group -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Symmetric.lean b/GroundZero/Algebra/Group/Symmetric.lean index 213e505..832b855 100644 --- a/GroundZero/Algebra/Group/Symmetric.lean +++ b/GroundZero/Algebra/Group/Symmetric.lean @@ -1,4 +1,6 @@ import GroundZero.Algebra.Group.Subgroup + +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Theorems open GroundZero.Types @@ -40,10 +42,10 @@ namespace Group begin existsi (G.φ x ·); apply Prod.mk <;> existsi (G.φ (G.ι x) ·) <;> intro y; { transitivity; { symmetry; apply G.mulAssoc }; - transitivity; { apply Id.map (G.φ · y); apply G.mulLeftInv }; + transitivity; { apply ap (G.φ · y); apply G.mulLeftInv }; apply G.oneMul }; { transitivity; { symmetry; apply G.mulAssoc }; - transitivity; { apply Id.map (G.φ · y); apply mulRightInv }; + transitivity; { apply ap (G.φ · y); apply mulRightInv }; apply G.oneMul } end @@ -71,4 +73,4 @@ namespace Group end end Group -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Group/Z.lean b/GroundZero/Algebra/Group/Z.lean index 869d37b..4ba6c1f 100644 --- a/GroundZero/Algebra/Group/Z.lean +++ b/GroundZero/Algebra/Group/Z.lean @@ -3,6 +3,7 @@ import GroundZero.HITs.Circle open GroundZero.Structures GroundZero.Types.Equiv open GroundZero.Types GroundZero.HITs +open GroundZero.Types.Id (ap) namespace GroundZero.Algebra @@ -23,7 +24,7 @@ noncomputable hott def helix.loop {G : Group} (z x : G.carrier) : transport (helix z) Circle.loop x = G.φ z x := begin transitivity; apply Equiv.transportToTransportconst; - transitivity; apply Id.map (transportconst · x); + transitivity; apply ap (transportconst · x); apply Circle.recβrule₂; apply ua.transportRule end @@ -31,8 +32,8 @@ noncomputable hott def helix.loopInv {G : Group} (z x : G.carrier) : transport (helix z) Circle.loop⁻¹ x = G.φ (G.ι z) x := begin transitivity; apply Equiv.transportToTransportconst; - transitivity; apply Id.map (transportconst · x); - transitivity; apply Id.mapInv; apply Id.map; + transitivity; apply ap (transportconst · x); + transitivity; apply Id.mapInv; apply ap; apply Circle.recβrule₂; apply ua.transportInvRule end @@ -49,18 +50,18 @@ noncomputable hott def power.mul {G : Group} (z : G.carrier) : begin intro p q; fapply @Circle.Ωind₁ (λ p, power z (p ⬝ q) = G.φ (power z p) (power z q)) <;> clear p; { symmetry; apply G.oneMul }; - { intros p ih; transitivity; apply Id.map; transitivity; - symmetry; apply Id.assoc; transitivity; apply Id.map (Id.trans p); + { intros p ih; transitivity; apply ap; transitivity; + symmetry; apply Id.assoc; transitivity; apply ap (Id.trans p); apply Circle.comm; apply Id.assoc; transitivity; apply power.succ; - transitivity; apply Id.map (G.φ z); exact ih; + transitivity; apply ap (G.φ z); exact ih; transitivity; symmetry; apply G.mulAssoc; - apply Id.map (G.φ · _); symmetry; apply power.succ }; - { intros p ih; transitivity; apply Id.map; transitivity; - symmetry; apply Id.assoc; transitivity; apply Id.map (Id.trans p); + apply ap (G.φ · _); symmetry; apply power.succ }; + { intros p ih; transitivity; apply ap; transitivity; + symmetry; apply Id.assoc; transitivity; apply ap (Id.trans p); apply Circle.comm; apply Id.assoc; transitivity; apply power.pred; - transitivity; apply Id.map (G.φ (G.ι z)); exact ih; + transitivity; apply ap (G.φ (G.ι z)); exact ih; transitivity; symmetry; apply G.mulAssoc; - apply Id.map (G.φ · _); symmetry; apply power.pred } + apply ap (G.φ · _); symmetry; apply power.pred } end noncomputable hott def ZΩ.rec {G : Group} (z : G.carrier) : Group.Hom ZΩ G := @@ -75,7 +76,7 @@ begin { intros p ih; transitivity; apply power.succ; transitivity; apply G.oneMul; exact ih }; { intros p ih; transitivity; apply power.pred; - transitivity; apply Id.map (G.φ · _); + transitivity; apply ap (G.φ · _); symmetry; apply Group.unitInv; transitivity; apply G.oneMul; exact ih } end @@ -89,6 +90,6 @@ by reflexivity -- something is really wrong with this thing --noncomputable hott def ZΩ.zeroMul (p : ZΩ.carrier) : ZΩ.mul Id.refl p = Id.refl := ---@Id.map (Group.S ZΩ.1.zero).carrier ZΩ.carrier _ _ (λ e, e.1 Id.refl) (power.one p) +--@ap (Group.S ZΩ.1.zero).carrier ZΩ.carrier _ _ (λ e, e.1 Id.refl) (power.one p) -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Monoid.lean b/GroundZero/Algebra/Monoid.lean index 17bb81c..3922610 100644 --- a/GroundZero/Algebra/Monoid.lean +++ b/GroundZero/Algebra/Monoid.lean @@ -1,6 +1,8 @@ import GroundZero.Algebra.Basic import GroundZero.HITs.Trunc + open GroundZero GroundZero.Types +open GroundZero.Types.Id (ap) namespace GroundZero.Algebra @@ -58,7 +60,7 @@ hott def Term.ofAppend (M : Monoid) : Π (xs ys : List M.carrier), Term.toMonoid M (Term.ofList (xs ++ ys)) = M.φ (Term.toMonoid M (Term.ofList xs)) (Term.toMonoid M (Term.ofList ys)) | [], ys => (M.oneMul _)⁻¹ -| x :: xs, ys => Id.map (M.φ x) (ofAppend M xs ys) ⬝ (M.mulAssoc _ _ _)⁻¹ +| x :: xs, ys => ap (M.φ x) (ofAppend M xs ys) ⬝ (M.mulAssoc _ _ _)⁻¹ hott def Term.sec (M : Monoid) : Term.toMonoid M ∘ Term.ofList ∘ Term.toList ~ Term.toMonoid M | Term.e => Id.refl @@ -67,7 +69,7 @@ hott def Term.sec (M : Monoid) : Term.toMonoid M ∘ Term.ofList ∘ Term.toList hott def Term.solve (M : Monoid) (τ₁ τ₂ : Term M.carrier) (ρ : τ₁.toList = τ₂.toList) : τ₁.toMonoid M = τ₂.toMonoid M := -(Term.sec M τ₁)⁻¹ ⬝ Id.map (Term.toMonoid M ∘ Term.ofList) ρ ⬝ Term.sec M τ₂ +(Term.sec M τ₁)⁻¹ ⬝ ap (Term.toMonoid M ∘ Term.ofList) ρ ⬝ Term.sec M τ₂ hott def Term.example (M : Monoid) (x y z : M.carrier) : M.φ (M.φ (M.φ x (M.φ y M.e)) M.e) (M.φ z M.e) = M.φ x (M.φ y z) := @@ -76,6 +78,6 @@ Term.solve M (Term.φ (Term.φ (Term.φ (Term.ι x) (Term.φ (Term.ι y) Term.e) hott def Term.ret {A : Type u} : Term.toList ∘ @Term.ofList A ~ id | [] => Id.refl -| x :: xs => Id.map (List.cons x) (ret xs) +| x :: xs => ap (List.cons x) (ret xs) -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Orgraph.lean b/GroundZero/Algebra/Orgraph.lean index 880249b..ed82d3c 100644 --- a/GroundZero/Algebra/Orgraph.lean +++ b/GroundZero/Algebra/Orgraph.lean @@ -2,6 +2,7 @@ import GroundZero.Theorems.Classical import GroundZero.Algebra.Ring open GroundZero.Types GroundZero.Proto +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Theorems open GroundZero.HITs @@ -158,7 +159,7 @@ namespace GroundZero.Algebra apply Equiv.transportconst; apply Equiv.bimap; symmetry; apply @Group.cancelRight T.τ⁺ a c; symmetry; apply @Group.cancelRight T.τ⁺ b c; - apply Id.map (λ x, x - c) q; apply orfield.leOverAdd; exact p.2 + apply ap (λ x, x - c) q; apply orfield.leOverAdd; exact p.2 end hott def ltOverAddLeft (T : Overring) [orfield T] (a b c : T.carrier) (p : a < b) : c + a < c + b := @@ -196,7 +197,7 @@ namespace GroundZero.Algebra change T.carrier; exact -b; change T.carrier; exact -a; apply T.κ.prop; { intro ih; induction ih; assumption; match @Classical.lem (a = b) (T.hset _ _) with | Sum.inl r₁ => _ | Sum.inr r₂ => _; - apply eqImplReflRel T.κ; symmetry; apply Id.map T.τ.neg r₁; + apply eqImplReflRel T.κ; symmetry; apply ap T.τ.neg r₁; apply Empty.elim; apply (_ : T.σ 0 0).1; reflexivity; apply Equiv.transportconst; apply Equiv.bimap; apply @Group.mulRightInv T.τ⁺; exact a; @@ -359,4 +360,4 @@ namespace GroundZero.Algebra hott def gtIfGtZero (T : Overring) [orfield T] {a b : T.carrier} (H : 0 ≤ b - a) : a ≤ b := begin apply Equiv.transport (λ c, c ≤ b); apply T.τ⁺.oneMul; apply addLeIfSubGe; exact H end -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Reals.lean b/GroundZero/Algebra/Reals.lean index 817da11..8dde452 100644 --- a/GroundZero/Algebra/Reals.lean +++ b/GroundZero/Algebra/Reals.lean @@ -1,6 +1,7 @@ import GroundZero.Algebra.Orgraph import GroundZero.Theorems.Nat +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Theorems open GroundZero.Types @@ -54,7 +55,7 @@ namespace GroundZero.Algebra noncomputable hott def N.incl.add (n : ℕ) : Π m, N.incl (n + m) = N.incl n + N.incl m | Nat.zero => Id.inv (R.τ⁺.mulOne _) - | Nat.succ m => @Id.map ℝ ℝ _ _ (λ r, r + 1) (add n m) ⬝ R.τ⁺.mulAssoc _ _ _ + | Nat.succ m => @ap ℝ ℝ _ _ (λ r, r + 1) (add n m) ⬝ R.τ⁺.mulAssoc _ _ _ noncomputable hott def leAddOne (x : ℝ) : R.ρ x (x + 1) := begin @@ -69,7 +70,7 @@ namespace GroundZero.Algebra | 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.succ m => λ p, orfield.leOverAdd (N.incl n) (N.incl m) 1 (lt n m (Id.map Nat.pred 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.κ φ) : Σ M, exact (@Majorant R.κ φ) M := @@ -136,10 +137,10 @@ namespace GroundZero.Algebra noncomputable hott def R.totalIsProp (x y : ℝ) : prop (R.ρ x y + (x > y)) := begin intros p q; match p, q with - | Sum.inl p₁, Sum.inl q₁ => { apply Id.map; apply R.κ.prop } + | 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.inr (p, p'), Sum.inr (q, q') => { apply Id.map; apply Product.prod; apply notIsProp; apply R.κ.prop } + | Sum.inr (p, p'), Sum.inr (q, q') => { apply ap; apply Product.prod; apply notIsProp; apply R.κ.prop } end noncomputable hott def R.total (x y : ℝ) : R.ρ x y + (x > y) := @@ -168,7 +169,7 @@ namespace GroundZero.Algebra noncomputable hott def R.zeroEqMinusZero {x : ℝ} (p : x = 0) : x = -x := begin transitivity; exact p; symmetry; - transitivity; apply Id.map; exact p; + transitivity; apply ap; exact p; symmetry; apply @Group.unitInv R.τ⁺ end @@ -237,12 +238,12 @@ namespace GroundZero.Algebra match R.total 0 x with | Sum.inl p => { apply Equiv.transport (R.ρ · x); symmetry; - apply Id.map; apply abs.pos p; apply @transitive.trans R.κ; + apply ap; apply abs.pos p; apply @transitive.trans R.κ; apply R.zeroLeImplZeroGeMinus p; assumption } | Sum.inr q => { apply Equiv.transport (R.ρ · x); symmetry; - transitivity; apply Id.map; apply abs.neg q.2; + transitivity; apply ap; apply abs.neg q.2; apply @Group.invInv R.τ⁺; apply @reflexive.refl R.κ } end @@ -352,10 +353,10 @@ namespace GroundZero.Algebra { apply (A.2.1 (G.φ x (G.ι y))).right; induction p; apply Group.mulRightInv } }; { intros x y; transitivity; apply A.2.2.1 (G.φ x (G.ι y)); - apply Id.map A.1; transitivity; apply Group.invExplode; - apply Id.map (λ z, G.φ z (G.ι x)); apply Group.invInv }; + apply ap A.1; transitivity; apply Group.invExplode; + apply ap (λ z, G.φ z (G.ι x)); apply Group.invInv }; { intros x y z; apply Equiv.transport (R.ρ · _); - apply Id.map A.1; apply Group.chainRdiv x y z; apply A.2.2.2 } + apply ap A.1; apply Group.chainRdiv x y z; apply A.2.2.2 } end hott def Absolute.space (G : Group) (A : Absolute G) : Metric := @@ -368,10 +369,10 @@ namespace GroundZero.Algebra { apply geIfMinusLe; apply Equiv.transport (λ w, R.ρ w _); symmetry; apply @Group.mulInvInv R.τ⁺; apply subLeIfAddGeRev; apply Equiv.transport (λ w, R.ρ (A.1 y) (w + A.1 (G.φ x y))); symmetry; apply A.2.2.1; - apply Equiv.transport (R.ρ · _); apply Id.map A.1; symmetry; apply Group.revCancelLeft x y; apply A.2.2.2 }; + apply Equiv.transport (R.ρ · _); apply ap A.1; symmetry; apply Group.revCancelLeft x y; apply A.2.2.2 }; { apply subLeIfAddGe; apply Equiv.transport (λ w, R.ρ (A.1 x) (A.1 (G.φ x y) + w)); symmetry; apply A.2.2.1; apply Equiv.transport (R.ρ · _); - apply Id.map A.1; symmetry; apply Group.cancelRight x y; apply A.2.2.2 } + apply ap A.1; symmetry; apply Group.cancelRight x y; apply A.2.2.2 } end noncomputable hott def triangle (x y : ℝ) : R.ρ (abs (x + y)) (abs x + abs y) := @@ -386,7 +387,7 @@ namespace GroundZero.Algebra noncomputable hott def R.absolute : absolute R.τ⁺ abs := begin apply (_, (_, _)); intro; apply Prod.mk; apply abs.zeroIf; - { intro p; transitivity; exact Id.map abs p; apply abs.zero }; + { intro p; transitivity; exact ap abs p; apply abs.zero }; apply abs.even; apply triangle end @@ -461,4 +462,4 @@ namespace GroundZero.Algebra apply subLeIfAddGe; apply Equiv.transport (R.ρ · _); apply R.τ⁺.mulOne; apply leOverAddLeft; exact p end -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Algebra/Ring.lean b/GroundZero/Algebra/Ring.lean index 8dae933..cbcaec8 100644 --- a/GroundZero/Algebra/Ring.lean +++ b/GroundZero/Algebra/Ring.lean @@ -1,7 +1,7 @@ import GroundZero.Algebra.Group.Factor open GroundZero.Algebra.Group (factorLeft) open GroundZero.Types.Equiv (transport) -open GroundZero.Types.Id (map) +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero @@ -169,21 +169,21 @@ section begin apply @Group.unitOfSqr T⁺; transitivity; symmetry; apply ring.distribLeft; - apply map (T.ψ a); apply T.zeroAdd + apply ap (T.ψ a); apply T.zeroAdd end hott def ring.zeroMul (a : T.carrier) : 0 * a = 0 := begin apply @Group.unitOfSqr T⁺; transitivity; symmetry; apply T.distribRight; - apply map (· * a); apply T.addZero + apply ap (· * a); apply T.addZero end hott def ring.mulNeg (a b : T.carrier) : a * (-b) = -(a * b) := begin apply @Group.eqInvOfMulEqOne T⁺; transitivity; symmetry; apply T.distribLeft; transitivity; - apply map (T.ψ a); apply T.addLeftNeg; + apply ap (T.ψ a); apply T.addLeftNeg; apply ring.mulZero end @@ -191,16 +191,16 @@ section begin apply @Group.eqInvOfMulEqOne T⁺; transitivity; symmetry; apply T.distribRight; transitivity; - apply map (· * b); apply T.addLeftNeg; apply ring.zeroMul + apply ap (· * b); apply T.addLeftNeg; apply ring.zeroMul end hott def ring.subDistribLeft (a b c : T.carrier) := calc a * (b - c) = a * b + a * (-c) : T.distribLeft a b (T.neg c) - ... = a * b - a * c : Id.map (T.φ (T.ψ a b)) (ring.mulNeg a c) + ... = a * b - a * c : ap (T.φ (T.ψ a b)) (ring.mulNeg a c) hott def ring.subDistribRight (a b c : T.carrier) := calc (a - b) * c = a * c + (-b) * c : T.distribRight a (T.neg b) c - ... = a * c - b * c : Id.map (T.φ (T.ψ a c)) (ring.negMul b c) + ... = a * c - b * c : ap (T.φ (T.ψ a c)) (ring.negMul b c) end class ring.assoc (T : Prering) := @@ -233,7 +233,7 @@ class field (T : Prering) extends ring.assoc T, ring.divisible T, ring.comm T := hott def ring.minusOneSqr (T : Prering) [ring T] [ring.monoid T] : @Id T.carrier ((-1) * (-1)) 1 := begin transitivity; apply ring.mulNeg; - transitivity; apply Id.map T.neg; + transitivity; apply ap T.neg; apply ring.monoid.mulOne; apply @Group.invInv T⁺ end @@ -243,20 +243,20 @@ hott def field.properMul {T : Prering} [field T] {a b : T.carrier} : begin intros p q r; apply @field.nontrivial T _; transitivity; { symmetry; apply ring.divisible.mulLeftInv b q }; - transitivity; { apply map (· * b); symmetry; apply ring.monoid.mulOne }; + transitivity; { apply ap (· * b); symmetry; apply ring.monoid.mulOne }; transitivity; apply ring.assoc.mulAssoc; - transitivity; apply map (λ y, b⁻¹ * (y * b)); + transitivity; apply ap (λ y, b⁻¹ * (y * b)); { symmetry; apply ring.divisible.mulLeftInv a p }; - transitivity; apply map (T.ψ _); apply ring.assoc.mulAssoc; + transitivity; apply ap (T.ψ _); apply ring.assoc.mulAssoc; transitivity; { symmetry; apply ring.assoc.mulAssoc }; - transitivity; apply map; exact r; apply ring.mulZero + transitivity; apply ap; exact r; apply ring.mulZero end hott def field.propInv {T : Prering} [field T] {a : T.carrier} : T.isproper a → T.isproper a⁻¹ := begin intros p q; apply @field.nontrivial T _; transitivity; { symmetry; apply ring.divisible.mulLeftInv a p }; - transitivity; apply map (· * a); exact q; apply ring.zeroMul + transitivity; apply ap (· * a); exact q; apply ring.zeroMul end hott def field.mul (T : Prering) [field T] : @@ -282,7 +282,7 @@ postfix:max "ˣ" => multiplicative -- voilà, no need to repeat a bunch of lemmas hott def field.mulRightInv (T : Prering) [field T] {x : T.carrier} (p : T.isproper x) : x * x⁻¹ = 1 := -Id.map Sigma.fst (Tˣ.mulRightInv ⟨x, p⟩) +ap Sigma.fst (Tˣ.mulRightInv ⟨x, p⟩) class lid (T : Prering) [ring T] (φ : T⁺.subgroup) := (ideal : Π r i, i ∈ φ.set → T.ψ r i ∈ φ.set) @@ -313,18 +313,18 @@ namespace Ring { let φ' := T⁺.leftDiv; change T.φ (φ' (T.ψ a₁ a₂) (T.ψ a₁ b₂)) (φ' (T.ψ a₁ b₂) (T.ψ b₁ b₂)) = _; transitivity; apply T⁺.mulAssoc; - transitivity; apply Id.map (T.φ _); + transitivity; apply ap (T.φ _); transitivity; symmetry; apply T⁺.mulAssoc; - apply Id.map (λ z, T.φ z (T.ψ b₁ b₂)); - apply Group.mulRightInv; apply Id.map; apply T.zeroAdd }; + apply ap (λ z, T.φ z (T.ψ b₁ b₂)); + apply Group.mulRightInv; apply ap; apply T.zeroAdd }; apply φ.mul; { apply transport (· ∈ φ.set); transitivity; apply T.distribLeft a₁ (T.neg a₂) b₂; - apply Id.map (λ z, T.φ z (T.ψ a₁ b₂)); + apply ap (λ z, T.φ z (T.ψ a₁ b₂)); apply ring.mulNeg; apply ideal.left; exact q }; { apply transport (· ∈ φ.set); transitivity; apply T.distribRight (T.neg a₁) b₁ b₂; - apply Id.map (λ z, T.φ z (T.ψ b₁ b₂)); + apply ap (λ z, T.φ z (T.ψ b₁ b₂)); apply ring.negMul; apply ideal.right; exact p } } end end Ring diff --git a/GroundZero/Algebra/Transformational.lean b/GroundZero/Algebra/Transformational.lean index abdae60..bdeb04b 100644 --- a/GroundZero/Algebra/Transformational.lean +++ b/GroundZero/Algebra/Transformational.lean @@ -2,6 +2,7 @@ import GroundZero.Algebra.Group.Product import GroundZero.Algebra.Group.Action open GroundZero.Algebra.Group +open GroundZero.Types.Id (ap) open GroundZero.Types.Equiv open GroundZero.Structures open GroundZero.Types @@ -82,10 +83,10 @@ namespace GroundZero.Algebra end hott def invTrans (x y z : M) : (L.ι x y)⁻¹ * (L.ι x z) = L.ι y z := - begin transitivity; apply Id.map (G.φ · (L.ι x z)); apply inv; apply L.trans end + begin transitivity; apply ap (G.φ · (L.ι x z)); apply inv; apply L.trans end hott def transInv (x y z : M) : (L.ι x y) * (L.ι z y)⁻¹ = L.ι x z := - begin transitivity; apply Id.map; apply inv; apply L.trans end + begin transitivity; apply ap; apply inv; apply L.trans end hott def propι : Π g x, prop (Σ y, L.ι x y = g) := λ g x, contrImplProp (L.full g x) @@ -95,13 +96,13 @@ namespace GroundZero.Algebra hott def zero {x y : M} (p : L.ι x y = G.e) : x = y := let q := L.propι (L.ι x y) x ⟨y, Id.refl⟩ ⟨x, L.neut x ⬝ Id.inv p⟩; - Id.map Sigma.fst (Id.inv q) + ap Sigma.fst (Id.inv q) hott def injιᵣ {x y z : M} : L.ι z x = L.ι z y → x = y := begin intro p; apply L.zero; transitivity; symmetry; apply L.trans x z y; - transitivity; apply Id.map; exact Id.inv p; + transitivity; apply ap; exact Id.inv p; transitivity; apply L.trans; apply neut end @@ -137,8 +138,8 @@ namespace GroundZero.Algebra { apply (K.fixι g₂ x.2).2 } }; { intro ⟨(p₁, p₂), v⟩; fapply Sigma.prod; { fapply Product.prod; - apply Id.map Sigma.fst ((L.full g₁ x.1).2 ⟨p₁, Id.map Prod.fst v⟩); - apply Id.map Sigma.fst ((K.full g₂ x.2).2 ⟨p₂, Id.map Prod.snd v⟩) }; + apply ap Sigma.fst ((L.full g₁ x.1).2 ⟨p₁, ap Prod.fst v⟩); + apply ap Sigma.fst ((K.full g₂ x.2).2 ⟨p₂, ap Prod.snd v⟩) }; { apply Structures.prodHset; apply G.hset; apply H.hset } } } end @@ -162,19 +163,19 @@ namespace GroundZero.Algebra (p : L.ι a₁ b₁ ∈ φ.set) (q : L.ι a₂ b₂ ∈ φ.set) : G.φ (L.ι a₁ a₂)⁻¹ (L.ι b₁ b₂) ∈ φ.set := begin apply transport (· ∈ φ.set); symmetry; - transitivity; apply Id.map (G.φ _); + transitivity; apply ap (G.φ _); symmetry; apply G.oneMul; transitivity; - apply Id.map; apply Id.map (G.φ · (L.ι b₁ b₂)); + apply ap; apply ap (G.φ · (L.ι b₁ b₂)); symmetry; apply G.mulLeftInv (L.ι a₂ b₁); - transitivity; apply Id.map; apply G.mulAssoc; + transitivity; apply ap; apply G.mulAssoc; symmetry; apply G.mulAssoc; apply φ.1.mul; { apply transport (· ∈ φ.set); apply invExplode; apply φ.1.inv; - apply transport (· ∈ φ.set); symmetry; apply Id.map (G.φ · (L.ι a₁ a₂)); - transitivity; symmetry; apply L.trans a₂ a₁; apply Id.map (G.φ · (L.ι a₁ b₁)); + apply transport (· ∈ φ.set); symmetry; apply ap (G.φ · (L.ι a₁ a₂)); + transitivity; symmetry; apply L.trans a₂ a₁; apply ap (G.φ · (L.ι a₁ b₁)); symmetry; apply inv; apply isNormalSubgroup.conj φ.2; exact p }; { apply φ.2; apply transport (· ∈ φ.set); symmetry; - apply Id.map (G.φ · (L.ι a₂ b₁)); transitivity; symmetry; apply L.trans b₁ a₂; - apply Id.map (G.φ · (L.ι a₂ b₂)); symmetry; apply inv; + apply ap (G.φ · (L.ι a₂ b₁)); transitivity; symmetry; apply L.trans b₁ a₂; + apply ap (G.φ · (L.ι a₂ b₂)); symmetry; apply inv; apply isNormalSubgroup.conj φ.2; exact q } end @@ -204,7 +205,7 @@ namespace GroundZero.Algebra begin apply Prod.mk <;> existsi L.τ i⁻¹ <;> { intro x; transitivity; apply τ.comp; - transitivity; apply Id.map (L.τ · x); + transitivity; apply ap (L.τ · x); first | apply G.mulLeftInv | apply Group.mulRightInv; apply τ.id } end @@ -213,7 +214,7 @@ namespace GroundZero.Algebra begin apply @injιᵣ M G L _ _ a; apply τ.lawful end hott def τ.inj {g h : G.carrier} (x : M) (p : L.τ g x = L.τ h x) : g = h := - Id.inv (τ.lawful L g x) ⬝ (Id.map (L.ι x) p) ⬝ (τ.lawful L h x) + Id.inv (τ.lawful L g x) ⬝ ap (L.ι x) p ⬝ τ.lawful L h x hott def τ.act : Gᵒᵖ ⮎ M := ⟨L.τ, (τ.id L, τ.comp L)⟩ @@ -255,7 +256,7 @@ namespace GroundZero.Algebra transitivity; apply τ.lawful; symmetry; transitivity; apply H; transitivity; symmetry; apply inv; - apply Id.map; apply τ.lawful + apply ap; apply τ.lawful end hott def reversing.acommᵣ {f : M → M} {i : G.carrier} @@ -271,7 +272,7 @@ namespace GroundZero.Algebra intros i; apply τ.inj L m; transitivity; { symmetry; apply τ.comp }; transitivity; apply reversing.acommᵣ; apply H; - transitivity; apply τ.comp; apply Id.map (L.τ · m); + transitivity; apply τ.comp; apply ap (L.τ · m); apply G.mulLeftInv end @@ -290,28 +291,28 @@ namespace GroundZero.Algebra L.ι a (L.τ i b) = G.φ (L.ι a b) i := begin transitivity; { symmetry; apply L.trans _ b _ }; - apply Id.map; apply τ.lawful + apply ap; apply τ.lawful end hott def π.conjugate {i : G.carrier} (a b : M) : L.ι a (L.π i⁻¹ a (L.τ i b)) = Group.conjugate (L.ι a b) i := begin transitivity; { apply π.lawful }; - transitivity; { apply Id.map (G.φ i⁻¹); apply τ.mulRight }; + transitivity; { apply ap (G.φ i⁻¹); apply τ.mulRight }; symmetry; apply G.mulAssoc end hott def π.preserving {i : G.carrier} (x : M) : preserving L L (L.π i x) := begin intros a b; transitivity; { symmetry; apply L.trans _ x }; - transitivity; apply Id.map; apply π.lawful; - transitivity; apply Id.map (G.φ · _); + transitivity; apply ap; apply π.lawful; + transitivity; apply ap (G.φ · _); transitivity; symmetry; apply inv; - transitivity; { apply Id.map; apply π.lawful }; + transitivity; { apply ap; apply π.lawful }; apply invExplode; transitivity; apply G.mulAssoc; - transitivity; apply Id.map; + transitivity; apply ap; transitivity; symmetry; apply G.mulAssoc; - transitivity; apply Id.map (G.φ · _); + transitivity; apply ap (G.φ · _); apply G.mulLeftInv; apply G.oneMul; apply invTrans end @@ -331,7 +332,7 @@ namespace GroundZero.Algebra transitivity; apply π.lawful; symmetry; transitivity; symmetry; apply L.trans _ (f m) _; - apply Id.map; apply H + apply ap; apply H end hott def τ.abelianImplPreserving (ρ : G.isCommutative) : @@ -339,15 +340,15 @@ namespace GroundZero.Algebra begin intros i a b; transitivity; symmetry; apply L.trans _ a; - transitivity; apply Id.map (G.φ · _); + transitivity; apply ap (G.φ · _); transitivity; symmetry; apply inv; - apply Id.map; apply τ.lawful; - transitivity; apply Id.map (G.φ i⁻¹); + apply ap; apply τ.lawful; + transitivity; apply ap (G.φ i⁻¹); transitivity; symmetry; apply L.trans _ b; transitivity; apply ρ; - apply Id.map (G.φ · _); apply τ.lawful; + apply ap (G.φ · _); apply τ.lawful; transitivity; symmetry; apply G.mulAssoc; - transitivity; apply Id.map (G.φ · _); + transitivity; apply ap (G.φ · _); apply G.mulLeftInv; apply G.oneMul end @@ -363,7 +364,7 @@ namespace GroundZero.Algebra begin intro n; apply @injιᵣ M G L _ _ m; transitivity; apply π.lawful; - transitivity; apply Id.map (G.φ i); apply π.lawful; + transitivity; apply ap (G.φ i); apply π.lawful; symmetry; transitivity; apply π.lawful; apply G.mulAssoc end @@ -377,7 +378,7 @@ namespace GroundZero.Algebra begin apply Prod.mk <;> existsi L.π i⁻¹ m <;> { intro x; transitivity; apply π.comp; - transitivity; apply Id.map (L.π · m x); + transitivity; apply ap (L.π · m x); first | apply G.mulLeftInv | apply Group.mulRightInv; apply π.id } end @@ -396,19 +397,19 @@ namespace GroundZero.Algebra hott def ρ.ι (u v a b : M) : L.ι a (L.ρ u v b) = L.ι a v * L.ι b u := begin transitivity; symmetry; apply L.trans _ v _; - apply Id.map; apply ρ.lawful + apply ap; apply ρ.lawful end hott def ρ.inv (u v : M) : ρ L u v ∘ ρ L v u ~ id := begin intro m; apply @injιᵣ M G L _ _ m; transitivity; apply ρ.ι; - transitivity; apply Id.map (G.φ (L.ι m v)); + transitivity; apply ap (G.φ (L.ι m v)); transitivity; symmetry; apply gis.inv; - transitivity; apply Id.map; apply ρ.ι; + transitivity; apply ap; apply ρ.ι; apply Group.invExplode; transitivity; symmetry; apply G.mulAssoc; - transitivity; apply Id.map (G.φ · _); + transitivity; apply ap (G.φ · _); apply Group.mulRightInv; transitivity; apply G.oneMul; transitivity; apply gis.inv; apply neut₂ @@ -458,7 +459,7 @@ namespace GroundZero.Algebra λ ⟨φ, H⟩, ⟨λ a b, (H a b).1.1, begin intros x y z; apply (regular.elim φ H).2 x; transitivity; symmetry; apply φ.2.2; - transitivity; apply Id.map; apply (H x y).1.2; + transitivity; apply ap; apply (H x y).1.2; transitivity; apply (H y z).1.2; symmetry; apply (H x z).1.2 end, begin @@ -466,7 +467,7 @@ namespace GroundZero.Algebra { existsi φ.1 g x; apply (regular.elim φ H).2 x; apply (H _ _).1.2 }; { intro ⟨y, p⟩; fapply Sigma.prod; - { transitivity; apply Id.map (φ.1 · x); + { transitivity; apply ap (φ.1 · x); exact Id.inv p; apply (H x y).1.2 }; { apply G.hset } } end⟩ @@ -510,7 +511,7 @@ namespace GroundZero.Algebra Π a b, L.ι a (f b) = L.ι a (f a) * (L.ι a b)⁻¹ := begin intros a b; transitivity; symmetry; apply L.trans a (f a); - apply Id.map (G.φ (L.ι a (f a))); transitivity; + apply ap (G.φ (L.ι a (f a))); transitivity; apply H; symmetry; apply inv end @@ -519,7 +520,7 @@ namespace GroundZero.Algebra begin intro n; apply @injιᵣ M G L _ _ n; transitivity; apply ρ.ι; - transitivity; apply Id.map (G.φ · _); + transitivity; apply ap (G.φ · _); apply reversing.ι L f H; symmetry; apply Group.cancelLeft end @@ -540,8 +541,7 @@ namespace GroundZero.Algebra def L.length {A : Type u} : L A → ℕ := Sigma.fst def L.nth {A : Type u} (xs : L A) : Finite xs.length → A := xs.snd - hott def L.all {A : Type u} (π : A → propset) - (xs : L A) : propset := + hott def L.all {A : Type u} (π : A → Prop) (xs : L A) : Prop := ⟨Π n, (π (xs.nth n)).fst, begin apply piProp; intro; apply (π _).2 end⟩ -- Set of (12 × n) ordered notes, where n ∈ ℕ @@ -562,10 +562,10 @@ namespace GroundZero.Algebra -- Set of tone rows def R := Orbits (tr φ) - def M.dodecaphonic (xs : M A) (r : P A) : propset := + def M.dodecaphonic (xs : M A) (r : P A) : Prop := xs.all (λ x, ⟨x ∈ orbit (tr φ) r, Ens.prop x _⟩) - noncomputable hott def R.dodecaphonic (xs : M A) (r : R φ) : propset := + noncomputable hott def R.dodecaphonic (xs : M A) (r : R φ) : Prop := begin fapply HITs.Quotient.rec _ _ _ r; { exact M.dodecaphonic φ xs }; @@ -581,4 +581,4 @@ namespace GroundZero.Algebra end end Dodecaphony -end GroundZero.Algebra \ No newline at end of file +end GroundZero.Algebra diff --git a/GroundZero/Cubical/Path.lean b/GroundZero/Cubical/Path.lean index f201e23..65799bb 100644 --- a/GroundZero/Cubical/Path.lean +++ b/GroundZero/Cubical/Path.lean @@ -1,6 +1,8 @@ import GroundZero.HITs.Interval + open GroundZero.HITs.Interval (i₀ i₁ seg) open GroundZero.Types GroundZero.HITs +open GroundZero.Types.Id (ap) open GroundZero.Proto (idfun) /- @@ -28,7 +30,7 @@ hott def elim {A : Type u} {a b : A} (p : Path A a b) : I → A := @Path.casesOn A (λ _ _ _, I → A) a b p (@idfun (I → A)) hott def encode {A : Type u} {a b : A} (p : Path A a b) : a = b := -@Path.casesOn A (λ a b _, a = b) a b p (Id.map · seg) +@Path.casesOn A (λ a b _, a = b) a b p (ap · seg) noncomputable hott def encodeDecode {A : Type u} {a b : A} (p : a = b) : encode (decode p) = p := by apply Interval.recβrule @@ -49,7 +51,7 @@ Interval.ind x (Equiv.subst Interval.seg x) Id.refl i hott def coe.back (B : I → Type u) (i : I) (x : B i₁) : B i := Interval.ind (Equiv.subst Interval.seg⁻¹ x) x (begin apply Id.trans; symmetry; apply Equiv.substComp; - transitivity; apply Id.map (Equiv.subst · x); + transitivity; apply ap (Equiv.subst · x); apply Id.invComp; reflexivity end) i @@ -160,11 +162,12 @@ def eta {A : Type u} (a : A) : singl a := ⟨a, refl a⟩ @[hottAxiom] def meet {A : Type u} {a b : A} (p : Path A a b) : LineP (λ i, Path A a (p @ i)) := -Interval.hrec _ (refl a) p (begin +begin + fapply Interval.hrec; exact refl a; exact p; induction p using Path.casesOn; apply HEq.map lam; apply Theorems.funext; - intro; apply Id.map; apply Interval.contrLeft -end) + intro; apply Id.ap; apply Interval.contrLeft +end /- This doesn’t pass typechecking. @@ -190,4 +193,4 @@ Path (σ 1) (Equiv.subst Interval.seg a) b hott def PathP.lam (σ : I → Type u) (f : Π i, σ i) : PathP σ (f 0) (f 1) := Path.lam (Interval.rec _ _ (Equiv.apd f Interval.seg)) -end GroundZero.Cubical \ No newline at end of file +end GroundZero.Cubical diff --git a/GroundZero/Exercises/Chap1.lean b/GroundZero/Exercises/Chap1.lean index 0741340..d81f2c4 100644 --- a/GroundZero/Exercises/Chap1.lean +++ b/GroundZero/Exercises/Chap1.lean @@ -3,6 +3,7 @@ import GroundZero.Theorems.Nat import GroundZero.Types.Sigma open GroundZero GroundZero.Types +open GroundZero.Types.Id (ap) open GroundZero.Types.Equiv open GroundZero.Proto @@ -66,7 +67,7 @@ hott def grec {C : Type u} (c₀ : C) (cₛ : ℕ → C → C) : ℕ → ℕ × hott def grec.stable {C : Type u} (c₀ : C) (cₛ : ℕ → C → C) : Π n, (grec c₀ cₛ n).1 = n | Nat.zero => idp 0 -| Nat.succ n => Id.map Nat.succ (stable c₀ cₛ n) +| Nat.succ n => ap Nat.succ (stable c₀ cₛ n) section variable {C : Type u} (c₀ : C) (cₛ : ℕ → C → C) @@ -77,7 +78,7 @@ section by reflexivity hott def Nat.iterB₂ (n : ℕ) : Nat.rec' c₀ cₛ (n + 1) = cₛ n (Nat.rec' c₀ cₛ n) := - Id.map (λ m, cₛ m (Nat.rec' c₀ cₛ n)) (grec.stable c₀ cₛ n) + ap (λ m, cₛ m (Nat.rec' c₀ cₛ n)) (grec.stable c₀ cₛ n) end -- exercise 1.5 @@ -127,8 +128,8 @@ namespace Product' hott def indB (a : A) (b : B) : ind π φ (mk a b) = φ a b := begin - transitivity; apply Id.map (transport π · (φ a b)); - transitivity; apply Id.map Theorems.funext; change _ = (λ x, idp (mk a b x)); + transitivity; apply ap (transport π · (φ a b)); + transitivity; apply ap Theorems.funext; change _ = (λ x, idp (mk a b x)); apply Theorems.funext; intro b; induction b using Bool.casesOn <;> reflexivity; apply Theorems.funextId; reflexivity end @@ -189,33 +190,33 @@ namespace Nat' hott def addZero : Π n, add n 0 = n := idp hott def zeroAdd : Π n, add 0 n = n := - ind (λ n, add 0 n = n) (idp 0) (λ n p, Id.map Nat.succ p) + ind (λ n, add 0 n = n) (idp 0) (λ n p, ap Nat.succ p) hott def succAdd : Π n m, add (n + 1) m = add n m + 1 := - λ n, ind (λ m, add (n + 1) m = add n m + 1) (idp (n + 1)) (λ m p, Id.map Nat.succ p) + λ n, ind (λ m, add (n + 1) m = add n m + 1) (idp (n + 1)) (λ m p, ap Nat.succ p) hott def addComm : Π n m, add n m = add m n := λ n, ind (λ m, add n m = add m n) (zeroAdd n)⁻¹ - (λ m p, (Id.map Nat.succ p) ⬝ (succAdd m n)⁻¹) + (λ m p, (ap Nat.succ p) ⬝ (succAdd m n)⁻¹) hott def addAssoc : Π n m k, add n (add m k) = add (add n m) k := - λ n m, ind (λ k, add n (add m k) = add (add n m) k) (idp (add n m)) (λ k p, Id.map Nat.succ p) + λ n m, ind (λ k, add n (add m k) = add (add n m) k) (idp (add n m)) (λ k p, ap Nat.succ p) hott def oneMul : Π n, mult 1 n = n := - ind (λ n, mult 1 n = n) (idp 0) (λ n p, (addComm 1 (mult 1 n)) ⬝ Id.map Nat.succ p) + ind (λ n, mult 1 n = n) (idp 0) (λ n p, (addComm 1 (mult 1 n)) ⬝ ap Nat.succ p) hott def succMul : Π n m, mult (n + 1) m = add m (mult n m) := λ n, ind (λ m, mult (n + 1) m = add m (mult n m)) (idp 0) (λ m p, calc mult (n + 1) (m + 1) = add n (mult (n + 1) m) + 1 : succAdd n (mult (n + 1) m) - ... = add n (add m (mult n m)) + 1 : Id.map (λ k, add n k + 1) p - ... = add (add n m) (mult n m) + 1 : Id.map Nat.succ (addAssoc n m (mult n m)) - ... = add (add m n) (mult n m) + 1 : Id.map (λ k, add k (mult n m) + 1) (addComm n m) - ... = add m (add n (mult n m)) + 1 : Id.map Nat.succ (addAssoc m n (mult n m))⁻¹ + ... = add n (add m (mult n m)) + 1 : ap (λ k, add n k + 1) p + ... = add (add n m) (mult n m) + 1 : ap Nat.succ (addAssoc n m (mult n m)) + ... = add (add m n) (mult n m) + 1 : ap (λ k, add k (mult n m) + 1) (addComm n m) + ... = add m (add n (mult n m)) + 1 : ap Nat.succ (addAssoc m n (mult n m))⁻¹ ... = add (m + 1) (mult n (m + 1)) : (succAdd m (mult n (m + 1)))⁻¹) hott def mulOne : Π n, mult n 1 = n := ind (λ n, mult n 1 = n) (idp 0) (λ n p, - (succMul n 1) ⬝ (addComm 1 (mult n 1)) ⬝ Id.map Nat.succ p) + (succMul n 1) ⬝ (addComm 1 (mult n 1)) ⬝ ap Nat.succ p) hott def mulZero : Π n, mult n 0 = 0 := λ _, idp 0 @@ -224,14 +225,14 @@ namespace Nat' hott def mulComm : Π n m, mult n m = mult m n := λ n, ind (λ m, mult n m = mult m n) (zeroMul n)⁻¹ - (λ m p, Id.map (add n) p ⬝ (succMul m n)⁻¹) + (λ m p, ap (add n) p ⬝ (succMul m n)⁻¹) hott def mulDistrLeft : Π n m k, mult n (add m k) = add (mult n m) (mult n k) := λ n m, ind (λ k, mult n (add m k) = add (mult n m) (mult n k)) (idp (mult n m)) (λ k p, calc - mult n (add m (k + 1)) = add n (add (mult n m) (mult n k)) : Id.map (add n) p + mult n (add m (k + 1)) = add n (add (mult n m) (mult n k)) : ap (add n) p ... = add (add (mult n m) (mult n k)) n : addComm _ _ ... = add (mult n m) (add (mult n k) n) : (addAssoc _ _ _)⁻¹ - ... = add (mult n m) (mult n (k + 1)) : Id.map (add (mult n m)) (addComm _ _)) + ... = add (mult n m) (mult n (k + 1)) : ap (add (mult n m)) (addComm _ _)) hott def mulDistrRight : Π n m k, mult (add n m) k = add (mult n k) (mult m k) := λ n m k, calc mult (add n m) k = mult k (add n m) : mulComm _ _ @@ -241,7 +242,7 @@ namespace Nat' hott def mulAssoc : Π n m k, mult n (mult m k) = mult (mult n m) k := λ n m, ind (λ k, mult n (mult m k) = mult (mult n m) k) (idp 0) (λ k p, calc mult n (mult m (k + 1)) = add (mult n m) (mult n (mult m k)) : mulDistrLeft _ _ _ - ... = add (mult n m) (mult (mult n m) k) : Id.map (add (mult n m)) p + ... = add (mult n m) (mult (mult n m) k) : ap (add (mult n m)) p ... = mult (mult n m) (k + 1) : idp _) end Nat' diff --git a/GroundZero/Exercises/Chap2.lean b/GroundZero/Exercises/Chap2.lean index ef59e98..3056641 100644 --- a/GroundZero/Exercises/Chap2.lean +++ b/GroundZero/Exercises/Chap2.lean @@ -1,6 +1,7 @@ import GroundZero.Theorems.Pullback open GroundZero GroundZero.Types +open GroundZero.Types.Id (ap) open GroundZero.Types.Equiv open GroundZero.Proto @@ -112,9 +113,9 @@ namespace «2.7» def φ (x : Σ a, B a) : Σ a', B' a' := ⟨g x.1, h x.1 x.2⟩ hott def prodMap : Π (x y : Σ a, B a) (p : x.1 = y.1) (q : x.2 =[p] y.2), - Id.map (φ g h) (Sigma.prod p q) + ap (φ g h) (Sigma.prod p q) = @Sigma.prod A' B' (φ g h x) (φ g h y) - (@Id.map A A' x.1 y.1 g p) (depPathMap' g h q) := + (@ap A A' x.1 y.1 g p) (depPathMap' g h q) := begin intro ⟨x, H⟩ ⟨y, G⟩ (p : x = y); induction p; intro (q : H = G); induction q; reflexivity @@ -130,13 +131,13 @@ namespace «2.8» Coproduct.elim (Coproduct.inl ∘ g) (Coproduct.inr ∘ h) hott def ρ : Π {x y : A + B}, Coproduct.code x y → Coproduct.code (φ g h x) (φ g h y) - | Sum.inl _, Sum.inl _, p => Id.map _ p + | 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.inr _, p => Id.map _ p + | Sum.inr _, Sum.inr _, p => ap _ p hott def mapPathSum (x y : A + B) : Π p, - Id.map (φ g h) (Coproduct.pathSum x y p) + ap (φ g h) (Coproduct.pathSum x y p) = Coproduct.pathSum (φ g h x) (φ g h y) (ρ g h p) := begin match x, y with @@ -203,8 +204,8 @@ namespace «2.12» def right : hcommSquare C E D F := ⟨k, s, g, j, β⟩ def outer : hcommSquare A E B F := - ⟨k, s ∘ h, g ∘ f, i, @Id.map (C → F) (A → F) _ _ (· ∘ f) β - ⬝ @Id.map _ (A → F) _ _ (s ∘ ·) α⟩ + ⟨k, s ∘ h, g ∘ f, i, @ap (C → F) (A → F) _ _ (· ∘ f) β + ⬝ @ap _ (A → F) _ _ (s ∘ ·) α⟩ hott def pullbackLemma (H : (right β).isPullback) : (left α).isPullback ↔ (outer α β).isPullback := @@ -225,11 +226,11 @@ example : (𝟐 ≃ 𝟐) ≃ 𝟐 := Theorems.Equiv.boolEquivEqvBool -- exercise 2.15 hott def transportMap {A : Type u} {B : A → Type v} {x y : A} (p : x = y) : - transport B p = idtoeqv (Id.map B p) := + transport B p = idtoeqv (ap B p) := begin induction p; reflexivity end -- exercise 2.18 hott def transportSquare {A : Type u} {B : A → Type v} {f g : Π x, B x} (H : f ~ g) {x y : A} (p : x = y) : - Id.map (transport B p) (H x) ⬝ apd g p = apd f p ⬝ H y := + ap (transport B p) (H x) ⬝ apd g p = apd f p ⬝ H y := begin induction p; transitivity; apply Id.reflRight; apply Equiv.idmap end diff --git a/GroundZero/Exercises/Chap3.lean b/GroundZero/Exercises/Chap3.lean index bfd7c0b..68d9633 100644 --- a/GroundZero/Exercises/Chap3.lean +++ b/GroundZero/Exercises/Chap3.lean @@ -116,19 +116,19 @@ namespace «3.9» | false => ap (Coproduct.elim _ _) (lemFalse Empty.elim) | true => ap (Coproduct.elim _ _) (lemTrue ★) - hott lemma Ωrinv (lem : LEM₋₁) : Ωintro ∘ Ωelim lem ~ idfun := + noncomputable hott lemma Ωrinv (lem : LEM₋₁) : Ωintro ∘ Ωelim lem ~ idfun := begin intro w; apply Equiv.propset.Id; match lem w.1 w.2 with | Sum.inl x => _ | Sum.inr φ => _; - transitivity; apply Id.map; apply Id.map (Bool.elim _ _); apply Id.map (Coproduct.elim _ _); + transitivity; apply ap; apply ap (Bool.elim _ _); apply ap (Coproduct.elim _ _); apply lemTrue x; symmetry; apply ua; apply Structures.contrEquivUnit; fapply Sigma.mk; exact x; intro y; apply w.2; - transitivity; apply Id.map; apply Id.map (Bool.elim _ _); apply Id.map (Coproduct.elim _ _); + transitivity; apply ap; apply ap (Bool.elim _ _); apply ap (Coproduct.elim _ _); apply lemFalse φ; symmetry; apply ua; apply uninhabitedType; exact Empty.elim ∘ φ end - hott theorem lemImplPropEqvBool (lem : LEM₋₁) : Prop u ≃ 𝟐 := + noncomputable hott theorem lemImplPropEqvBool (lem : LEM₋₁) : Prop u ≃ 𝟐 := ⟨Ωelim lem, Qinv.toBiinv _ ⟨Ωintro, (Ωlinv lem, Ωrinv lem)⟩⟩ end «3.9» @@ -160,11 +160,11 @@ namespace «3.10» hott corollary lemSucCumulativity : LEM₋₁ (u + 1) → LEM₋₁ u := lemCumulativity.{u, u + 1} - hott lemma lemImplPropUniverseEqv (lem : LEM₋₁ (max u v)) : Prop u ≃ Prop (max u v) := + noncomputable hott lemma lemImplPropUniverseEqv (lem : LEM₋₁ (max u v)) : Prop u ≃ Prop (max u v) := Equiv.trans (lemImplPropEqvBool (lemCumulativity.{u, v} lem)) (Equiv.symm (lemImplPropEqvBool lem)) - hott lemma resizeUniqLem1 (lem : LEM₋₁ (max u v)) : (lemImplPropUniverseEqv.{u, v} lem).1 ∘ Ωintro ~ ResizeΩ.{u, v} ∘ Ωintro := + noncomputable hott lemma resizeUniqLem1 (lem : LEM₋₁ (max u v)) : (lemImplPropUniverseEqv.{u, v} lem).1 ∘ Ωintro ~ ResizeΩ.{u, v} ∘ Ωintro := begin intro b; transitivity; apply ap Ωintro; apply Ωlinv; apply Equiv.propset.Id; symmetry; apply ua; induction b using Bool.casesOn; @@ -173,16 +173,16 @@ namespace «3.10» intro (Resize.intro b); apply ap; apply Structures.unitIsProp } end - hott lemma resizeUniqLem2 (lem : LEM₋₁ (max u v)) : (lemImplPropUniverseEqv.{u, v} lem).1 ~ ResizeΩ.{u, v} := + noncomputable hott lemma resizeUniqLem2 (lem : LEM₋₁ (max u v)) : (lemImplPropUniverseEqv.{u, v} lem).1 ~ ResizeΩ.{u, v} := begin intro w; transitivity; apply ap; symmetry; apply Ωrinv (lemCumulativity.{u, v} lem); transitivity; apply resizeUniqLem1; apply ap ResizeΩ; apply Ωrinv end - hott theorem lemImplResizing (lem : LEM₋₁ (max u v)) : biinv ResizeΩ := + noncomputable hott theorem lemImplResizing (lem : LEM₋₁ (max u v)) : biinv ResizeΩ := transport biinv (Theorems.funext (resizeUniqLem2.{u, v} lem)) (lemImplPropUniverseEqv lem).2 - hott corollary lemImplResizingSuc : LEM₋₁ (u + 1) → biinv ResizeΩ.{u, u + 1} := + noncomputable hott corollary lemImplResizingSuc : LEM₋₁ (u + 1) → biinv ResizeΩ.{u, u + 1} := lemImplResizing.{u, u + 1} end «3.10» diff --git a/GroundZero/HITs/Circle.lean b/GroundZero/HITs/Circle.lean index 09fddbf..c3e44da 100644 --- a/GroundZero/HITs/Circle.lean +++ b/GroundZero/HITs/Circle.lean @@ -51,17 +51,17 @@ namespace Loop hott def powerComp (p : a = a) : Π z, power p z ⬝ p = power p (Integer.succ z) | Integer.neg Nat.zero => Id.invComp _ - | Integer.neg (Nat.succ n) => (Id.assoc _ _ _)⁻¹ ⬝ Id.map (neg p n ⬝ ·) (Id.invComp _) ⬝ Id.reflRight _ + | Integer.neg (Nat.succ n) => (Id.assoc _ _ _)⁻¹ ⬝ ap (neg p n ⬝ ·) (Id.invComp _) ⬝ Id.reflRight _ | Integer.pos _ => idp _ hott def powerCompPred (p : a = a) : Π z, power p z ⬝ p⁻¹ = power p (Integer.pred z) | Integer.neg _ => idp _ | Integer.pos Nat.zero => idp _ - | Integer.pos (Nat.succ n) => (Id.assoc _ _ _)⁻¹ ⬝ Id.map (pos p n ⬝ ·) (Id.compInv _) ⬝ Id.reflRight _ + | Integer.pos (Nat.succ n) => (Id.assoc _ _ _)⁻¹ ⬝ ap (pos p n ⬝ ·) (Id.compInv _) ⬝ Id.reflRight _ hott def compPowerPos (p : a = a) : Π n, p ⬝ power p (Integer.pos n) = power p (Integer.succ (Integer.pos n)) | Nat.zero => Id.reflRight _ - | Nat.succ n => Id.assoc _ _ _ ⬝ Id.map (· ⬝ p) (compPowerPos p n) + | Nat.succ n => Id.assoc _ _ _ ⬝ ap (· ⬝ p) (compPowerPos p n) hott def compPowerNeg (p : a = a) : Π n, p ⬝ power p (Integer.neg n) = power p (Integer.succ (Integer.neg n)) | Nat.zero => Id.compInv _ @@ -94,23 +94,23 @@ namespace Loop begin fapply @Integer.indsp (λ x, Π y, power p x ⬝ power p y = power p y ⬝ power p x) _ _ _ x <;> clear x; { intro y; symmetry; apply Id.reflRight }; - { intros x ih y; transitivity; apply Id.map (· ⬝ power p y); + { intros x ih y; transitivity; apply ap (· ⬝ power p y); symmetry; apply compPower; transitivity; symmetry; apply Id.assoc; - transitivity; apply Id.map; apply ih; + transitivity; apply ap; apply ih; transitivity; apply Id.assoc; - transitivity; apply Id.map (· ⬝ power p x); apply compPowerComm; + transitivity; apply ap (· ⬝ power p x); apply compPowerComm; transitivity; symmetry; apply Id.assoc; - apply Id.map; apply compPower }; - { intros x ih y; transitivity; apply Id.map (· ⬝ power p y); + apply ap; apply compPower }; + { intros x ih y; transitivity; apply ap (· ⬝ power p y); symmetry; apply compPowerPred; transitivity; symmetry; apply Id.assoc; - transitivity; apply Id.map; apply ih; + transitivity; apply ap; apply ih; transitivity; apply Id.assoc; - transitivity; apply Id.map (· ⬝ power p x); + transitivity; apply ap (· ⬝ power p x); apply invCompPowerComm; transitivity; symmetry; apply Id.assoc; - apply Id.map; apply compPowerPred } + apply ap; apply compPowerPred } end end Loop @@ -158,19 +158,19 @@ namespace Circle -- why this doesn’t require “noncomputable” attribute as it was in Lean 3? -- looks pretty strange hott def recβrule₂ {B : Type u} (b : B) (ℓ : b = b) := calc - Id.map (rec b ℓ) loop - = Id.map (rec b ℓ) seg₂ ⬝ Id.map (rec b ℓ) seg₁⁻¹ : Equiv.mapFunctoriality _ - ... = Id.map (rec b ℓ) seg₂ ⬝ (Id.map (rec b ℓ) seg₁)⁻¹ : Id.map (_ ⬝ ·) (Id.mapInv _ _) - ... = ℓ ⬝ Id.refl⁻¹ : bimap (· ⬝ ·⁻¹) (Suspension.recβrule _ _ _ _) (Suspension.recβrule _ _ _ _) - ... = ℓ : Id.reflRight _ + ap (rec b ℓ) loop + = ap (rec b ℓ) seg₂ ⬝ ap (rec b ℓ) seg₁⁻¹ : Equiv.mapFunctoriality _ + ... = ap (rec b ℓ) seg₂ ⬝ (ap (rec b ℓ) seg₁)⁻¹ : ap (_ ⬝ ·) (Id.mapInv _ _) + ... = ℓ ⬝ (idp b)⁻¹ : bimap (· ⬝ ·⁻¹) (Suspension.recβrule _ _ _ _) (Suspension.recβrule _ _ _ _) + ... = ℓ : Id.reflRight _ hott def recβrule₃ {B : Type u} (b : B) (ℓ : b = b) := calc - Id.map (rec b ℓ) loop⁻¹ - = (Id.map (rec b ℓ) loop)⁻¹ : Id.mapInv _ _ - ... = ℓ⁻¹ : Id.map Id.inv (recβrule₂ _ _) + ap (rec b ℓ) loop⁻¹ + = (ap (rec b ℓ) loop)⁻¹ : Id.mapInv _ _ + ... = ℓ⁻¹ : ap Id.inv (recβrule₂ _ _) hott def ind {B : S¹ → Type u} (b : B base) (ℓ : b =[loop] b) : Π (x : S¹), B x := - ind₂ b (Equiv.subst seg₁ b) Id.refl (depPathTransSymm ℓ) + ind₂ b (transport B seg₁ b) (idp _) (depPathTransSymm ℓ) attribute [eliminator] ind @@ -182,7 +182,7 @@ namespace Circle dsimp [ind, ind₂]; transitivity; apply apdFunctoriality; transitivity; apply bimap depTrans; apply Suspension.indβrule; - transitivity; apply apdInv; apply Id.map; + transitivity; apply apdInv; apply ap; apply Suspension.indβrule; apply depPathTransSymmCoh end @@ -199,8 +199,8 @@ namespace Circle begin intros a p; transitivity; symmetry; apply Circle.recβrule₂ a p; - change _ = Id.map (rec a p) (idp _); - apply Id.map; apply H + change _ = ap (rec a p) (idp _); + apply ap; apply H end noncomputable hott def loopNeqRefl : ¬(loop = idp base) := @@ -217,22 +217,22 @@ namespace Circle noncomputable hott def trivialNotHmtpy : ¬(trivial = id) := begin intro p; apply loopNeqRefl; transitivity; symmetry; apply idmap; - apply transport (λ f, Id.map f loop = idp (f base)) p; apply Circle.recβrule₂ + apply transport (λ f, ap f loop = idp (f base)) p; apply Circle.recβrule₂ end noncomputable hott def trivialHmtpy : trivial ~ (λ _, base) := begin intro x; induction x; reflexivity; apply Id.trans; apply transportOverContrMap; - transitivity; apply Id.map (· ⬝ idp base); transitivity; apply Id.mapInv; - apply Id.map; apply recβrule₂; reflexivity + transitivity; apply ap (· ⬝ idp base); transitivity; apply Id.mapInv; + apply ap; apply recβrule₂; reflexivity end noncomputable hott def nontrivialHmtpy : nontrivial ~ id := begin intro x; induction x; reflexivity; apply Id.trans; apply transportOverInvolution; - transitivity; apply Id.map (· ⬝ idp base ⬝ loop); - transitivity; apply Id.mapInv; apply Id.map; apply recβrule₂; + transitivity; apply ap (· ⬝ idp base ⬝ loop); + transitivity; apply Id.mapInv; apply ap; apply recβrule₂; transitivity; symmetry; apply Id.assoc; apply Id.invComp end @@ -265,15 +265,15 @@ namespace Circle noncomputable hott def transportThere (x : ℤ) := calc transport helix loop x - = transportconst (Id.map helix loop) x : Equiv.transportComp id helix loop x - ... = transportconst (ua Integer.succEquiv) x : Id.map (transportconst · x) (recβrule₂ _ _) + = transportconst (ap helix loop) x : Equiv.transportComp id helix loop x + ... = transportconst (ua Integer.succEquiv) x : ap (transportconst · x) (recβrule₂ _ _) ... = Integer.succ x : ua.transportRule _ _ noncomputable hott def transportBack (x : ℤ) := calc transport helix loop⁻¹ x - = transportconst (Id.map helix loop⁻¹) x : Equiv.transportComp id helix loop⁻¹ x - ... = transportconst (Id.map helix loop)⁻¹ x : Id.map (transportconst · x) (Id.mapInv _ _) - ... = transportconst (ua Integer.succEquiv)⁻¹ x : Id.map (transportconst ·⁻¹ x) (recβrule₂ _ _) + = transportconst (ap helix loop⁻¹) x : Equiv.transportComp id helix loop⁻¹ x + ... = transportconst (ap helix loop)⁻¹ x : ap (transportconst · x) (Id.mapInv _ _) + ... = transportconst (ua Integer.succEquiv)⁻¹ x : ap (transportconst ·⁻¹ x) (recβrule₂ _ _) ... = Integer.pred x : ua.transportInvRule _ _ noncomputable hott def decode (x : S¹) : helix x → base = x := @@ -281,8 +281,8 @@ namespace Circle induction x; exact power; apply Theorems.funext; intro x; transitivity; apply Homotopy.Id (transportCharacterization power loop) x; transitivity; apply transportComposition; - transitivity; apply Id.map (power · ⬝ loop); apply transportBack; - transitivity; apply Id.map (· ⬝ loop); + transitivity; apply ap (power · ⬝ loop); apply transportBack; + transitivity; apply ap (· ⬝ loop); transitivity; symmetry; apply Loop.compPowerPred; apply Loop.invCompPowerComm; apply Id.cancelInvComp end @@ -295,11 +295,11 @@ namespace Circle noncomputable hott def windingPos : Π n, winding (power (Integer.pos n)) = Integer.pos n | Nat.zero => idp _ - | Nat.succ n => substOverPathComp _ _ _ ⬝ transportThere _ ⬝ Id.map _ (windingPos n) + | Nat.succ n => substOverPathComp _ _ _ ⬝ transportThere _ ⬝ ap _ (windingPos n) noncomputable hott def windingNeg : Π n, winding (power (Integer.neg n)) = Integer.neg n | Nat.zero => transportBack _ - | Nat.succ n => substOverPathComp _ _ _ ⬝ transportBack _ ⬝ Id.map _ (windingNeg n) + | Nat.succ n => substOverPathComp _ _ _ ⬝ transportBack _ ⬝ ap _ (windingNeg n) noncomputable hott def windingPower : Π z, winding (power z) = z | Integer.neg n => windingNeg n @@ -321,20 +321,20 @@ namespace Circle noncomputable example : winding loop⁻¹ = -1 := windingPower (Integer.neg 0) hott def rot : Π (x : S¹), x = x := - Circle.ind Circle.loop (begin - apply Id.trans; apply transportInvCompComp; change _ = idp _ ⬝ loop; - apply Id.map (· ⬝ loop); apply Id.invComp - end) + begin + fapply ind; exact loop; apply Id.trans; apply transportInvCompComp; + change _ = idp _ ⬝ loop; apply ap (· ⬝ loop); apply Id.invComp + end def μₑ : S¹ → S¹ ≃ S¹ := Circle.rec (ideqv S¹) (Sigma.prod (Theorems.funext rot) (Theorems.Equiv.biinvProp _ _ _)) def μ (x : S¹) : S¹ → S¹ := (μₑ x).forward - noncomputable hott def μLoop : Id.map μ loop = Theorems.funext rot := + noncomputable hott def μLoop : ap μ loop = Theorems.funext rot := begin transitivity; apply mapOverComp; - transitivity; apply Id.map; apply recβrule₂; + transitivity; apply ap; apply recβrule₂; apply Sigma.mapFstOverProd end @@ -342,46 +342,46 @@ namespace Circle hott def inv : S¹ → S¹ := rec base loop⁻¹ noncomputable hott def invInv (x : S¹) : inv (inv x) = x := - let invₚ := @Id.map S¹ S¹ base base (inv ∘ inv); + let invₚ := @ap S¹ S¹ base base (inv ∘ inv); begin induction x; reflexivity; apply calc - transport (λ x, inv (inv x) = x) loop Id.refl - = invₚ loop⁻¹ ⬝ Id.refl ⬝ loop : transportOverInvolution _ _ _ - ... = invₚ loop⁻¹ ⬝ (Id.refl ⬝ loop) : (Id.assoc _ _ _)⁻¹ - ... = Id.map inv (Id.map inv loop⁻¹) ⬝ loop : Id.map (· ⬝ loop) (mapOverComp _ _ _) - ... = Id.map inv (Id.map inv loop)⁻¹ ⬝ loop : Id.map (· ⬝ loop) (Id.map (Id.map inv) (Id.mapInv inv loop)) - ... = Id.map inv loop⁻¹⁻¹ ⬝ loop : @Id.map Ω¹(S¹) _ _ _ (Id.map inv ·⁻¹ ⬝ loop) (Circle.recβrule₂ base loop⁻¹) - ... = Id.map inv loop ⬝ loop : @Id.map Ω¹(S¹) _ _ _ (Id.map inv · ⬝ loop) (Id.invInv _) - ... = loop⁻¹ ⬝ loop : Id.map (· ⬝ loop) (Circle.recβrule₂ _ _) - ... = idp base : Id.invComp _ + transport (λ x, inv (inv x) = x) loop (idp base) + = invₚ loop⁻¹ ⬝ idp base ⬝ loop : transportOverInvolution _ _ _ + ... = invₚ loop⁻¹ ⬝ (idp base ⬝ loop) : (Id.assoc _ _ _)⁻¹ + ... = ap inv (ap inv loop⁻¹) ⬝ loop : ap (· ⬝ loop) (mapOverComp _ _ _) + ... = ap inv (ap inv loop)⁻¹ ⬝ loop : ap (· ⬝ loop) (ap (ap inv) (Id.mapInv inv loop)) + ... = ap inv loop⁻¹⁻¹ ⬝ loop : @ap Ω¹(S¹) _ _ _ (ap inv ·⁻¹ ⬝ loop) (Circle.recβrule₂ base loop⁻¹) + ... = ap inv loop ⬝ loop : @ap Ω¹(S¹) _ _ _ (ap inv · ⬝ loop) (Id.invInv _) + ... = loop⁻¹ ⬝ loop : ap (· ⬝ loop) (Circle.recβrule₂ _ _) + ... = idp base : Id.invComp _ end hott def unitLeft (x : S¹) : μ base x = x := idp x - hott def μRight : Id.map (μ base) loop = loop := Equiv.idmap _ + hott def μRight : ap (μ base) loop = loop := Equiv.idmap _ noncomputable hott def μLeft := calc - Id.map (μ · base) loop - = happly (Id.map μ loop) base : Interval.mapHapply _ _ - ... = (happly ∘ Theorems.funext) rot base : Id.map (λ f, happly f base) μLoop + ap (μ · base) loop + = happly (ap μ loop) base : Interval.mapHapply _ _ + ... = (happly ∘ Theorems.funext) rot base : ap (λ f, happly f base) μLoop ... = loop : happly (Theorems.happlyFunext _ _ rot) base noncomputable hott def unitRight (x : S¹) : μ x base = x := begin induction x; reflexivity; change _ = _; transitivity; apply transportOverInvolution (μ · base); - transitivity; apply Id.map (· ⬝ idp base ⬝ loop); - transitivity; apply Id.mapInv; apply Id.map; - apply μLeft; transitivity; apply Id.map (· ⬝ loop); + transitivity; apply ap (· ⬝ idp base ⬝ loop); + transitivity; apply Id.mapInv; apply ap; + apply μLeft; transitivity; apply ap (· ⬝ loop); apply Id.reflRight; apply Id.invComp end hott def μLeftApLem {x : S¹} (p : base = x) : - Id.map (μ · base) p = transport (base = ·) (unitRight x)⁻¹ p := + ap (μ · base) p = transport (base = ·) (unitRight x)⁻¹ p := begin induction p; reflexivity end - hott def μLeftAp (p : Ω¹(S¹)) : Id.map (μ · base) p = p := μLeftApLem p - hott def μRightAp (p : Ω¹(S¹)) : Id.map (μ base) p = p := Equiv.idmap p + hott def μLeftAp (p : Ω¹(S¹)) : ap (μ · base) p = p := μLeftApLem p + hott def μRightAp (p : Ω¹(S¹)) : ap (μ base) p = p := Equiv.idmap p noncomputable hott def unitComm (x : S¹) : μ base x = μ x base := (unitRight x)⁻¹ @@ -390,9 +390,9 @@ namespace Circle induction x; exact loop; change _ = _; transitivity; apply transportComp (base = ·) (AS μ inv) loop; transitivity; apply transportComposition; - transitivity; apply Id.map; apply Equiv.mapOverAS; - transitivity; apply Id.map; apply Id.map; apply Circle.recβrule₂; - transitivity; apply Id.map (· ⬝ Equiv.bimap μ loop loop⁻¹); + transitivity; apply ap; apply Equiv.mapOverAS; + transitivity; apply ap; apply ap; apply Circle.recβrule₂; + transitivity; apply ap (· ⬝ Equiv.bimap μ loop loop⁻¹); symmetry; apply μRight; symmetry; transitivity; symmetry; apply μLeft; apply bimapComp end @@ -403,7 +403,7 @@ namespace Circle begin intro x; induction x; exact f; change _ = _; transitivity; apply transportOverPi; apply Theorems.funext; intro y; induction y; - transitivity; apply Id.map; exact p; transitivity; apply apd; exact p⁻¹; apply setπ + transitivity; apply ap; exact p; transitivity; apply apd; exact p⁻¹; apply setπ end noncomputable hott def isGroupoid : groupoid S¹ := @@ -425,8 +425,8 @@ namespace Circle noncomputable hott def mulAssoc : Π x y z, μ x (μ y z) = μ (μ x y) z := begin intro x; fapply @lemSetTorus (λ y z, μ x (μ y z) = μ (μ x y) z); apply isGroupoid; - { intro z; apply Id.map (μ · z); exact (unitRight x)⁻¹ }; - { intro z; transitivity; apply Id.map; apply unitRight; symmetry; apply unitRight }; + { intro z; apply ap (μ · z); exact (unitRight x)⁻¹ }; + { intro z; transitivity; apply ap; apply unitRight; symmetry; apply unitRight }; { induction x; reflexivity; apply isGroupoid } end @@ -466,7 +466,7 @@ namespace Circle end noncomputable hott def Ωind₂ {π : Ω¹(S¹) → Type u} - (zeroπ : π Id.refl) (succπ : Π x, π x → π (loop ⬝ x)) + (zeroπ : π (idp base)) (succπ : Π x, π x → π (loop ⬝ x)) (predπ : Π x, π x → π (loop⁻¹ ⬝ x)) : Π x, π x := begin fapply Ωind₁; exact zeroπ; @@ -476,10 +476,8 @@ namespace Circle noncomputable hott def transComm {z : S¹} : Π (p q : z = z), p ⬝ q = q ⬝ p := begin - induction z; apply comm; - apply Theorems.funext; intro; - apply Theorems.funext; intro; - apply isGroupoid + induction z; apply comm; apply Theorems.funext; intro; + apply Theorems.funext; intro; apply isGroupoid end noncomputable hott def transportOverCircle {z : S¹} {f g : S¹ → S¹} {p : f = g} @@ -498,8 +496,8 @@ namespace Circle transitivity; apply transportOverContrMap; transitivity; apply Id.reflRight; transitivity; apply Id.mapInv; - transitivity; apply Id.map; apply mapOverComp; - transitivity; apply Id.map; apply Id.map (map (elim loop)); + transitivity; apply ap; apply mapOverComp; + transitivity; apply ap; apply ap (ap (elim loop)); change _ = idp 0; apply Structures.propIsSet; apply Interval.intervalProp; reflexivity end @@ -539,10 +537,10 @@ namespace Circle = succ (Ωrec zero succ pred p q r) := begin transitivity; apply transportToTransportconst; - transitivity; apply Id.map (transportconst · zero); - transitivity; apply mapFunctoriality; apply Id.map; apply recβrule₂; + transitivity; apply ap (transportconst · zero); + transitivity; apply mapFunctoriality; apply ap; apply recβrule₂; transitivity; apply transportconstOverComposition; - transitivity; apply ua.transportRule; apply Id.map succ; + transitivity; apply ua.transportRule; apply ap succ; symmetry; apply transportToTransportconst end @@ -551,12 +549,12 @@ namespace Circle = pred (Ωrec zero succ pred p q r) := begin transitivity; apply transportToTransportconst; - transitivity; apply Id.map (transportconst · zero); - transitivity; apply mapFunctoriality; apply Id.map; - transitivity; apply Id.mapInv; apply Id.map Id.symm; apply recβrule₂; + transitivity; apply ap (transportconst · zero); + transitivity; apply mapFunctoriality; apply ap; + transitivity; apply Id.mapInv; apply ap Id.symm; apply recβrule₂; transitivity; apply transportconstOverComposition; transitivity; apply transportconstOverInv; - transitivity; apply ua.transportInvRule; apply Id.map pred; + transitivity; apply ua.transportInvRule; apply ap pred; symmetry; apply transportToTransportconst end @@ -590,7 +588,7 @@ namespace Circle end hott def multSucc (p q : Ω¹(S¹)) : mult p (succ q) = mult p q ⬝ p := - begin transitivity; apply mapFunctoriality; apply Id.map; apply recβrule₂ end + begin transitivity; apply mapFunctoriality; apply ap; apply recβrule₂ end hott def multDistrRight (p q r : Ω¹(S¹)) : mult p (q ⬝ r) = mult p q ⬝ mult p r := by apply mapFunctoriality @@ -602,8 +600,8 @@ namespace Circle begin fapply ind; reflexivity; change _ = _; transitivity; apply Equiv.transportOverHmtpy; transitivity; - apply Id.map (· ⬝ _ ⬝ _); transitivity; apply mapInv; - apply Id.map; transitivity; apply Equiv.bimapBicom (rec a p) (rec b q); + apply ap (· ⬝ _ ⬝ _); transitivity; apply mapInv; + apply ap; transitivity; apply Equiv.bimapBicom (rec a p) (rec b q); apply bimap (bimap μ) <;> apply recβrule₂; transitivity; apply ap; apply recβrule₂; transitivity; symmetry; apply Id.assoc; apply Id.invComp; @@ -614,8 +612,8 @@ namespace Circle begin fapply ind; reflexivity; change _ = _; transitivity; apply Equiv.transportOverHmtpy; transitivity; - apply Id.map (· ⬝ _ ⬝ _); transitivity; apply mapInv; - apply Id.map; transitivity; apply mapOverComp; apply Id.map (mult p); apply recβrule₂; + apply ap (· ⬝ _ ⬝ _); transitivity; apply mapInv; + apply ap; transitivity; apply mapOverComp; apply ap (mult p); apply recβrule₂; transitivity; apply bimap; apply Id.reflRight; apply recβrule₂; apply Id.invComp end @@ -628,7 +626,7 @@ namespace Circle hott def mulNegRight (p q : Ω¹(S¹)) : mult p q⁻¹ = (mult p q)⁻¹ := by apply Id.mapInv - hott lemma mapExt {B : Type u} (φ : S¹ → B) : φ ~ rec (φ base) (Id.map φ loop) := + hott lemma mapExt {B : Type u} (φ : S¹ → B) : φ ~ rec (φ base) (ap φ loop) := begin fapply ind; reflexivity; change _ = _; transitivity; apply Equiv.transportOverHmtpy; transitivity; apply bimap; transitivity; apply Id.reflRight; apply Id.mapInv; @@ -645,7 +643,7 @@ namespace Circle { intro φ; symmetry; apply Theorems.funext; apply mapExt } end - hott lemma recBaseInj {x : S¹} (p q : x = x) (ε : rec x p = rec x q) : p = q := + noncomputable hott lemma recBaseInj {x : S¹} (p q : x = x) (ε : rec x p = rec x q) : p = q := begin have θ := ap (subst ε) (recβrule₂ x p)⁻¹ ⬝ apd (λ f, ap f loop) ε ⬝ recβrule₂ x q; apply transport (p = ·) θ _⁻¹; transitivity; apply Equiv.transportOverHmtpy; @@ -1112,7 +1110,7 @@ namespace Circle (p : b = c) (η : Π q, f (q ⬝ p⁻¹) = g q) : f =[λ x, a = x → B, p] g := begin induction p; apply Theorems.funext; intro; transitivity; - apply Id.map; apply Id.symm; apply Id.reflRight; apply η + apply ap; apply Id.symm; apply Id.reflRight; apply η end hott def transportPathMap {A : Type u} {B : Type v} {a b c : A} (φ : a = b → B) (p : b = c) (q : a = c) : @@ -1127,10 +1125,10 @@ namespace Circle hott def happlyRevFunextPath {q : b = a} : happly (depSymm p (funextPath f g p φ)) q⁻¹ - = transportPathMap g p⁻¹ q⁻¹ ⬝ (φ (q⁻¹ ⬝ p⁻¹⁻¹))⁻¹ ⬝ Id.map f (cancelInvComp _ _) := + = transportPathMap g p⁻¹ q⁻¹ ⬝ (φ (q⁻¹ ⬝ p⁻¹⁻¹))⁻¹ ⬝ ap f (cancelInvComp _ _) := begin induction p; induction q; transitivity; apply Interval.happly (Interval.happlyRev _); - transitivity; apply Id.map Id.symm; apply Interval.happly (Theorems.happlyFunext _ _ _); + transitivity; apply ap Id.symm; apply Interval.happly (Theorems.happlyFunext _ _ _); symmetry; apply Id.reflRight end end @@ -1161,14 +1159,14 @@ namespace Circle noncomputable hott def ΩEquivSuccInj {z : x = base} {w₁ w₂ : π z} (H : succπ z w₁ = succπ z w₂) : w₁ = w₂ := begin transitivity; apply Id.symm; apply coh₁; - transitivity; apply Id.map (subst _ ∘ predπ _); + transitivity; apply ap (subst _ ∘ predπ _); apply H; apply coh₁ end noncomputable hott def ΩEquivPredInj {z : x = base} {w₁ w₂ : π z} (H : predπ z w₁ = predπ z w₂) : w₁ = w₂ := begin transitivity; apply Id.symm; apply coh₂; - transitivity; apply Id.map (subst _ ∘ succπ _); + transitivity; apply ap (subst _ ∘ succπ _); apply H; apply coh₂ end @@ -1176,7 +1174,7 @@ namespace Circle ⟨λ H, subst (cancelInvComp z loop) (succπ _ H), (⟨predπ z, λ _, ΩEquivSuccInj π succπ predπ coh₁ ((transportForwardAndBack (cancelInvComp _ _) _)⁻¹ ⬝ - Id.map (subst _) (coh₂ _ _) ⬝ transportForwardAndBack _ _)⟩, + ap (subst _) (coh₂ _ _) ⬝ transportForwardAndBack _ _)⟩, ⟨predπ z, coh₂ _⟩)⟩ noncomputable hott def ΩHelix : Π y, x = y → Type u := @@ -1187,15 +1185,15 @@ namespace Circle = succπ z (subst (reflRight _) w) := begin induction z using J₂; transitivity; apply ΩJDef; - transitivity; apply Id.map (transportconst · _); - transitivity; apply Id.map (happly · _); apply indβrule₂; apply happlyFunextPath; + transitivity; apply ap (transportconst · _); + transitivity; apply ap (happly · _); apply indβrule₂; apply happlyFunextPath; transitivity; apply transportconstOverComposition; - transitivity; apply Id.map (transportconst _); apply meetTransportCoh (ΩHelix π succπ predπ coh₁ coh₂); + transitivity; apply ap (transportconst _); apply meetTransportCoh (ΩHelix π succπ predπ coh₁ coh₂); transitivity; apply ua.transportRule; show subst _ _ = _; transitivity; - apply Id.map (subst _); transitivity; transitivity; apply happly; + apply ap (subst _); transitivity; transitivity; apply happly; symmetry; apply apd succπ (compInv loop)⁻¹; apply happly; - apply transportImpl; apply Id.map (subst _); apply Id.map (succπ _); + apply transportImpl; apply ap (subst _); apply ap (succπ _); apply transportForwardAndBack; apply compInvCancelCoh end @@ -1204,19 +1202,19 @@ namespace Circle = predπ z (subst (reflRight _) w) := begin induction z using J₂; transitivity; apply ΩJDef; - transitivity; apply Id.map (transportconst · _); - transitivity; apply Id.map (happly · _); - transitivity; apply apdInv; apply Id.map (depSymm _); apply indβrule₂; apply happlyRevFunextPath; + transitivity; apply ap (transportconst · _); + transitivity; apply ap (happly · _); + transitivity; apply apdInv; apply ap (depSymm _); apply indβrule₂; apply happlyRevFunextPath; transitivity; apply transportconstOverComposition; - transitivity; apply Id.map (transportconst _); + transitivity; apply ap (transportconst _); transitivity; apply transportconstOverComposition; - transitivity; apply Id.map (transportconst _); apply meetTransportCoh (ΩHelix π succπ predπ coh₁ coh₂); + transitivity; apply ap (transportconst _); apply meetTransportCoh (ΩHelix π succπ predπ coh₁ coh₂); apply ua.transportInvRule; transitivity; symmetry; apply transportToTransportconst; show transport _ _ (predπ _ _) = _; transitivity; - apply Id.map (subst _); transitivity; transitivity; apply happly; + apply ap (subst _); transitivity; transitivity; apply happly; symmetry; apply apd predπ (compInv loop⁻¹)⁻¹; apply happly; - apply transportImpl; apply Id.map (subst _); apply Id.map (predπ _); + apply transportImpl; apply ap (subst _); apply ap (predπ _); apply transportForwardAndBack; apply compInvCancelCoh end end @@ -1240,7 +1238,7 @@ namespace Circle begin transitivity; apply JTrans; transitivity; apply ΩHelixSucc; - apply Id.map; apply transportBackAndForward + apply ap; apply transportBackAndForward end noncomputable hott def Ωindβ₃ (z : Ω¹(S¹)) : @@ -1249,7 +1247,7 @@ namespace Circle begin transitivity; apply JTrans; transitivity; apply ΩHelixPred; - apply Id.map; apply transportBackAndForward + apply ap; apply transportBackAndForward end end end Circle diff --git a/GroundZero/HITs/Coequalizer.lean b/GroundZero/HITs/Coequalizer.lean index 901032a..4820568 100644 --- a/GroundZero/HITs/Coequalizer.lean +++ b/GroundZero/HITs/Coequalizer.lean @@ -1,4 +1,6 @@ import GroundZero.HITs.Graph + +open GroundZero.Types.Id (ap) open GroundZero.Types.Equiv open GroundZero.Types @@ -35,7 +37,7 @@ namespace Coeq ind (λ _, C) i (λ x, pathoverOfEq (resp x) (ρ x)) noncomputable hott def recβrule (C : Type w) (i : B → C) - (ρ : Π x, i (f x) = i (g x)) : Π x, Id.map (rec C i ρ) (resp x) = ρ x := + (ρ : Π x, i (f x) = i (g x)) : Π x, ap (rec C i ρ) (resp x) = ρ x := begin intro x; apply pathoverOfEqInj (resp x); transitivity; symmetry; apply apdOverConstantFamily; @@ -43,4 +45,4 @@ namespace Coeq end end Coeq -end GroundZero.HITs \ No newline at end of file +end GroundZero.HITs diff --git a/GroundZero/HITs/Flattening.lean b/GroundZero/HITs/Flattening.lean index 9414fe9..7023488 100644 --- a/GroundZero/HITs/Flattening.lean +++ b/GroundZero/HITs/Flattening.lean @@ -1,6 +1,7 @@ import GroundZero.HITs.Coequalizer import GroundZero.Theorems.UA +open GroundZero.Types.Id (ap) open GroundZero.Types.Equiv open GroundZero.Types open GroundZero (ua) @@ -37,7 +38,7 @@ namespace Flattening begin fapply Sigma.prod; apply Coeq.resp; transitivity; apply transportToTransportconst; - transitivity; apply @Id.map _ _ (Id.map (P f g C D) (Coeq.resp x)) _ (transportconst · y); + transitivity; apply @ap _ _ (ap (P f g C D) (Coeq.resp x)) _ (transportconst · y); apply Coeq.recβrule (Type w) C (λ x, ua (D x)) x; apply GroundZero.ua.transportRule end @@ -45,4 +46,4 @@ namespace Flattening begin fapply Coeq.rec; intro w; apply iotaφ w.1 w.2; intro w; apply respφ w.1 w.2 end end Flattening -end GroundZero.HITs \ No newline at end of file +end GroundZero.HITs diff --git a/GroundZero/HITs/Graph.lean b/GroundZero/HITs/Graph.lean index cf5b478..f85342e 100644 --- a/GroundZero/HITs/Graph.lean +++ b/GroundZero/HITs/Graph.lean @@ -1,4 +1,6 @@ import GroundZero.Types.HEq + +open GroundZero.Types.Id (ap) open GroundZero.Types namespace GroundZero.HITs @@ -34,11 +36,11 @@ namespace Graph axiom recβrule {A : Type u} {B : Type v} {R : A → A → Type w} (f : A → B) (h : Π x y, R x y → f x = f y) {x y : A} (g : R x y) : - Id.map (rec f h) (line g) = h x y g + ap (rec f h) (line g) = h x y g axiom indβrule {A : Type u} {R : A → A → Type w} {B : Graph R → Type v} (f : Π x, B (elem x)) (h : Π x y (H : R x y), f x =[line H] f y) {x y : A} (g : R x y) : Equiv.apd (ind f h) (line g) = h x y g end Graph -end GroundZero.HITs \ No newline at end of file +end GroundZero.HITs diff --git a/GroundZero/HITs/Int.lean b/GroundZero/HITs/Int.lean index 8e1bb2e..821a101 100644 --- a/GroundZero/HITs/Int.lean +++ b/GroundZero/HITs/Int.lean @@ -1,4 +1,6 @@ import GroundZero.Theorems.Nat + +open GroundZero.Types.Id (ap) open GroundZero.Types open GroundZero @@ -58,8 +60,8 @@ namespace Int begin apply glue; transitivity; symmetry; apply Theorems.Nat.assoc; symmetry; transitivity; symmetry; apply Theorems.Nat.assoc; - apply Id.map (λ n, n + k); apply Theorems.Nat.comm + apply ap (λ n, n + k); apply Theorems.Nat.comm end end Int -end GroundZero.HITs \ No newline at end of file +end GroundZero.HITs diff --git a/GroundZero/HITs/Interval.lean b/GroundZero/HITs/Interval.lean index 788a12c..aa86047 100644 --- a/GroundZero/HITs/Interval.lean +++ b/GroundZero/HITs/Interval.lean @@ -1,6 +1,8 @@ import GroundZero.Structures + open GroundZero.Structures GroundZero.Types open GroundZero.Theorems (funext) +open GroundZero.Types.Id (ap) open GroundZero.Types.Equiv namespace GroundZero @@ -61,7 +63,7 @@ namespace Interval infix:70 " ∨ " => max hott def elim {A : Type u} {a b : A} (p : a = b) : I → A := rec a b p - hott def lam {A : Type u} (f : I → A) : f 0 = f 1 := Id.map f seg + hott def lam {A : Type u} (f : I → A) : f 0 = f 1 := ap f seg hott def connAnd {A : Type u} {a b : A} (p : a = b) : Π i, a = elim p i := @@ -75,37 +77,37 @@ namespace Interval {a : A} (f : A → B) : cong f (idp a) = idp (f a) := begin transitivity; apply mapOverComp; - transitivity; apply Id.map; + transitivity; apply ap; apply recβrule; reflexivity end noncomputable hott def mapEqCong {A : Type u} {B : Type v} {a b : A} - (f : A → B) (p : a = b) : Id.map f p = cong f p := + (f : A → B) (p : a = b) : ap f p = cong f p := begin induction p; symmetry; apply congRefl end noncomputable hott def negNeg : Π x, neg (neg x) = x := ind (idp i₀) (idp i₁) (calc transport (λ x, neg (neg x) = x) seg (idp i₀) = - (@Id.map I I i₁ i₀ (neg ∘ neg) seg⁻¹) ⬝ idp i₀ ⬝ seg : + (@ap I I i₁ i₀ (neg ∘ neg) seg⁻¹) ⬝ idp i₀ ⬝ seg : by apply transportOverInvolution - ... = Id.map neg (Id.map neg seg⁻¹) ⬝ idp i₀ ⬝ seg : - begin apply Id.map (λ p, p ⬝ idp i₀ ⬝ seg); + ... = ap neg (ap neg seg⁻¹) ⬝ idp i₀ ⬝ seg : + begin apply ap (λ p, p ⬝ idp i₀ ⬝ seg); apply mapOverComp end - ... = Id.map neg (Id.map neg seg)⁻¹ ⬝ idp i₀ ⬝ seg : - begin apply Id.map (λ p, p ⬝ idp i₀ ⬝ seg); - apply Id.map; apply Id.mapInv end - ... = Id.map neg seg⁻¹⁻¹ ⬝ idp i₀ ⬝ seg : - begin apply Id.map (λ p, p ⬝ idp i₀ ⬝ seg); - apply Id.map; apply Id.map Types.Id.symm; + ... = ap neg (ap neg seg)⁻¹ ⬝ idp i₀ ⬝ seg : + begin apply ap (λ p, p ⬝ idp i₀ ⬝ seg); + apply ap; apply Id.mapInv end + ... = ap neg seg⁻¹⁻¹ ⬝ idp i₀ ⬝ seg : + begin apply ap (λ p, p ⬝ idp i₀ ⬝ seg); + apply ap; apply ap Types.Id.symm; apply recβrule end - ... = Id.map neg seg ⬝ idp i₀ ⬝ seg : - begin apply Id.map (λ (p : i₀ = i₁), Id.map neg p ⬝ idp i₀ ⬝ seg); + ... = ap neg seg ⬝ idp i₀ ⬝ seg : + begin apply ap (λ (p : i₀ = i₁), ap neg p ⬝ idp i₀ ⬝ seg); apply Id.invInv end ... = seg⁻¹ ⬝ idp i₀ ⬝ seg : - begin apply Id.map (· ⬝ idp i₀ ⬝ seg); + begin apply ap (· ⬝ idp i₀ ⬝ seg); apply recβrule end ... = seg⁻¹ ⬝ seg : - begin apply Id.map (· ⬝ seg); + begin apply ap (· ⬝ seg); apply Id.reflRight end ... = idp i₁ : by apply Id.invComp) @@ -116,14 +118,14 @@ namespace Interval ⟨neg, ⟨⟨neg, negNeg'⟩, ⟨neg, negNeg'⟩⟩⟩ noncomputable hott def lineRec {A : Type u} (p : I → A) : - rec (p 0) (p 1) (Id.map p seg) = p := + rec (p 0) (p 1) (ap p seg) = p := begin apply Theorems.funext; intro x; induction x; reflexivity; reflexivity; change _ = _; transitivity; apply Equiv.transportOverHmtpy; - transitivity; apply Id.map (· ⬝ Id.map p seg); + transitivity; apply ap (· ⬝ ap p seg); transitivity; apply Id.reflRight; - transitivity; apply Id.mapInv; apply Id.map; + transitivity; apply Id.mapInv; apply ap; apply recβrule; apply Id.invComp end @@ -132,7 +134,7 @@ namespace Interval @transport I (λ i, π (elim p i)) 0 1 Interval.seg u = subst p u := begin transitivity; apply transportComp; - transitivity; apply Id.map (subst · u); + transitivity; apply ap (subst · u); apply recβrule; reflexivity end @@ -142,4 +144,4 @@ namespace Interval end Interval end HITs -end GroundZero \ No newline at end of file +end GroundZero diff --git a/GroundZero/HITs/Join.lean b/GroundZero/HITs/Join.lean index 3da3244..b49d4fd 100644 --- a/GroundZero/HITs/Join.lean +++ b/GroundZero/HITs/Join.lean @@ -1,4 +1,5 @@ import GroundZero.HITs.Suspension + open GroundZero.Types.Equiv (pathoverOfEq) open GroundZero.Types @@ -44,4 +45,4 @@ namespace Join | true => λ _, idp _) end Join -end GroundZero.HITs \ No newline at end of file +end GroundZero.HITs diff --git a/GroundZero/HITs/Merely.lean b/GroundZero/HITs/Merely.lean index 8cd7f5f..57fbf17 100644 --- a/GroundZero/HITs/Merely.lean +++ b/GroundZero/HITs/Merely.lean @@ -52,7 +52,7 @@ namespace Merely begin transitivity; { symmetry; apply Colimit.glue }; symmetry; transitivity; { symmetry; apply Colimit.glue }; - apply map; apply Generalized.glue + apply ap; apply Generalized.glue end hott def incl {A : Type u} {n : ℕ} := @@ -72,7 +72,7 @@ namespace Merely hott def inclUniq {A : Type u} {n : ℕ} (a b : Generalized.rep A n) : incl a = incl b := calc incl a = incl (Generalized.dep A n a) : glue⁻¹ - ... = incl (Generalized.dep A n b) : Id.map incl (Generalized.glue a b) + ... = incl (Generalized.dep A n b) : ap incl (Generalized.glue a b) ... = incl b : glue hott def inclZeroEqIncl {A : Type u} {n : ℕ} (x : A) @@ -81,32 +81,32 @@ namespace Merely ... = incl y : inclUniq (exactNth x n) y hott def weaklyConstantAp {A : Type u} {B : Type v} (f : A → B) - {a b : A} (p q : a = b) (H : Π a b, f a = f b) : Id.map f p = Id.map f q := - let L : Π {u v : A} (r : u = v), (H a u)⁻¹ ⬝ H a v = Id.map f r := + {a b : A} (p q : a = b) (H : Π a b, f a = f b) : ap f p = ap f q := + let L : Π {u v : A} (r : u = v), (H a u)⁻¹ ⬝ H a v = ap f r := begin intros u v r; induction r; apply Types.Id.invComp end; (L p)⁻¹ ⬝ L q hott def congClose {A : Type u} {n : ℕ} {a b : Generalized.rep A n} (p : a = b) : - glue⁻¹ ⬝ Id.map incl (Id.map (Generalized.dep A n) p) ⬝ glue = Id.map incl p := + glue⁻¹ ⬝ ap incl (ap (Generalized.dep A n) p) ⬝ glue = ap incl p := begin induction p; transitivity; { symmetry; apply Id.assoc }; apply Equiv.rewriteComp; symmetry; apply Id.reflRight end hott def congOverPath {A : Type u} {n : ℕ} {a b : Generalized.rep A n} - (p q : a = b) : Id.map incl p = Id.map incl q := + (p q : a = b) : ap incl p = ap incl q := weaklyConstantAp incl p q inclUniq hott def glueClose {A : Type u} {n : ℕ} {a b : Generalized.rep A n} : - glue⁻¹ ⬝ Id.map incl (Generalized.glue (Generalized.dep A n a) (Generalized.dep A n b)) ⬝ glue - = Id.map incl (Generalized.glue a b) := + glue⁻¹ ⬝ ap incl (Generalized.glue (Generalized.dep A n a) (Generalized.dep A n b)) ⬝ glue + = ap incl (Generalized.glue a b) := begin symmetry; transitivity; { symmetry; apply @congClose A (n + 1) _ _ (Generalized.glue a b) }; - apply map (· ⬝ glue); apply map; apply congOverPath + apply ap (· ⬝ glue); apply ap; apply congOverPath end hott def inclUniqClose {A : Type u} {n : ℕ} (a b : Generalized.rep A n) : glue⁻¹ ⬝ inclUniq (Generalized.dep A n a) (Generalized.dep A n b) ⬝ glue = inclUniq a b := - Id.map (· ⬝ glue) (Id.map _ glueClose) + ap (· ⬝ glue) (ap _ glueClose) hott def uniq {A : Type u} : prop ∥A∥ := begin @@ -114,12 +114,12 @@ namespace Merely { intro x; existsi elem x; fapply Colimit.ind <;> intros n y; { apply inclZeroEqIncl }; { apply pathoverFromTrans; symmetry; transitivity; - apply Id.map (_ ⬝ ·); symmetry; apply inclUniqClose; - symmetry; transitivity; apply Id.map (· ⬝ _ ⬝ _); apply Id.explodeInv; + apply ap (_ ⬝ ·); symmetry; apply inclUniqClose; + symmetry; transitivity; apply ap (· ⬝ _ ⬝ _); apply Id.explodeInv; -- TODO: use “iterate” here transitivity; symmetry; apply Id.assoc; transitivity; symmetry; apply Id.assoc; - apply Id.map ((nthGlue x n)⁻¹ ⬝ ·); apply Id.assoc } }; + apply ap ((nthGlue x n)⁻¹ ⬝ ·); apply Id.assoc } }; { intro x; apply Structures.contrIsProp } end @@ -147,4 +147,4 @@ namespace Merely rec Structures.emptyIsProp end Merely -end GroundZero.HITs \ No newline at end of file +end GroundZero.HITs diff --git a/GroundZero/HITs/Moebius.lean b/GroundZero/HITs/Moebius.lean index 893ac85..2246457 100644 --- a/GroundZero/HITs/Moebius.lean +++ b/GroundZero/HITs/Moebius.lean @@ -1,4 +1,6 @@ import GroundZero.HITs.Circle + +open GroundZero.Types.Id (ap) open GroundZero namespace GroundZero.HITs @@ -18,17 +20,17 @@ noncomputable hott def C.const : Π x, C x = I := begin intro x; induction x; reflexivity; change _ = _; transitivity; apply Equiv.transportOverContrMap; - transitivity; apply Id.map (· ⬝ idp I); - transitivity; apply Id.mapInv; apply Id.map; + transitivity; apply ap (· ⬝ idp I); + transitivity; apply Id.mapInv; apply ap; apply Circle.recβrule₂; reflexivity end noncomputable hott def cylEqv : cylinder' ≃ cylinder := begin transitivity; - { apply Equiv.idtoeqv; apply Id.map; + { apply Equiv.idtoeqv; apply ap; apply Theorems.funext; exact C.const }; { apply Sigma.const } end -end GroundZero.HITs \ No newline at end of file +end GroundZero.HITs diff --git a/GroundZero/HITs/Pushout.lean b/GroundZero/HITs/Pushout.lean index 4a55c8b..b36e287 100644 --- a/GroundZero/HITs/Pushout.lean +++ b/GroundZero/HITs/Pushout.lean @@ -1,4 +1,6 @@ import GroundZero.HITs.Graph + +open GroundZero.Types.Id (ap) open GroundZero.Types.Equiv open GroundZero.Types @@ -55,7 +57,7 @@ namespace Pushout noncomputable hott def recβrule {D : Type w} (inlπ : A → D) (inrπ : B → D) (glueπ : Π x, inlπ (f x) = inrπ (g x)) (x : C) : - Id.map (rec inlπ inrπ glueπ) (glue x) = glueπ x := + ap (rec inlπ inrπ glueπ) (glue x) = glueπ x := begin apply pathoverOfEqInj (glue x); transitivity; symmetry; apply apdOverConstantFamily; @@ -64,4 +66,4 @@ namespace Pushout end Pushout end HITs -end GroundZero \ No newline at end of file +end GroundZero diff --git a/GroundZero/HITs/Quotient.lean b/GroundZero/HITs/Quotient.lean index 93c60f6..2008514 100644 --- a/GroundZero/HITs/Quotient.lean +++ b/GroundZero/HITs/Quotient.lean @@ -1,6 +1,7 @@ import GroundZero.HITs.Trunc import GroundZero.HITs.Graph +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Theorems open GroundZero.Types @@ -16,7 +17,7 @@ Trunc.elem ∘ Graph.elem hott def Quot.sound {A : Type u} {R : A → A → propset.{v}} {a b : A} : (R a b).1 → @Id (Quot R) (Quot.elem a) (Quot.elem b) := -begin intro H; apply Id.map Trunc.elem; apply Graph.line; assumption end +begin intro H; apply ap Trunc.elem; apply Graph.line; assumption end noncomputable hott def Quot.set {A : Type u} {R : A → A → propset.{v}} : hset (Quot R) := zeroEqvSet.forward (Trunc.uniq 0) @@ -100,4 +101,4 @@ begin repeat { assumption } end -end GroundZero.HITs \ No newline at end of file +end GroundZero.HITs diff --git a/GroundZero/HITs/Reals.lean b/GroundZero/HITs/Reals.lean index 6a27cf7..8c7d605 100644 --- a/GroundZero/HITs/Reals.lean +++ b/GroundZero/HITs/Reals.lean @@ -51,7 +51,7 @@ namespace Reals noncomputable hott def recβrule {A : Type u} (cz : ℤ → A) (sz : Π z, cz z = cz (Integer.succ z)) (z : ℤ) : - Id.map (rec cz sz) (glue z) = sz z := + ap (rec cz sz) (glue z) = sz z := begin apply Equiv.pathoverOfEqInj (glue z); transitivity; symmetry; apply Equiv.apdOverConstantFamily; @@ -81,7 +81,7 @@ namespace Reals | Integer.neg n => _; induction n using Nat.casesOn; apply Id.invComp; { transitivity; symmetry; apply Id.assoc; - transitivity; apply Id.map; apply Id.invComp; + transitivity; apply ap; apply Id.invComp; apply Id.reflRight } end)⟩ @@ -102,16 +102,16 @@ namespace Reals hott def helixOverHomo (x : A.1) : helix (φ.ap x) = ℤ := begin - transitivity; apply map (helix ∘ φ.ap); + transitivity; apply ap (helix ∘ φ.ap); apply H x A.point; change _ = helix base; - apply map helix; apply φ.id + apply ap helix; apply φ.id end noncomputable hott def fibOfHomo (x : S¹) := calc fib φ.ap x ≃ Σ (z : A.1), φ.ap z = x : Equiv.ideqv (fib φ.ap x) - ... = Σ (z : A.1), φ.ap A.point = x : Id.map Sigma (funext (λ z, Id.map (φ.ap · = x) (H z A.point))) - ... = Σ (z : A.1), base = x : Id.map Sigma (funext (λ _, Id.map (· = x) φ.id)) - ... = Σ (z : A.1), helix x : Id.map Sigma (funext (λ _, GroundZero.ua (Circle.family x))) + ... = Σ (z : A.1), φ.ap A.point = x : ap Sigma (funext (λ z, ap (φ.ap · = x) (H z A.point))) + ... = Σ (z : A.1), base = x : ap Sigma (funext (λ _, ap (· = x) φ.id)) + ... = Σ (z : A.1), helix x : ap Sigma (funext (λ _, GroundZero.ua (Circle.family x))) ... ≃ A.1 × (helix x) : Sigma.const A.1 (helix x) ... ≃ 𝟏 × (helix x) : ua.productEquiv₃ (contrEquivUnit.{_, 0} ⟨A.point, H A.point⟩) (Equiv.ideqv (helix x)) ... ≃ helix x : prodUnitEquiv (helix x) @@ -141,20 +141,20 @@ namespace Reals case sz z => { change _ = _; let p := Integer.shift z; apply calc Equiv.transport (λ x, helix (cis x) = ℤ) (glue z) (Integer.shift z)⁻¹ - = @Id.map R Type _ _ (helix ∘ cis) (glue z)⁻¹ ⬝ (Integer.shift z)⁻¹ : + = @ap R Type _ _ (helix ∘ cis) (glue z)⁻¹ ⬝ (Integer.shift z)⁻¹ : Equiv.transportOverContrMap _ _ _ - ... = (Id.map (helix ∘ cis) (glue z))⁻¹ ⬝ (Integer.shift z)⁻¹ : - Id.map (· ⬝ p⁻¹) (Id.mapInv _ _) - ... = (Id.map helix (Id.map cis (glue z)))⁻¹ ⬝ (Integer.shift z)⁻¹ : - Id.map (·⁻¹ ⬝ p⁻¹) (Equiv.mapOverComp _ _ _) - ... = (Id.map helix loop)⁻¹ ⬝ (Integer.shift z)⁻¹ : - begin apply Id.map (·⁻¹ ⬝ p⁻¹); apply Id.map; apply recβrule end + ... = (ap (helix ∘ cis) (glue z))⁻¹ ⬝ (Integer.shift z)⁻¹ : + ap (· ⬝ p⁻¹) (Id.mapInv _ _) + ... = (ap helix (ap cis (glue z)))⁻¹ ⬝ (Integer.shift z)⁻¹ : + ap (·⁻¹ ⬝ p⁻¹) (Equiv.mapOverComp _ _ _) + ... = (ap helix loop)⁻¹ ⬝ (Integer.shift z)⁻¹ : + begin apply ap (·⁻¹ ⬝ p⁻¹); apply ap; apply recβrule end ... = Integer.succPath⁻¹ ⬝ (Integer.shift z)⁻¹ : - begin apply Id.map (·⁻¹ ⬝ p⁻¹); apply Circle.recβrule₂ end + begin apply ap (·⁻¹ ⬝ p⁻¹); apply Circle.recβrule₂ end ... = (Integer.shift z ⬝ Integer.succPath)⁻¹ : (Id.explodeInv _ _)⁻¹ ... = (Integer.shift (Integer.succ z))⁻¹ : - Id.map _ (Integer.shiftComp _) + ap _ (Integer.shiftComp _) } end diff --git a/GroundZero/HITs/Suspension.lean b/GroundZero/HITs/Suspension.lean index f84d5e9..f1ea5b3 100644 --- a/GroundZero/HITs/Suspension.lean +++ b/GroundZero/HITs/Suspension.lean @@ -1,6 +1,7 @@ import GroundZero.HITs.Pushout import GroundZero.Types.Unit +open GroundZero.Types.Id (ap) open GroundZero.Types.Equiv open GroundZero.Types @@ -42,7 +43,7 @@ namespace Suspension by apply Pushout.indβrule noncomputable hott def recβrule {A : Type u} {B : Type v} (n s : B) - (m : A → n = s) (x : A) : Id.map (rec n s m) (merid x) = m x := + (m : A → n = s) (x : A) : ap (rec n s m) (merid x) = m x := by apply Pushout.recβrule end Suspension diff --git a/GroundZero/HITs/Topologization.lean b/GroundZero/HITs/Topologization.lean index 3125e13..b281cb8 100644 --- a/GroundZero/HITs/Topologization.lean +++ b/GroundZero/HITs/Topologization.lean @@ -1,4 +1,5 @@ import GroundZero.Algebra.Reals + open GroundZero.Structures open GroundZero.Types open GroundZero @@ -27,4 +28,4 @@ namespace GroundZero.HITs noncomputable hott def D.η₁ {a b : A} (R : r a b) : D.ρ R 1 = D.ε b := Graph.line (D.rel.η₁ R) end -end GroundZero.HITs \ No newline at end of file +end GroundZero.HITs diff --git a/GroundZero/HITs/Trunc.lean b/GroundZero/HITs/Trunc.lean index d88e6f3..e97dcb5 100644 --- a/GroundZero/HITs/Trunc.lean +++ b/GroundZero/HITs/Trunc.lean @@ -1,4 +1,6 @@ import GroundZero.Structures + +open GroundZero.Types.Id (ap) open GroundZero.Structures namespace GroundZero.HITs @@ -38,7 +40,7 @@ namespace Trunc (f g : ∥A∥ₙ → B) (H : f ∘ elem = g ∘ elem) : f = g := begin apply GroundZero.Theorems.funext; fapply ind <;> intro x; - { exact Types.Id.map (λ (f : A → B), f x) H }; + { exact ap (λ (f : A → B), f x) H }; { apply hlevel.cumulative; assumption } end @@ -63,4 +65,4 @@ namespace Trunc rec (lift ∘ f) (piRespectsNType n (λ _, uniq n)) end Trunc -end GroundZero.HITs \ No newline at end of file +end GroundZero.HITs diff --git a/GroundZero/Modal/Disc.lean b/GroundZero/Modal/Disc.lean index a891da8..f6fed21 100644 --- a/GroundZero/Modal/Disc.lean +++ b/GroundZero/Modal/Disc.lean @@ -33,7 +33,7 @@ noncomputable section λ τ, ⟨f τ.1, d f τ.1 τ.2⟩ end -hott def infProxApIdp {A : Type u} {a b : A} (ρ : a ~ b) : infProxAp idfun ρ = ρ := +noncomputable hott def infProxApIdp {A : Type u} {a b : A} (ρ : a ~ b) : infProxAp idfun ρ = ρ := begin symmetry; transitivity; symmetry; apply Equiv.idmap; transitivity; apply mapWithHomotopy _ _ Im.apIdfun; @@ -41,7 +41,7 @@ begin transitivity; apply Id.ap; apply Im.indεβrule; apply Id.invInv end -hott def infProxApCom {A : Type u} {B : Type v} {C : Type w} (f : B → C) (g : A → B) +noncomputable hott def infProxApCom {A : Type u} {B : Type v} {C : Type w} (f : B → C) (g : A → B) {a b : A} (ρ : a ~ b) : infProxAp (f ∘ g) ρ = infProxAp f (infProxAp g ρ) := begin transitivity; apply Id.ap (_ ⬝ · ⬝ _); @@ -104,4 +104,4 @@ hott def Homogeneous.cart (A B : Homogeneous) : Homogeneous := instance : HMul Homogeneous Homogeneous Homogeneous := ⟨Homogeneous.cart⟩ -end GroundZero.HITs.Infinitesimal \ No newline at end of file +end GroundZero.HITs.Infinitesimal diff --git a/GroundZero/Modal/Infinitesimal.lean b/GroundZero/Modal/Infinitesimal.lean index c8a5222..7e87feb 100644 --- a/GroundZero/Modal/Infinitesimal.lean +++ b/GroundZero/Modal/Infinitesimal.lean @@ -1,6 +1,7 @@ import GroundZero.Types.Equiv open GroundZero.Types.Equiv (biinv) +open GroundZero.Types.Id (ap) open GroundZero.Types open GroundZero.Proto @@ -40,7 +41,7 @@ noncomputable hott def κ.right {A : Type u} {a b : ℑ A} : @κ A a b ∘ ι ~ @Id.rec (ℑ A) a (λ b p, κ (ι p) = p) κ.idp b noncomputable hott def κ.left {A : Type u} {a b : ℑ A} : ι ∘ @κ A a b ~ idfun := -λ ρ, κ (@Im.ind (a = b) (λ ρ, ι (κ ρ) = ρ) (λ p, ι (Id.map ι (κ.right p))) ρ) +λ ρ, κ (@Im.ind (a = b) (λ ρ, ι (κ ρ) = ρ) (λ p, ι (ap ι (κ.right p))) ρ) hott def isCoreduced (A : Type u) := biinv (@ι A) @@ -56,7 +57,7 @@ noncomputable hott def Im.indε {A : Type u} {B : ℑ A → Type v} (η : Π i, noncomputable def Im.indεβrule {A : Type u} {B : ℑ A → Type v} (η : Π i, isCoreduced (B i)) (f : Π x, B (ι x)) : Π x, Im.indε η f (ι x) = f x := -λ a, Id.map (η (ι a)).1.1 (Im.indβrule a) ⬝ (η (ι a)).1.2 (f a) +λ a, ap (η (ι a)).1.1 (Im.indβrule a) ⬝ (η (ι a)).1.2 (f a) noncomputable section variable {A : Type u} {B : Type v} (f : A → ℑ B) @@ -89,6 +90,6 @@ noncomputable hott def Im.apCom {A : Type u} {B : Type v} {C : Type w} (f : B → C) (g : A → B) : Im.ap (f ∘ g) ~ Im.ap f ∘ Im.ap g := Im.indε (λ _, Im.idCoreduced _ _) (λ _, Im.naturality _ _ ⬝ (Im.naturality f _)⁻¹ - ⬝ Id.map (ap f) (Im.naturality g _)⁻¹) + ⬝ Id.ap (ap f) (Im.naturality g _)⁻¹) -end GroundZero.HITs.Infinitesimal \ No newline at end of file +end GroundZero.HITs.Infinitesimal diff --git a/GroundZero/Structures.lean b/GroundZero/Structures.lean index 47f35aa..7f81535 100644 --- a/GroundZero/Structures.lean +++ b/GroundZero/Structures.lean @@ -3,10 +3,10 @@ import GroundZero.Types.Sigma import GroundZero.Types.Product import GroundZero.Types.Coproduct -open GroundZero.Types.Unit -open GroundZero.Types.Id (map) open GroundZero.Types (Coproduct idp fib) open GroundZero.Types.Equiv (biinv) +open GroundZero.Types.Id (ap) +open GroundZero.Types.Unit namespace GroundZero universe u v w k r @@ -184,7 +184,7 @@ section hott def contrIsProp {A : Type u} : prop (contr A) := begin intro ⟨x, u⟩ ⟨y, v⟩; have p := u y; - induction p; apply map; + induction p; apply ap; apply HITs.Interval.funext; intro a; apply propIsSet (contrImplProp ⟨x, u⟩) end @@ -222,19 +222,19 @@ hott def retract (B : Type u) (A : Type v) := hott def retract.section {B : Type u} {A : Type v} (w : retract B A) : B → A := w.2.1 hott def contrRetract {A : Type u} {B : Type v} : retract B A → contr A → contr B := -λ ⟨r, s, ε⟩ ⟨a₀, p⟩, ⟨r a₀, λ b, map r (p (s b)) ⬝ (ε b)⟩ +λ ⟨r, s, ε⟩ ⟨a₀, p⟩, ⟨r a₀, λ b, ap r (p (s b)) ⬝ (ε b)⟩ hott def retract.path {A : Type u} {B : Type v} : Π (H : retract B A) {a b : B}, retract (a = b) (H.section a = H.section b) := -λ ⟨r, s, ε⟩ a b, ⟨λ q, (ε a)⁻¹ ⬝ (@map A B _ _ r q) ⬝ (ε b), map s, +λ ⟨r, s, ε⟩ a b, ⟨λ q, (ε a)⁻¹ ⬝ (@ap A B _ _ r q) ⬝ (ε b), ap s, begin intro p; transitivity; symmetry; apply Types.Id.assoc; symmetry; apply Types.Equiv.invRewriteComp; - transitivity; apply map (· ⬝ p); apply Types.Id.invInv; - transitivity; apply map (ε a ⬝ ·); symmetry; apply Types.Equiv.idmap; + transitivity; apply ap (· ⬝ p); apply Types.Id.invInv; + transitivity; apply ap (ε a ⬝ ·); symmetry; apply Types.Equiv.idmap; transitivity; apply Types.Equiv.homotopySquare ε p; - apply map (· ⬝ ε b); apply Types.Equiv.mapOverComp + apply ap (· ⬝ ε b); apply Types.Equiv.mapOverComp end⟩ hott def equivRespectsRetraction : Π {n : ℕ₋₂} {A : Type u} {B : Type v}, @@ -411,7 +411,7 @@ begin apply Types.Id.transCancelLeft (f a a (ρ a)); transitivity; symmetry; apply Types.Equiv.transportComposition; transitivity; apply Types.Equiv.liftedHapply (R a); apply Types.Equiv.apd (f a) p; - transitivity; apply map (f a a) (h _ _ _ (ρ a)); symmetry; apply Types.Id.reflRight + transitivity; apply ap (f a a) (h _ _ _ (ρ a)); symmetry; apply Types.Id.reflRight end hott def doubleNegEq {A : Type u} (h : Π (x y : A), ¬¬(x = y) → x = y) : hset A := @@ -451,9 +451,9 @@ section hott def zeroPath {A B : 0-Type} (p : A.fst = B.fst) : A = B := begin fapply Sigma.prod; exact p; apply ntypeIsProp end - hott def zeroPathRefl (A : 0-Type) : @zeroPath A A Id.refl = Id.refl := + hott def zeroPathRefl (A : 0-Type) : @zeroPath A A (idp A.1) = idp A := begin - transitivity; apply Id.map (Sigma.prod (idp _)); change _ = Id.refl; + transitivity; apply ap (Sigma.prod (idp _)); change _ = idp _; apply propIsSet (ntypeIsProp 0); apply Sigma.prodRefl end end @@ -506,7 +506,7 @@ namespace Theorems begin existsi Sigma.mk f (Homotopy.id f); intro ⟨g, H⟩; change r (λ x, Sigma.mk (f x) (idp _)) = r (s g H); - apply Id.map r; apply contrImplProp; + apply ap r; apply contrImplProp; apply weak; intro x; apply singl.contr end @@ -518,7 +518,7 @@ namespace Theorems hott lemma homotopyIndId : homotopyInd f r f (Homotopy.id f) = r := begin - transitivity; apply Id.map + transitivity; apply ap (λ p, @transport (Σ g, f ~ g) (λ p, π p.fst p.snd) ⟨f, Homotopy.id f⟩ ⟨f, Homotopy.id f⟩ p r); change _ = idp _; apply propIsSet; apply contrImplProp; @@ -541,7 +541,7 @@ namespace Theorems (f g : Π x, B x) : HITs.Interval.happly ∘ @funext A B f g ~ id := begin intro H; fapply @homotopyInd _ _ f (λ g G, HITs.Interval.happly (funext G) = G) _ g H; - change _ = HITs.Interval.happly (idp _); apply Id.map HITs.Interval.happly; + change _ = HITs.Interval.happly (idp _); apply ap HITs.Interval.happly; change homotopyInd _ _ _ _ = _; apply homotopyIndId end @@ -557,12 +557,12 @@ namespace Theorems open GroundZero.Types.Equiv (transport) hott lemma mapHomotopy {A : Type u} {B : Type v} {a b : A} (f g : A → B) (p : a = b) (q : f ~ g) : - Id.map g p = @transport (A → B) (λ h, h a = h b) f g (funext q) (Id.map f p) := + ap g p = @transport (A → B) (λ h, h a = h b) f g (funext q) (ap f p) := begin induction p; symmetry; transitivity; apply Types.Equiv.transportOverHmtpy; - transitivity; apply Id.map (· ⬝ Id.map (λ (h : A → B), h a) (funext q)); + transitivity; apply ap (· ⬝ ap (λ (h : A → B), h a) (funext q)); apply Id.reflRight; transitivity; symmetry; apply mapFunctoriality (λ (h : A → B), h a); - transitivity; apply Id.map; apply Id.invComp; reflexivity + transitivity; apply ap; apply Id.invComp; reflexivity end end Theorems @@ -749,7 +749,7 @@ namespace hcommSquare hott def induced (η : hcommSquare P A B C) (X : Type r) : (X → P) → @pullback (X → A) (X → B) (X → C) (λ f, right η ∘ f) (λ g, bot η ∘ g) := - λ φ, ⟨(top η ∘ φ, left η ∘ φ), @map (P → C) (X → C) (right η ∘ top η) (bot η ∘ left η) (· ∘ φ) η.naturality⟩ + λ φ, ⟨(top η ∘ φ, left η ∘ φ), @ap (P → C) (X → C) (right η ∘ top η) (bot η ∘ left η) (· ∘ φ) η.naturality⟩ hott def isPullback (η : hcommSquare P A B C) := Π (X : Type (max u v w k)), biinv (induced η X) diff --git a/GroundZero/Theorems/Classical.lean b/GroundZero/Theorems/Classical.lean index e99fdba..7874f1f 100644 --- a/GroundZero/Theorems/Classical.lean +++ b/GroundZero/Theorems/Classical.lean @@ -1,6 +1,7 @@ import GroundZero.Theorems.Equiv + open GroundZero.Types.Equiv (transport) -open GroundZero.Types.Id (map) +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types @@ -67,7 +68,7 @@ section case inl s' => { right; intro z; apply ffNeqTt; transitivity; exact s'⁻¹; symmetry; transitivity; exact r'⁻¹; - apply map; fapply Types.Sigma.prod; apply Theorems.funext; + apply ap; fapply Types.Sigma.prod; apply Theorems.funext; intro x; apply Theorems.Equiv.propset.Id; apply GroundZero.ua.propext; apply HITs.Merely.uniq; apply HITs.Merely.uniq; apply Prod.mk <;> intro <;> apply HITs.Merely.elem <;> right <;> exact z; apply HITs.Merely.uniq }; @@ -114,4 +115,4 @@ section end end Theorems.Classical -end GroundZero \ No newline at end of file +end GroundZero diff --git a/GroundZero/Theorems/Equiv.lean b/GroundZero/Theorems/Equiv.lean index 049a363..dd384d2 100644 --- a/GroundZero/Theorems/Equiv.lean +++ b/GroundZero/Theorems/Equiv.lean @@ -2,6 +2,7 @@ import GroundZero.HITs.Interval import GroundZero.Theorems.UA import GroundZero.HITs.Merely +open GroundZero.Types.Id (ap) open GroundZero.HITs.Interval open GroundZero.Proto (idfun) open GroundZero.Types.Equiv @@ -24,28 +25,28 @@ hott def 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 Id.map g; exact HITs.Merely.uniq (f b) (f a) + apply ap g; exact HITs.Merely.uniq (f b) (f a) end hott def mapToHapply {A : Type u} {B : A → Type v} (c : A) (f g : Π x, B x) (p : f = g) : - Id.map (λ (f : Π x, B x), f c) p = happly p c := + ap (λ (f : Π x, B x), f c) p = happly p c := begin induction p; reflexivity end hott def mapToHapply₂ {A : Type u} {B : A → Type v} {C : Π x, B x → Type w} (c₁ : A) (c₂ : B c₁) (f g : Π (x : A) (y : B x), C x y) (p : f = g) : - Id.map (λ f, f c₁ c₂) p = happly (happly p c₁) c₂ := + ap (λ f, f c₁ c₂) p = happly (happly p c₁) c₂ := begin induction p; reflexivity end hott def mapToHapply₃ {A : Type u} {B : A → Type v} {C : Π x, B x → Type w} {D : Π x y, C x y → Type w'} (c₁ : A) (c₂ : B c₁) (c₃ : C c₁ c₂) (f g : Π x y z, D x y z) (p : f = g) : - Id.map (λ f, f c₁ c₂ c₃) p = happly (happly (happly p c₁) c₂) c₃ := + ap (λ f, f c₁ c₂ c₃) p = happly (happly (happly p c₁) c₂) c₃ := begin induction p; reflexivity end hott def mapToHapply₄ {A : Type u} {B : A → Type v} {C : Π x, B x → Type w} {D : Π (x : A) (y : B x), C x y → Type w'} {E : Π (x : A) (y : B x) (z : C x y), D x y z → Type w''} (c₁ : A) (c₂ : B c₁) (c₃ : C c₁ c₂) (c₄ : D c₁ c₂ c₃) (f g : Π x y z w, E x y z w) (p : f = g) : - Id.map (λ f, f c₁ c₂ c₃ c₄) p = happly (happly (happly (happly p c₁) c₂) c₃) c₄ := + ap (λ f, f c₁ c₂ c₃ c₄) p = happly (happly (happly (happly p c₁) c₂) c₃) c₄ := begin induction p; reflexivity end hott def happlyFunextPt {A : Type u} {B : A → Type v} {f g : Π x, B x} (H : f ~ g) (x : A) : happly (funext H) x = H x := @@ -54,33 +55,33 @@ begin apply happly; apply happlyFunext end hott def happlyFunextPt₂ {A : Type u} {B : A → Type v} {C : Π x, B x → Type w} {f g : Π x y, C x y} (H : Π x y, f x y = g x y) (c₁ : A) (c₂ : B c₁) : happly (happly (funext (λ x, funext (H x))) c₁) c₂ = H c₁ c₂ := -begin transitivity; apply Id.map (happly · c₂); apply happlyFunextPt; apply happlyFunextPt end +begin transitivity; apply ap (happly · c₂); apply happlyFunextPt; apply happlyFunextPt end hott def happlyFunextPt₃ {A : Type u} {B : A → Type v} {C : Π x, B x → Type w} {D : Π x y, C x y → Type w'} {f g : Π x y z, D x y z} (H : Π x y z, f x y z = g x y z) (c₁ : A) (c₂ : B c₁) (c₃ : C c₁ c₂) : happly (happly (happly (funext (λ x, funext (λ y, funext (H x y)))) c₁) c₂) c₃ = H c₁ c₂ c₃ := -begin transitivity; apply Id.map (happly · c₃); apply happlyFunextPt₂; apply happlyFunextPt end +begin transitivity; apply ap (happly · c₃); apply happlyFunextPt₂; apply happlyFunextPt end hott def happlyFunextPt₄ {A : Type u} {B : A → Type v} {C : Π x, B x → Type w} {D : Π x y, C x y → Type w'} {E : Π x y z, D x y z → Type w''} {f g : Π x y z w, E x y z w} (H : Π x y z w, f x y z w = g x y z w) (c₁ : A) (c₂ : B c₁) (c₃ : C c₁ c₂) (c₄ : D c₁ c₂ c₃) : happly (happly (happly (happly (funext (λ x, funext (λ y, funext (λ z, funext (H x y z))))) c₁) c₂) c₃) c₄ = H c₁ c₂ c₃ c₄ := -begin transitivity; apply Id.map (happly · c₄); apply happlyFunextPt₃; apply happlyFunextPt end +begin transitivity; apply ap (happly · c₄); apply happlyFunextPt₃; apply happlyFunextPt end hott def happlyRevPt {A : Type u} {B : A → Type v} {f g : Π x, B x} (p : f = g) (x : A) : happly p⁻¹ x = Homotopy.symm f g (happly p) x := begin apply happly; apply HITs.Interval.happlyRev end -hott def hmtpyRewrite {A : Type u} (f : A → A) (H : f ~ id) (x : A) : H (f x) = Id.map f (H x) := +hott def 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 := begin - intro ⟨g, ⟨ε, η⟩⟩; let ε' := λ b, (ε (f (g b)))⁻¹ ⬝ (Id.map f (η (g b)) ⬝ ε b); + intro ⟨g, ⟨ε, η⟩⟩; let ε' := λ b, (ε (f (g b)))⁻¹ ⬝ (ap f (η (g b)) ⬝ ε b); existsi g; existsi η; existsi ε'; intro x; symmetry; transitivity; - { apply Id.map (λ p, _ ⬝ (Id.map f p ⬝ _)); apply hmtpyRewrite (g ∘ f) }; - apply rewriteComp; transitivity; apply Id.map (· ⬝ _); symmetry; apply mapOverComp (g ∘ f); + { apply ap (λ p, _ ⬝ (ap f p ⬝ _)); apply hmtpyRewrite (g ∘ f) }; + apply rewriteComp; transitivity; apply ap (· ⬝ _); symmetry; apply mapOverComp (g ∘ f); symmetry; apply @homotopySquare A B (f ∘ g ∘ f) f (λ x, ε (f x)) (g (f x)) x (η x) end @@ -92,23 +93,23 @@ begin 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), Id.map f γ ⬝ q = p) → @Id (fib f y) ⟨a, p⟩ ⟨b, q⟩ := + (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 Id.map (· ⬝ p); apply Id.mapInv; apply rewriteComp; exact r⁻¹ + transitivity; apply ap (· ⬝ p); apply Id.mapInv; apply rewriteComp; exact r⁻¹ end hott def 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; - existsi (Id.map g p)⁻¹ ⬝ η x; transitivity; - apply Id.map (· ⬝ p); apply mapFunctoriality; - transitivity; apply Id.map (_ ⬝ · ⬝ p); apply τ; + existsi (ap g p)⁻¹ ⬝ η x; transitivity; + apply ap (· ⬝ p); apply mapFunctoriality; + transitivity; apply ap (_ ⬝ · ⬝ p); apply τ; transitivity; symmetry; apply Id.assoc; transitivity; - { apply Id.map (· ⬝ _); transitivity; apply Id.mapInv; - apply Id.map; symmetry; apply mapOverComp }; - apply rewriteComp; transitivity; apply Id.map (_ ⬝ ·); + { apply ap (· ⬝ _); transitivity; apply Id.mapInv; + apply ap; symmetry; apply mapOverComp }; + apply rewriteComp; transitivity; apply ap (_ ⬝ ·); symmetry; apply idmap; apply homotopySquare end @@ -126,7 +127,7 @@ hott def compQinv₂ {A : Type u} {B : Type v} {C : Type w} begin existsi (· ∘ g) <;> apply Prod.mk <;> intro G <;> apply Theorems.funext <;> intro <;> - apply Id.map G; apply H.2; apply H.1 + apply ap G; apply H.2; apply H.1 end hott def linvContr {A : Type u} {B : Type v} @@ -196,7 +197,7 @@ begin existsi contrToType H; apply Prod.mk <;> existsi @typeToContr A B H <;> intro x; { fapply Sigma.prod; apply H.2; apply transportBackAndForward }; - { transitivity; apply Id.map (subst · x); + { transitivity; apply ap (subst · x); apply propIsSet (contrImplProp H) _ _ _ (idp _); reflexivity } end @@ -246,9 +247,9 @@ begin -- TODO: apply “or” here somehow { apply Proto.Empty.elim; apply ffNeqTt; apply eqvInj ⟨φ, H⟩; exact p₁ ⬝ q₁⁻¹ }; - { transitivity; apply Id.map (bool.encode · x); apply p₂; + { transitivity; apply ap (bool.encode · x); apply p₂; symmetry; induction x using Bool.casesOn <;> assumption }; - { transitivity; apply Id.map (bool.encode · x); apply p₁; + { transitivity; apply ap (bool.encode · x); apply p₁; symmetry; induction x using Bool.casesOn <;> assumption }; { apply Proto.Empty.elim; apply ffNeqTt; apply eqvInj ⟨φ, H⟩; exact p₂ ⬝ q₂⁻¹ } } @@ -274,8 +275,8 @@ hott def 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; - { intro b; apply Id.map Sigma.fst ((w.2.1 (w.2.2 b).1.1).2 ⟨b, (w.2.2 b).1.2⟩) }; - { intro a; apply Id.map Sigma.fst ((w.2.2 (w.2.1 a).1.1).2 ⟨a, (w.2.1 a).1.2⟩) } + { intro b; apply ap Sigma.fst ((w.2.1 (w.2.2 b).1.1).2 ⟨b, (w.2.2 b).1.2⟩) }; + { intro a; apply ap Sigma.fst ((w.2.2 (w.2.1 a).1.1).2 ⟨a, (w.2.1 a).1.2⟩) } end section @@ -300,8 +301,8 @@ section begin fapply Sigma.mk; { intro p; apply transport (R x) p; apply ρ }; fapply Qinv.toBiinv; fapply Sigma.mk; intro r; exact (H x (φ x) (ρ x))⁻¹ ⬝ H x y r; apply Prod.mk; - { intro r; dsimp; transitivity; apply Id.map; symmetry; apply c x (φ x) (ρ x); - transitivity; apply substComp; transitivity; apply Id.map (subst (H x y r)); + { intro r; dsimp; transitivity; apply ap; symmetry; apply c x (φ x) (ρ x); + transitivity; apply substComp; transitivity; apply ap (subst (H x y r)); apply transportForwardAndBack; apply c }; { intro p; induction p; apply Id.invComp } end @@ -312,7 +313,7 @@ section apply Theorems.funext; intro x; apply Theorems.funext; intro y; change (y = (w.2.1 x).1.1) = (w.1 x y); apply ua; apply Equiv.trans; apply inveqv; fapply corrLem w.1 (λ x, (w.2.1 x).1.1) (λ x, (w.2.1 x).1.2) - (λ x y ρ, Id.map Sigma.fst ((w.2.1 x).2 ⟨y, ρ⟩)); + (λ x y ρ, ap Sigma.fst ((w.2.1 x).2 ⟨y, ρ⟩)); { intros x y ρ; change _ = _; transitivity; symmetry; apply transportComp (w.1 x) Sigma.fst ((w.2.1 x).2 ⟨y, ρ⟩); apply apd Sigma.snd }; @@ -345,19 +346,19 @@ begin induction η; apply Theorems.funext (λ w, (ω.2.2 x w)⁻¹) }; transitivity; apply transportOverProduct; apply Product.prod; transitivity; apply transportOverContrMap; - { transitivity; apply Id.map (· ⬝ _); - transitivity; apply Id.mapInv; apply Id.map Id.inv; + { transitivity; apply ap (· ⬝ _); + transitivity; apply Id.mapInv; apply ap Id.inv; transitivity; apply mapToHapply₄; - transitivity; apply Id.map (happly · _); + transitivity; apply ap (happly · _); apply happlyFunextPt₃; apply happlyFunextPt; apply Id.invCompCancel }; { transitivity; apply transportOverPi; apply Theorems.funext; intro; transitivity; apply transportOverPi; apply Theorems.funext; intro; transitivity; apply transportOverContrMap; transitivity; apply Id.reflRight; transitivity; apply Id.mapInv; - transitivity; apply Id.map Id.inv; + transitivity; apply ap Id.inv; transitivity; apply mapToHapply₄; - transitivity; apply Id.map (happly · _); + transitivity; apply ap (happly · _); apply happlyFunextPt₃; apply happlyFunextPt; apply Id.invInv } }; { induction p; reflexivity } end diff --git a/GroundZero/Theorems/Functions.lean b/GroundZero/Theorems/Functions.lean index c0ced81..e19b49e 100644 --- a/GroundZero/Theorems/Functions.lean +++ b/GroundZero/Theorems/Functions.lean @@ -1,6 +1,7 @@ import GroundZero.HITs.Merely open GroundZero.Types GroundZero.HITs +open GroundZero.Types.Id (ap) open GroundZero.Structures namespace GroundZero.Theorems.Functions @@ -25,7 +26,7 @@ hott def 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 := -λ x, ⟨f x, Merely.elem ⟨x, Id.refl⟩⟩ +λ x, ⟨f x, Merely.elem ⟨x, idp (f x)⟩⟩ hott def cutIsSurj {A : Type u} {B : Type v} (f : A → B) : surjective (cut f) := begin @@ -53,7 +54,7 @@ end hott def ranConst {A : Type u} (a : A) {B : Type v} (b : B) : Ran (Function.const A b) := -⟨b, Merely.elem ⟨a, Id.refl⟩⟩ +⟨b, Merely.elem ⟨a, idp b⟩⟩ hott def ranConstEqv {A : Type u} (a : A) {B : Type v} (H : hset B) (b : B) : Ran (Function.const A b) ≃ 𝟏 := @@ -66,7 +67,7 @@ begin end hott def isEmbedding {A : Type u} {B : Type v} (f : A → B) := -Π x y, @Equiv.biinv (x = y) (f x = f y) (Id.map f) +Π x y, @Equiv.biinv (x = y) (f x = f y) (ap f) hott def Embedding (A : Type u) (B : Type v) := Σ (f : A → B), isEmbedding f @@ -78,19 +79,19 @@ section def Embedding.ap : A → B := f.1 def Embedding.eqv (x y : A) : (x = y) ≃ (f.ap x = f.ap y) := - ⟨Id.map f.ap, f.2 x y⟩ + ⟨Id.ap f.ap, f.2 x y⟩ end hott def 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 Id.map f.1; apply f.2; apply H + existsi ap f.1; apply f.2; apply H end hott def eqvMapForward {A : Type u} {B : Type v} (e : A ≃ B) (x y : A) (p : e x = e y) : x = y := -(e.leftForward x)⁻¹ ⬝ (@Id.map B A _ _ e.left p) ⬝ (e.leftForward y) +(e.leftForward x)⁻¹ ⬝ (@ap B A _ _ e.left p) ⬝ (e.leftForward y) hott def sigmaPropEq {A : Type u} {B : A → Type v} (H : Π x, prop (B x)) {x y : Sigma B} (p : x.1 = y.1) : x = y := @@ -117,4 +118,4 @@ end hott def isConnected (A : Type u) := Σ (x : A), Π y, ∥x = y∥ -end GroundZero.Theorems.Functions \ No newline at end of file +end GroundZero.Theorems.Functions diff --git a/GroundZero/Theorems/Funext.lean b/GroundZero/Theorems/Funext.lean index 2c1b961..68c93c1 100644 --- a/GroundZero/Theorems/Funext.lean +++ b/GroundZero/Theorems/Funext.lean @@ -1,4 +1,6 @@ import GroundZero.Types.HEq + +open GroundZero.Types.Id (ap) open GroundZero.Types /- @@ -54,7 +56,7 @@ namespace Interval (s : b₀ =[seg] b₁) : Equiv.apd (ind b₀ b₁ s) seg = s noncomputable hott def recβrule {B : Type u} (b₀ b₁ : B) - (s : b₀ = b₁) : Id.map (rec b₀ b₁ s) seg = s := + (s : b₀ = b₁) : ap (rec b₀ b₁ s) seg = s := begin apply Equiv.pathoverOfEqInj seg; transitivity; symmetry; apply Equiv.apdOverConstantFamily; apply indβrule @@ -66,7 +68,7 @@ namespace Interval hott def funext {A : Type u} {B : A → Type v} {f g : Π x, B x} (p : f ~ g) : f = g := - @Id.map I (Π x, B x) 0 1 (λ i x, homotopy p x i) seg + @ap I (Π x, B x) 0 1 (λ i x, homotopy p x i) seg hott def happly {A : Type u} {B : A → Type v} {f g : Π x, B x} (p : f = g) : f ~ g := @@ -77,8 +79,8 @@ namespace Interval begin induction p; reflexivity end hott def mapHapply {A : Type u} {B : Type v} {C : Type w} {a b : A} {c : B} - (f : A → B → C) (p : a = b) : Id.map (f · c) p = happly (Id.map f p) c := + (f : A → B → C) (p : a = b) : ap (f · c) p = happly (ap f p) c := begin induction p; reflexivity end end Interval -end GroundZero.HITs \ No newline at end of file +end GroundZero.HITs diff --git a/GroundZero/Theorems/Hopf.lean b/GroundZero/Theorems/Hopf.lean index 899ed98..de51158 100644 --- a/GroundZero/Theorems/Hopf.lean +++ b/GroundZero/Theorems/Hopf.lean @@ -3,44 +3,78 @@ import GroundZero.HITs.Circle open GroundZero GroundZero.HITs GroundZero.Types.Equiv open GroundZero.Structures GroundZero.Types +open GroundZero.Types.Id (ap) +open GroundZero.Proto (idfun) namespace GroundZero.Theorems.Hopf namespace Real + open HITs.Circle + -- Real (S⁰ ↪ S¹ ↠ S¹) def family : S¹ → Type := Circle.rec S⁰ (ua ua.negBoolEquiv) def total : Type := Σ x, family x - def inj (x : S⁰) : total := ⟨Circle.base, x⟩ + def inj (x : S⁰) : total := ⟨base, x⟩ def map : total → S¹ := Sigma.fst - def μ₁ : total := ⟨Circle.base, false⟩ - def μ₂ : total := ⟨Circle.base, true⟩ + hott def μ₁ : total := ⟨base, false⟩ + hott def μ₂ : total := ⟨base, true⟩ + + abbrev μ := μ₁ + + noncomputable hott def μLoop : μ = μ := + Sigma.prod (loop ⬝ loop) (Circle.Ωrecβ₂ false not not ua.negNeg ua.negNeg loop ⬝ + ap not (Circle.Ωrecβ₂ false not not ua.negNeg ua.negNeg (idp base))) - noncomputable hott def family.transport₁ : transport family Circle.loop ~ not := + noncomputable hott def llinv' : map ∘ rec μ μLoop ~ rec base (loop ⬝ loop) := + begin + fapply ind; exact idp base; apply Id.trans; apply Equiv.transportOverHmtpy; + transitivity; apply ap (· ⬝ _ ⬝ _); transitivity; apply Id.mapInv; apply ap; + transitivity; apply Equiv.mapOverComp; transitivity; apply ap; apply recβrule₂; + apply Sigma.mapFstOverProd; transitivity; symmetry; apply Id.assoc; + apply Id.compReflIfEq; symmetry; apply recβrule₂ + end + + noncomputable hott def family.transport₁ : transport family loop ~ not := begin intro b; transitivity; apply transportToTransportconst; - transitivity; apply Id.map (transportconst · b); - apply Circle.recβrule₂; apply ua.transportRule + transitivity; apply ap (transportconst · b); + apply recβrule₂; apply ua.transportRule end - noncomputable hott def family.transport₂ : transport family Circle.loop⁻¹ ~ not := + noncomputable hott def family.transport₂ : transport family loop⁻¹ ~ not := begin intro b; transitivity; apply transportToTransportconst; - transitivity; apply Id.map (transportconst · b); - transitivity; apply Id.mapInv; apply Id.map; apply Circle.recβrule₂; + transitivity; apply ap (transportconst · b); + transitivity; apply Id.mapInv; apply ap; apply recβrule₂; transitivity; apply transportconstOverInv; apply ua.transportInvRule end noncomputable hott def ρ₁ : μ₁ = μ₂ := - Sigma.prod Circle.loop (family.transport₁ false) + Sigma.prod loop (family.transport₁ false) noncomputable hott def ρ₂ : μ₁ = μ₂ := - Sigma.prod Circle.loop⁻¹ (family.transport₂ false) + Sigma.prod loop⁻¹ (family.transport₂ false) noncomputable hott def ret : S¹ → total := Suspension.rec μ₁ μ₂ (λ | false => ρ₁ | true => ρ₂) + + noncomputable hott def linv : map ∘ ret ~ idfun := + begin + fapply Suspension.ind; reflexivity; apply Suspension.merid true; + intro (b : 𝟐); apply Id.trans; apply Equiv.transportOverHmtpy; + transitivity; apply ap (· ⬝ _); transitivity; apply Id.reflRight; + transitivity; apply Id.mapInv; apply ap; transitivity; apply Equiv.mapOverComp; + apply ap (ap map); apply Suspension.recβrule; induction b; + { transitivity; apply ap (· ⬝ _); transitivity; apply ap; apply Sigma.mapFstOverProd; + apply Id.explodeInv; transitivity; apply ap (_ ⬝ ·); apply Equiv.idmap; + transitivity; apply Id.cancelInvComp; apply Id.invInv }; + { transitivity; apply ap (· ⬝ _); transitivity; apply ap; apply Sigma.mapFstOverProd; + apply Id.invInv; transitivity; apply ap (_ ⬝ ·); apply Equiv.idmap; + apply Id.cancelInvComp } + end end Real namespace Complex @@ -48,4 +82,4 @@ namespace Complex hott def family : S² → Type := Suspension.rec S¹ S¹ (ua ∘ Circle.μₑ) end Complex -end GroundZero.Theorems.Hopf \ No newline at end of file +end GroundZero.Theorems.Hopf diff --git a/GroundZero/Theorems/Nat.lean b/GroundZero/Theorems/Nat.lean index 035546f..88c294f 100644 --- a/GroundZero/Theorems/Nat.lean +++ b/GroundZero/Theorems/Nat.lean @@ -1,6 +1,7 @@ import GroundZero.Theorems.UA import GroundZero.Types.Nat +open GroundZero.Types.Id (ap) open GroundZero.Proto (idfun) open GroundZero.Types.Equiv open GroundZero.Structures @@ -29,26 +30,26 @@ namespace Nat | Nat.zero, Nat.succ n => Sum.inr (ua.succNeqZero ∘ Id.inv) | Nat.succ m, Nat.succ n => match natDecEq m n with - | Sum.inl p => Sum.inl (Id.map Nat.succ p) + | Sum.inl p => Sum.inl (ap Nat.succ p) | Sum.inr φ => Sum.inr (φ ∘ succInj) hott def natIsSet : hset ℕ := Hedberg natDecEq hott def zeroPlus : Π (i : ℕ), 0 + i = i | Nat.zero => idp 0 - | Nat.succ i => Id.map Nat.succ (zeroPlus i) + | Nat.succ i => ap Nat.succ (zeroPlus i) hott def succPlus (i : ℕ) : Π j, Nat.succ i + j = Nat.succ (i + j) | Nat.zero => idp _ - | Nat.succ j => Id.map Nat.succ (succPlus i j) + | Nat.succ j => ap Nat.succ (succPlus i j) hott def comm : Π (i j : ℕ), i + j = j + i | Nat.zero, j => zeroPlus j - | Nat.succ i, j => succPlus i j ⬝ Id.map Nat.succ (comm i j) + | Nat.succ i, j => succPlus i j ⬝ ap Nat.succ (comm i j) hott def assoc (i j : ℕ) : Π k, (i + j) + k = i + (j + k) | Nat.zero => idp (i + j) - | Nat.succ k => Id.map Nat.succ (assoc i j k) + | Nat.succ k => ap Nat.succ (assoc i j k) hott def zeroMul : Π (i : ℕ), 0 * i = 0 | Nat.zero => idp 0 @@ -56,18 +57,18 @@ namespace Nat hott def oneMul : Π (i : ℕ), 1 * i = i | Nat.zero => idp 0 - | Nat.succ i => Id.map Nat.succ (oneMul i) + | Nat.succ i => ap Nat.succ (oneMul i) hott def mulOne (i : ℕ) : i * 1 = i := zeroPlus i hott def distribLeft (i : ℕ) : Π (j n : ℕ), n * (i + j) = n * i + n * j | Nat.zero, n => idp _ - | Nat.succ j, n => Id.map (λ m, m + n) (distribLeft i j n) ⬝ assoc _ _ _ + | Nat.succ j, n => ap (λ m, m + n) (distribLeft i j n) ⬝ assoc _ _ _ hott def mulSucc (i : ℕ) : Π j, Nat.succ i * j = i * j + j | Nat.zero => idp _ - | Nat.succ j => Id.map Nat.succ (Id.map (λ k, k + i) (mulSucc i j) ⬝ assoc _ _ _ - ⬝ (assoc _ _ _ ⬝ Id.map _ (comm _ _))⁻¹) + | Nat.succ j => ap Nat.succ (ap (λ k, k + i) (mulSucc i j) ⬝ assoc _ _ _ + ⬝ (assoc _ _ _ ⬝ ap _ (comm _ _))⁻¹) hott def mulComm (i : ℕ) : Π j, i * j = j * i | Nat.zero => (zeroMul _)⁻¹ @@ -80,23 +81,23 @@ namespace Nat mulComm (i + j) n ⬝ distribLeft _ _ _ ⬝ bimap Nat.add (mulComm _ _) (mulComm _ _) hott def oneNeqNPlusTwo (n : ℕ) : ¬(1 = n + 2) := - λ p, ua.succNeqZero (Id.map Nat.pred p)⁻¹ + λ p, ua.succNeqZero (ap Nat.pred p)⁻¹ def isEven (n : ℕ) := Σ m, n = m * 2 def isOdd (n : ℕ) := Σ m, n = m * 2 + 1 hott def plusOnePlus {i j : ℕ} : i + 1 + j = (i + j) + 1 := calc i + 1 + j = i + (1 + j) : assoc _ _ _ - ... = i + (j + 1) : Id.map (Nat.add i) (comm 1 j) + ... = i + (j + 1) : ap (Nat.add i) (comm 1 j) ... = (i + j) + 1 : idp _ hott def assocTetra {i j k l : ℕ} : i + (j + k) + l = (i + j) + (k + l) := calc (i + (j + k)) + l = i + ((j + k) + l) : assoc _ _ _ - ... = i + (j + (k + l)) : Id.map _ (assoc _ _ _) + ... = i + (j + (k + l)) : ap _ (assoc _ _ _) ... = (i + j) + (k + l) : (assoc _ _ _)⁻¹ hott def plusDiag (n : ℕ) : n * 2 = n + n := - Id.map (λ m, m + n) (zeroPlus _) + ap (λ m, m + n) (zeroPlus _) hott def apart : ℕ → ℕ → Type | Nat.zero, Nat.zero => 𝟎 @@ -114,7 +115,7 @@ namespace Nat | Nat.zero, Nat.zero => idp _ | Nat.succ m, Nat.zero => idp _ | Nat.zero, Nat.succ n => idp _ - | Nat.succ m, Nat.succ n => Id.map Nat.succ (comm _ _) + | Nat.succ m, Nat.succ n => ap Nat.succ (comm _ _) hott def min : ℕ → ℕ → ℕ | Nat.zero, Nat.zero => 0 @@ -126,15 +127,15 @@ namespace Nat | Nat.zero, Nat.zero => idp _ | Nat.succ m, Nat.zero => idp _ | Nat.zero, Nat.succ n => idp _ - | Nat.succ m, Nat.succ n => Id.map Nat.succ (comm _ _) + | Nat.succ m, Nat.succ n => ap Nat.succ (comm _ _) hott def max.refl : Π n, max n n = n | Nat.zero => idp 0 - | Nat.succ n => Id.map Nat.succ (refl n) + | Nat.succ n => ap Nat.succ (refl n) hott def min.refl : Π n, min n n = n | Nat.zero => idp 0 - | Nat.succ n => Id.map Nat.succ (refl n) + | Nat.succ n => ap Nat.succ (refl n) def le (n m : ℕ) := max n m = m infix:55 (priority := high) " ≤ " => le @@ -170,7 +171,7 @@ namespace Nat | Nat.succ n, Nat.zero, Nat.zero => idp _ | Nat.succ n, Nat.zero, Nat.succ k => idp _ | Nat.succ n, Nat.succ m, Nat.zero => idp _ - | Nat.succ n, Nat.succ m, Nat.succ k => Id.map Nat.succ (assoc _ _ _) + | Nat.succ n, Nat.succ m, Nat.succ k => ap Nat.succ (assoc _ _ _) hott def min.assoc : Π n m k, min n (min m k) = min (min n m) k | Nat.zero, Nat.zero, Nat.zero => idp _ @@ -180,19 +181,19 @@ namespace Nat | Nat.succ n, Nat.zero, Nat.zero => idp _ | Nat.succ n, Nat.zero, Nat.succ k => idp _ | Nat.succ n, Nat.succ m, Nat.zero => idp _ - | Nat.succ n, Nat.succ m, Nat.succ k => Id.map Nat.succ (assoc _ _ _) + | Nat.succ n, Nat.succ m, Nat.succ k => ap Nat.succ (assoc _ _ _) hott def le.trans {n m k : ℕ} : n ≤ m → m ≤ k → n ≤ k := begin intros p q; change _ = _; transitivity; - apply Id.map; exact q⁻¹; transitivity; apply max.assoc; - transitivity; apply Id.map (max · k); exact p; exact q + apply ap; exact q⁻¹; transitivity; apply max.assoc; + transitivity; apply ap (max · k); exact p; exact q end instance : Transitive le := ⟨@le.trans⟩ - hott def le.inj (n m : ℕ) : n + 1 ≤ m + 1 → n ≤ m := Id.map Nat.pred - hott def le.map (n m : ℕ) : n ≤ m → n + 1 ≤ m + 1 := Id.map Nat.succ + hott def le.inj (n m : ℕ) : n + 1 ≤ m + 1 → n ≤ m := ap Nat.pred + hott def le.map (n m : ℕ) : n ≤ m → n + 1 ≤ m + 1 := ap Nat.succ hott def le.addr (n m : ℕ) : Π k, n ≤ m → n + k ≤ m + k | Nat.zero, h => h @@ -203,7 +204,7 @@ namespace Nat hott def le.succ : Π (n : ℕ), n ≤ n + 1 | Nat.zero => idp _ - | Nat.succ n => Id.map Nat.succ (succ n) + | Nat.succ n => ap Nat.succ (succ n) hott def le.step : Π (n m : ℕ), n ≤ m → n ≤ m + 1 | Nat.zero, m, _ => idp _ @@ -213,12 +214,12 @@ namespace Nat | Nat.zero, Nat.zero, p => idp _ | Nat.succ m, Nat.zero, p => Proto.Empty.elim (max.neZero p) | Nat.zero, Nat.succ n, p => idp _ - | Nat.succ m, Nat.succ n, p => Id.map Nat.succ (minMax m n (Id.map Nat.pred p)) + | Nat.succ m, Nat.succ n, p => ap Nat.succ (minMax m n (ap Nat.pred p)) hott def le.max (n m : ℕ) : n ≤ max n m := begin change _ = _; transitivity; apply max.assoc; - apply Id.map (Nat.max · m); apply max.refl + apply ap (Nat.max · m); apply max.refl end hott def le.maxRev (n m : ℕ) : n ≤ Nat.max m n := @@ -228,7 +229,7 @@ namespace Nat | Nat.zero, Nat.zero => idp _ | Nat.succ n, Nat.zero => idp _ | Nat.zero, Nat.succ m => idp _ - | Nat.succ n, Nat.succ m => Id.map Nat.succ (min n m) + | Nat.succ n, Nat.succ m => ap Nat.succ (min n m) hott def le.minRev (n m : ℕ) : Nat.min m n ≤ m := @transport ℕ (· ≤ m) (Nat.min n m) (Nat.min m n) (min.comm n m) (le.min n m) @@ -238,9 +239,9 @@ namespace Nat hott def le.dec : Π (m n : ℕ), (m ≤ n) + (n + 1 ≤ m) | Nat.zero, Nat.zero => Sum.inl (idp _) - | Nat.succ m, Nat.zero => Sum.inr (Id.map Nat.succ (max.zeroLeft m)) + | Nat.succ m, Nat.zero => Sum.inr (ap Nat.succ (max.zeroLeft m)) | Nat.zero, Nat.succ n => Sum.inl (idp _) - | Nat.succ m, Nat.succ n => Coproduct.elim (Sum.inl ∘ Id.map Nat.succ) (Sum.inr ∘ Id.map Nat.succ) (dec m n) + | Nat.succ m, Nat.succ n => Coproduct.elim (Sum.inl ∘ ap Nat.succ) (Sum.inr ∘ ap Nat.succ) (dec m n) hott def le.neSucc : Π (n : ℕ), ¬(n + 1 ≤ n) | Nat.zero => max.neZero @@ -256,7 +257,7 @@ namespace Nat hott def le.leSucc : Π (n : ℕ), n ≤ n + 1 | Nat.zero => idp _ - | Nat.succ n => Id.map Nat.succ (leSucc n) + | Nat.succ n => ap Nat.succ (leSucc n) hott def le.elim (ρ : ℕ → ℕ → Type u) (τ : Π n m k, ρ n m → ρ m k → ρ n k) (reflρ : Π n, ρ n n) (succρ : Π n, ρ n (n + 1)) {n : ℕ} : Π {m : ℕ}, n ≤ m → ρ n m @@ -280,7 +281,7 @@ namespace Nat | Nat.zero, Nat.zero, _ => idp 0 | Nat.succ m, Nat.zero, p => p | Nat.zero, Nat.succ n, p => p⁻¹ - | Nat.succ m, Nat.succ n, p => Id.map Nat.succ (identity m n p) + | Nat.succ m, Nat.succ n, p => ap Nat.succ (identity m n p) hott def dist.symm : Π (n m : ℕ), dist n m = dist m n | Nat.zero, Nat.zero => idp _ @@ -307,9 +308,9 @@ namespace Nat | Nat.succ n, Nat.succ m => le.trans (le.map (max n m) (n + m) (leAdd n m)) (begin apply transport (n + m + 1 ≤ ·); symmetry; transitivity; - apply Nat.assoc n 1; transitivity; transitivity; apply Id.map; + apply Nat.assoc n 1; transitivity; transitivity; apply ap; symmetry; apply Nat.assoc 1 m 1; symmetry; apply Nat.assoc; - apply Id.map (λ k, n + k + 1); apply Nat.comm; apply le.leSucc + apply ap (λ k, n + k + 1); apply Nat.comm; apply le.leSucc end) -- ℕ-specific property @@ -347,11 +348,11 @@ namespace UnitList def decodeEncode : Π n, decode (encode n) = n | Nat.zero => idp _ - | Nat.succ n => Id.map Nat.succ (decodeEncode n) + | Nat.succ n => ap Nat.succ (decodeEncode n) def encodeDecode : Π xs, encode (decode xs) = xs | [] => idp _ - | ★ :: xs => Id.map succ' (encodeDecode xs) + | ★ :: xs => ap succ' (encodeDecode xs) hott def iso : ℕ ≃ List 𝟏 := ⟨encode, (⟨decode, decodeEncode⟩, ⟨decode, encodeDecode⟩)⟩ diff --git a/GroundZero/Theorems/Pullback.lean b/GroundZero/Theorems/Pullback.lean index b3b466c..d9a0914 100644 --- a/GroundZero/Theorems/Pullback.lean +++ b/GroundZero/Theorems/Pullback.lean @@ -1,6 +1,8 @@ import GroundZero.Theorems.Equiv open GroundZero GroundZero.Types open GroundZero.Structures + +open GroundZero.Types.Id (ap) open HITs.Interval (happly) universe u v w k @@ -14,9 +16,9 @@ section 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; - { apply Id.map (Sigma.mk _); apply happly (happlyFunext _ _ _) }; - { apply Id.map (Sigma.mk _); transitivity; - apply Id.map funext; change _ = happly w.2; apply funext; + { apply ap (Sigma.mk _); apply happly (happlyFunext _ _ _) }; + { apply ap (Sigma.mk _); transitivity; + apply ap funext; change _ = happly w.2; apply funext; intro c; induction c; reflexivity; apply funextHapply } end end @@ -32,4 +34,4 @@ section end end -end GroundZero.Theorems \ No newline at end of file +end GroundZero.Theorems diff --git a/GroundZero/Theorems/UA.lean b/GroundZero/Theorems/UA.lean index 8b38be7..51f925b 100644 --- a/GroundZero/Theorems/UA.lean +++ b/GroundZero/Theorems/UA.lean @@ -1,4 +1,6 @@ import GroundZero.Structures + +open GroundZero.Types.Id (ap) open GroundZero.Types.Equiv open GroundZero.Structures open GroundZero.Types @@ -45,7 +47,7 @@ noncomputable hott def transportRule {A B : Type u} (e : A ≃ B) (x : A) : transportconst (ua e) x = e x := begin induction e; transitivity; - apply Id.map (transport id · x); + apply ap (transport id · x); apply reflOnUa; reflexivity end @@ -53,7 +55,7 @@ noncomputable hott def transportInvRule {A B : Type u} (e : A ≃ B) (x : B) : transportconst (ua e)⁻¹ x = e.left x := begin induction e; transitivity; - apply Id.map (transport id ·⁻¹ x); + apply ap (transport id ·⁻¹ x); apply reflOnUa; reflexivity end @@ -64,7 +66,7 @@ hott def idtoeqvAndId {A : Type u} : idtoeqv (idp A) = ideqv A := by reflexivity noncomputable hott def uaβrule {A B : Type u} (e : A ≃ B) : idtoeqv (ua e) = e := -begin induction e; change _ = idtoeqv (idp _); apply Id.map; apply reflOnUa end +begin induction e; change _ = idtoeqv (idp _); apply ap; apply reflOnUa end noncomputable hott def propUniq {A B : Type u} (p : A = B) : ua (idtoeqv p) = p := begin induction p; exact Jβrule end @@ -80,7 +82,7 @@ noncomputable hott def uaTrans {A B γ : Type u} (p : A ≃ B) (q : B ≃ γ) : ua (Equiv.trans p q) = ua p ⬝ ua q := begin induction p; induction q; change ua (ideqv _) = _; symmetry; - change _ = idp _ ⬝ _; apply Id.map (· ⬝ ua _); apply reflOnUa + change _ = idp _ ⬝ _; apply ap (· ⬝ ua _); apply reflOnUa end hott def isZero : ℕ → 𝟐 @@ -88,10 +90,10 @@ hott def isZero : ℕ → 𝟐 | Nat.succ _ => false example (h : 0 = 1) : 𝟎 := -ffNeqTt (Id.map isZero h)⁻¹ +ffNeqTt (ap isZero h)⁻¹ hott def succNeqZero {n : ℕ} : ¬(Nat.succ n = 0) := -λ h, ffNeqTt (Id.map isZero h) +λ h, ffNeqTt (ap isZero h) hott def negNeg : Π x, not (not x) = x | true => idp true @@ -104,7 +106,7 @@ noncomputable hott def universeNotASet : ¬(hset Type) := begin let p : 𝟐 = 𝟐 := ua negBoolEquiv; let h := transportconst p true; let g : h = false := transportRule negBoolEquiv true; - intro ε; let f : h = true := Id.map (transportconst · true) (ε _ _ p (idp 𝟐)); + intro ε; let f : h = true := ap (transportconst · true) (ε _ _ p (idp 𝟐)); apply ffNeqTt; exact g⁻¹ ⬝ f end @@ -160,4 +162,4 @@ section end end ua -end GroundZero \ No newline at end of file +end GroundZero diff --git a/GroundZero/Types/Coproduct.lean b/GroundZero/Types/Coproduct.lean index 3380bd9..c57a450 100644 --- a/GroundZero/Types/Coproduct.lean +++ b/GroundZero/Types/Coproduct.lean @@ -1,5 +1,7 @@ import GroundZero.Types.Equiv +open GroundZero.Types.Id (ap) + namespace GroundZero.Types universe u v w w' @@ -40,7 +42,7 @@ namespace Coproduct Equiv.transport (code a₀) p (idp a₀) hott def decode {a₀ : A} : Π {x : A + B} (c : code a₀ x), inl a₀ = x - | inl a, c => Id.map inl c + | inl a, c => ap inl c | inr b, c => Proto.Empty.elim c hott def decodeEncode {a₀ : A} {x : A + B} @@ -76,7 +78,7 @@ namespace Coproduct hott def decode {b₀ : B} : Π {x : A + B} (c : code b₀ x), inr b₀ = x | inl a, c => Proto.Empty.elim c - | inr b, c => Id.map inr c + | inr b, c => ap inr c hott def decodeEncode {b₀ : B} {x : A + B} (p : inr b₀ = x) : decode (encode p) = p := @@ -108,8 +110,8 @@ namespace Coproduct hott def 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 Id.map; assumption; apply Proto.Empty.elim p; - apply Proto.Empty.elim p; apply Id.map; assumption + apply ap; assumption; apply Proto.Empty.elim p; + apply Proto.Empty.elim p; apply ap; assumption end end Coproduct diff --git a/GroundZero/Types/Equiv.lean b/GroundZero/Types/Equiv.lean index 013f1fb..7c101f7 100644 --- a/GroundZero/Types/Equiv.lean +++ b/GroundZero/Types/Equiv.lean @@ -69,7 +69,7 @@ namespace Equiv hott def homotopySquare {A : Type u} {B : Type v} {f g : A → B} (H : f ~ g) {x y : A} (p : x = y) : - H x ⬝ Id.map g p = Id.map f p ⬝ H y := + H x ⬝ ap g p = ap f p ⬝ H y := begin induction p; transitivity; apply Id.reflRight; apply Id.reflLeft end end Equiv @@ -97,8 +97,8 @@ namespace Equiv hott def biinvTrans {A : Type u} {B : Type v} {C : Type w} {f : A → B} {g : B → C} (e₁ : biinv f) (e₂ : biinv g) : biinv (g ∘ f) := - (⟨e₁.1.1 ∘ e₂.1.1, λ x, Id.map e₁.1.1 (e₂.1.2 (f x)) ⬝ e₁.1.2 x⟩, - ⟨e₁.2.1 ∘ e₂.2.1, λ x, Id.map g (e₁.2.2 (e₂.2.1 x)) ⬝ e₂.2.2 x⟩) + (⟨e₁.1.1 ∘ e₂.1.1, λ x, ap e₁.1.1 (e₂.1.2 (f x)) ⬝ e₁.1.2 x⟩, + ⟨e₁.2.1 ∘ e₂.2.1, λ x, ap g (e₁.2.2 (e₂.2.1 x)) ⬝ e₂.2.2 x⟩) hott def trans {A : Type u} {B : Type v} {C : Type w} (f : A ≃ B) (g : B ≃ C) : A ≃ C := @@ -234,7 +234,7 @@ namespace Equiv hott def depPathMap' {A : Type u} {B : Type v} {C : A → Type w} {D : B → Type k} {a b : A} {p : a = b} {u : C a} {v : C b} (f : A → B) - (g : Π x, C x → D (f x)) (q : u =[p] v) : g a u =[Id.map f p] g b v := + (g : Π x, C x → D (f x)) (q : u =[p] v) : g a u =[ap f p] g b v := begin induction p; induction q using Id.casesOn; apply idp end def transportInv {A : Type u} (B : A → Type v) {a b : A} (p : a = b) : B b → B a := @@ -248,11 +248,11 @@ namespace Equiv hott theorem transportComp {A : Type u} {B : Type v} (C : B → Type w) {x y : A} (f : A → B) (p : x = y) (u : C (f x)) : - transport (C ∘ f) p u = transport C (Id.map f p) u := + transport (C ∘ f) p u = transport C (ap f p) u := begin induction p; reflexivity end hott theorem transportToTransportconst {A : Type u} (B : A → Type v) {a b : A} - (p : a = b) (u : B a) : Equiv.transport B p u = Equiv.transportconst (Id.map B p) u := + (p : a = b) (u : B a) : Equiv.transport B p u = Equiv.transportconst (ap B p) u := begin induction p; reflexivity end hott theorem transportconstOverComposition {A B C : Type u} (p : A = B) (q : B = C) (x : A) : @@ -304,7 +304,7 @@ namespace Equiv begin intro ε; symmetry; apply invCompRewrite; exact ε end hott lemma mapWithHomotopy {A : Type u} {B : Type v} (f g : A → B) (H : f ~ g) {a b : A} (p : a = b) : - Id.map f p = H a ⬝ Id.map g p ⬝ (H b)⁻¹ := + ap f p = H a ⬝ ap g p ⬝ (H b)⁻¹ := begin apply invCompRewrite; symmetry; apply homotopySquare end hott def pathoverFromTrans {A : Type u} {a b c : A} @@ -317,46 +317,46 @@ namespace Equiv hott theorem mapFunctoriality {A : Type u} {B : Type v} {a b c : A} (f : A → B) {p : a = b} {q : b = c} : - Id.map f (p ⬝ q) = Id.map f p ⬝ Id.map f q := + ap f (p ⬝ q) = ap f p ⬝ ap f q := begin induction p; reflexivity end hott lemma transportOverContrMap {A : Type u} {B : Type v} {a b : A} {c : B} (f : A → B) (p : a = b) (q : f a = c) : - Equiv.transport (λ x, f x = c) p q = Id.map f p⁻¹ ⬝ q := + Equiv.transport (λ x, f x = c) p q = ap f p⁻¹ ⬝ q := begin induction p; reflexivity end hott lemma transportOverInvContrMap {A : Type u} {B : Type v} {a b : A} {c : B} (f : A → B) (p : a = b) (q : c = f a) : - Equiv.transport (λ x, c = f x) p q = q ⬝ Id.map f p := + Equiv.transport (λ x, c = f x) p q = q ⬝ ap f p := begin induction p; symmetry; apply Id.reflRight end hott lemma transportOverInvolution {A : Type u} {a b : A} (f : A → A) (p : a = b) (q : f a = a) : - Equiv.transport (λ x, f x = x) p q = Id.map f p⁻¹ ⬝ q ⬝ p := + Equiv.transport (λ x, f x = x) p q = ap f p⁻¹ ⬝ q ⬝ p := begin induction p; symmetry; apply Id.reflRight end hott lemma transportOverHmtpy {A : Type u} {B : Type v} {a b : A} (f g : A → B) (p : a = b) (q : f a = g a) : - Equiv.transport (λ x, f x = g x) p q = Id.map f p⁻¹ ⬝ q ⬝ Id.map g p := + Equiv.transport (λ x, f x = g x) p q = ap f p⁻¹ ⬝ q ⬝ ap g p := begin induction p; symmetry; apply Id.reflRight end - hott lemma idmap {A : Type u} {a b : A} (p : a = b) : Id.map idfun p = p := + hott lemma idmap {A : Type u} {a b : A} (p : a = b) : ap idfun p = p := begin induction p; reflexivity end hott lemma constmap {A : Type u} {B : Type v} {a b : A} {c : B} - (p : a = b) : Id.map (λ _, c) p = idp c := + (p : a = b) : ap (λ _, c) p = idp c := begin induction p; reflexivity end hott theorem transportOverDhmtpy {A : Type u} {B : A → Type v} {a b : A} (f g : Π x, B x) (p : a = b) (q : f a = g a) : - Equiv.transport (λ x, f x = g x) p q = (apd f p)⁻¹ ⬝ Id.map (subst p) q ⬝ apd g p := + Equiv.transport (λ x, f x = g x) p q = (apd f p)⁻¹ ⬝ ap (subst p) q ⬝ apd g p := begin induction p; symmetry; transitivity; apply Id.reflRight; apply idmap end hott theorem mapOverComp {A : Type u} {B : Type v} {C : Type w} {a b : A} (f : A → B) (g : B → C) (p : a = b) : - @Id.map A C a b (g ∘ f) p = Id.map g (Id.map f p) := + @ap A C a b (g ∘ f) p = ap g (ap f p) := begin induction p; reflexivity end hott theorem apdOverConstantFamily {A : Type u} {B : Type v} {a b : A} - (f : A → B) (p : a = b) : apd f p = pathoverOfEq p (Id.map f p) := + (f : A → B) (p : a = b) : apd f p = pathoverOfEq p (ap f p) := begin induction p; reflexivity end def reflPathover {A : Type u} {B : Type v} {a : A} {x y : B} (p : x =[λ _, B, idp a] y) : x = y := p @@ -395,7 +395,7 @@ namespace Equiv hott lemma transportOverFunction {A : Type u} {B : Type v} {a : A} {b : B} (f g : A → B) (p : f = g) (q : f a = b) : transport (λ (f' : A → B), f' a = b) p q = - @Id.map (A → B) B g f (λ (f' : A → B), f' a) p⁻¹ ⬝ q := + @ap (A → B) B g f (λ (f' : A → B), f' a) p⁻¹ ⬝ q := begin induction p; reflexivity end hott lemma transportOverOperation {A B : Type u} (φ : A → A → A) (p : A = B) : @@ -425,22 +425,22 @@ namespace Equiv hott lemma bimapReflLeft {A : Type u} {B : Type v} {C : Type w} {a : A} {a' b' : B} (f : A → B → C) (p : a' = b') : - bimap f (idp a) p = Id.map (f a) p := + bimap f (idp a) p = ap (f a) p := begin induction p; reflexivity end hott lemma bimapReflRight {A : Type u} {B : Type v} {C : Type w} {a b : A} {a' : B} (f : A → B → C) (p : a = b) : - bimap f p (idp a') = Id.map (f · a') p := + bimap f p (idp a') = ap (f · a') p := begin induction p; reflexivity end hott theorem bimapCharacterization {A : Type u} {B : Type v} {C : Type w} {a b : A} {a' b' : B} (f : A → B → C) (p : a = b) (q : a' = b') : - bimap f p q = @Id.map A C a b (f · a') p ⬝ Id.map (f b) q := + bimap f p q = @ap A C a b (f · a') p ⬝ ap (f b) q := begin induction p; induction q; reflexivity end hott theorem bimapCharacterization' {A : Type u} {B : Type v} {C : Type w} {a b : A} {a' b' : B} (f : A → B → C) (p : a = b) (q : a' = b') : - bimap f p q = Id.map (f a) q ⬝ @Id.map A C a b (f · b') p := + bimap f p q = ap (f a) q ⬝ @ap A C a b (f · b') p := begin induction p; induction q; reflexivity end hott theorem bimapInv {A : Type u} {B : Type v} {C : Type w} {a b : A} {a' b' : B} @@ -449,9 +449,9 @@ namespace Equiv hott theorem bimapComp {A : Type u} {B : Type v} {C : Type w} {a b : A} {a' b' : B} (f : A → B → C) (p : a = b) (q : a' = b') : - Id.map (f · a') p = Id.map (f a) q ⬝ bimap f p q⁻¹ := + ap (f · a') p = ap (f a) q ⬝ bimap f p q⁻¹ := begin - induction p; symmetry; transitivity; apply Id.map; transitivity; + induction p; symmetry; transitivity; apply ap; transitivity; apply bimapReflLeft; apply Id.mapInv; apply Id.compInv end @@ -479,7 +479,7 @@ namespace Equiv begin induction p; reflexivity end hott theorem mapOverAS {A : Type u} {a b : A} (f : A → A → A) (g : A → A) (p : a = b) : - Id.map (AS f g) p = @bimap A A A a b (g a) (g b) f p (Id.map g p) := + ap (AS f g) p = @bimap A A A a b (g a) (g b) f p (ap g p) := begin induction p; reflexivity end hott lemma liftedHapply {A : Type u} (B : A → Type v) (C : A → Type w) @@ -512,14 +512,14 @@ namespace Qinv (f : A → B) (g : B → A) (h : B → A) (G : f ∘ g ~ id) (H : h ∘ f ~ id) : g ∘ f ~ id := let F₁ := λ x, H (g (f x)); - let F₂ := λ x, Id.map h (G (f x)); + let F₂ := λ x, ap h (G (f x)); λ x, (F₁ x)⁻¹ ⬝ F₂ x ⬝ H x hott def rinvInv {A : Type u} {B : Type v} (f : A → B) (g : B → A) (h : B → A) (G : f ∘ g ~ id) (H : h ∘ f ~ id) : f ∘ h ~ id := - let F₁ := λ x, Id.map (f ∘ h) (G x); - let F₂ := λ x, Id.map f (H (g x)); + let F₁ := λ x, ap (f ∘ h) (G x); + let F₂ := λ x, ap f (H (g x)); λ x, (F₁ x)⁻¹ ⬝ F₂ x ⬝ G x hott def toBiinv {A : Type u} {B : Type v} (f : A → B) (q : qinv f) : biinv f := @@ -559,7 +559,7 @@ namespace Equiv (x y : A) (p : e.forward x = e.forward y) : x = y := begin transitivity; symmetry; apply e.leftForward; - transitivity; apply Id.map e.left; + transitivity; apply ap e.left; exact p; apply e.leftForward end @@ -567,7 +567,7 @@ namespace Equiv (x y : B) (p : e.left x = e.left y) : x = y := begin transitivity; symmetry; apply e.forwardLeft; - transitivity; apply Id.map e.forward; + transitivity; apply ap e.forward; exact p; apply e.forwardLeft end @@ -575,14 +575,14 @@ namespace Equiv (x y : B) (p : e.right x = e.right y) : x = y := begin transitivity; symmetry; apply e.forwardRight; - transitivity; apply Id.map e.forward; + transitivity; apply ap e.forward; exact p; apply e.forwardRight end end Equiv -- half adjoint equivalence def ishae {A : Type u} {B : Type v} (f : A → B) := -Σ (g : B → A) (η : g ∘ f ~ id) (ϵ : f ∘ g ~ id), Π x, Id.map f (η x) = ϵ (f x) +Σ (g : B → A) (η : g ∘ f ~ id) (ϵ : f ∘ g ~ id), Π x, ap f (η x) = ϵ (f x) def fib {A : Type u} {B : Type v} (f : A → B) (y : B) := Σ (x : A), f x = y def total {A : Type u} (B : A → Type v) := Σ x, B x diff --git a/GroundZero/Types/Id.lean b/GroundZero/Types/Id.lean index d488e03..5f253dc 100644 --- a/GroundZero/Types/Id.lean +++ b/GroundZero/Types/Id.lean @@ -3,8 +3,7 @@ import GroundZero.Proto namespace GroundZero.Types universe u v -theorem UIP {A : Type u} {a b : A} (p q : a = b) : p = q := -begin rfl end +theorem UIP {A : Type u} {a b : A} (p q : a = b) : p = q := by rfl section variable (A : Sort u) @@ -15,17 +14,17 @@ section end inductive Id {A : Type u} : A → A → Type u -| refl {a : A} : Id a a +| idp (a : A) : Id a a + +export Id (idp) infix:50 (priority := high) " = " => Id /- fails! hott theorem Id.UIP {A : Type u} {a b : A} (p q : a = b) : p = q := -begin cases p; cases q; apply Id.refl end +begin cases p; cases q; apply idp end -/ -@[match_pattern] abbrev idp {A : Type u} (a : A) : a = a := Id.refl - attribute [eliminator] Id.casesOn hott def J₁ {A : Type u} {a : A} (B : Π (b : A), a = b → Type v) @@ -34,9 +33,11 @@ hott def J₁ {A : Type u} {a : A} (B : Π (b : A), a = b → Type v) hott def J₂ {A : Type u} {b : A} (B : Π (a : A), a = b → Type v) (Bidp : B b (idp b)) {a : A} (p : a = b) : B a p := -by { induction p; apply Bidp } +begin induction p; apply Bidp end namespace Id + @[match_pattern] abbrev refl {A : Type u} {a : A} : a = a := idp a + hott def symm {A : Type u} {a b : A} (p : a = b) : b = a := begin induction p; apply idp end @@ -44,7 +45,7 @@ namespace Id (p : a = b) (q : b = c) : a = c := begin induction p; apply q end - instance (A : Type u) : Reflexive (@Id A) := ⟨@Id.refl A⟩ + instance (A : Type u) : Reflexive (@Id A) := ⟨@idp A⟩ instance (A : Type u) : Symmetric (@Id A) := ⟨@symm A⟩ instance (A : Type u) : Transitive (@Id A) := ⟨@trans A⟩ @@ -91,24 +92,24 @@ namespace Id hott def mpr {A B : Type u} (p : A = B) : B → A := begin induction p; intro x; exact x end - hott def map {A : Type u} {B : Type v} {a b : A} + hott def ap {A : Type u} {B : Type v} {a b : A} (f : A → B) (p : a = b) : f a = f b := begin induction p; reflexivity end hott def cancelCompInv {A : Type u} {a b c : A} (p : a = b) (q : b = c) : (p ⬝ q) ⬝ q⁻¹ = p := - (assoc p q q⁻¹)⁻¹ ⬝ map (trans p) (compInv q) ⬝ reflRight p + (assoc p q q⁻¹)⁻¹ ⬝ ap (trans p) (compInv q) ⬝ reflRight p hott def cancelInvComp {A : Type u} {a b c : A} (p : a = b) (q : c = b) : (p ⬝ q⁻¹) ⬝ q = p := - (assoc p q⁻¹ q)⁻¹ ⬝ map (trans p) (invComp q) ⬝ reflRight p + (assoc p q⁻¹ q)⁻¹ ⬝ ap (trans p) (invComp q) ⬝ reflRight p hott def compInvCancel {A : Type u} {a b c : A} (p : a = b) (q : a = c) : p ⬝ (p⁻¹ ⬝ q) = q := - assoc p p⁻¹ q ⬝ map (· ⬝ q) (compInv p) + assoc p p⁻¹ q ⬝ ap (· ⬝ q) (compInv p) hott def invCompCancel {A : Type u} {a b c : A} (p : a = b) (q : b = c) : p⁻¹ ⬝ (p ⬝ q) = q := - assoc p⁻¹ p q ⬝ map (· ⬝ q) (invComp p) + assoc p⁻¹ p q ⬝ ap (· ⬝ q) (invComp p) hott def mapInv {A : Type u} {B : Type v} {a b : A} - (f : A → B) (p : a = b) : map f p⁻¹ = (map f p)⁻¹ := + (f : A → B) (p : a = b) : ap f p⁻¹ = (ap f p)⁻¹ := begin induction p; reflexivity end hott def transCancelLeft {A : Type u} {a b c : A} @@ -121,13 +122,6 @@ namespace Id symmetry; transitivity; { symmetry; apply reflRight }; exact μ⁻¹ end - section - variable {A : Type u} {B : Type v} {a b : A} (f : A → B) (p : a = b) - - def cong := map f p - def ap := map f p - end - hott def ap₂ {A : Type u} {B : Type v} {a b : A} {p q : a = b} (f : A → B) (r : p = q) : ap f p = ap f q := ap (ap f) r @@ -158,7 +152,7 @@ namespace Id end pointed.map def loopSpace (X : Type⁎) : Type⁎ := - ⟨X.point = X.point, Id.refl⟩ + ⟨X.point = X.point, idp X.point⟩ hott def iteratedLoopSpace : Type⁎ → ℕ → Type⁎ | X, 0 => X @@ -188,18 +182,20 @@ namespace Not λ e, nomatch e end Not -namespace whiskering +namespace Whiskering + open GroundZero.Types.Id (ap) + variable {A : Type u} {a b c : A} - hott def rightWhs {p q : a = b} (ν : p = q) (r : b = c) : p ⬝ r = q ⬝ r := + hott def rwhs {p q : a = b} (ν : p = q) (r : b = c) : p ⬝ r = q ⬝ r := begin induction r; apply (Id.reflRight p) ⬝ ν ⬝ (Id.reflRight q)⁻¹ end - infix:60 " ⬝ᵣ " => rightWhs + infix:60 " ⬝ᵣ " => rwhs - hott def leftWhs {r s : b = c} (q : a = b) (κ : r = s) : q ⬝ r = q ⬝ s := + hott def lwhs {r s : b = c} (q : a = b) (κ : r = s) : q ⬝ r = q ⬝ s := begin induction q; exact (Id.reflLeft r) ⬝ κ ⬝ (Id.reflLeft s)⁻¹ end - infix:60 " ⬝ₗ " => leftWhs + infix:60 " ⬝ₗ " => lwhs variable {p q : a = b} {r s : b = c} @@ -214,23 +210,19 @@ namespace whiskering hott lemma loop₁ {A : Type u} {a : A} {ν κ : idp a = idp a} : ν ⬝ κ = ν ⋆ κ := begin - apply Id.symm; transitivity; - { apply Id.map (· ⬝ (Id.refl ⬝ κ ⬝ Id.refl)); - apply Id.reflTwice }; - apply Id.map (ν ⬝ ·); apply Id.reflTwice + apply Id.symm; transitivity; apply ap (· ⬝ _); + apply Id.reflTwice; apply ap (ν ⬝ ·); apply Id.reflTwice end hott lemma loop₂ {A : Type u} {a : A} {ν κ : idp a = idp a} : ν ⋆′ κ = κ ⬝ ν := begin - transitivity; - { apply Id.map (· ⬝ (Id.refl ⬝ ν ⬝ Id.refl)); - apply Id.reflTwice }; - apply Id.map (κ ⬝ ·); apply Id.reflTwice + transitivity; apply ap (· ⬝ _); apply Id.reflTwice; + apply ap (κ ⬝ ·); apply Id.reflTwice end hott theorem «Eckmann–Hilton argument» {A : Type u} {a : A} (ν κ : idp a = idp a) : ν ⬝ κ = κ ⬝ ν := loop₁ ⬝ compUniq ν κ ⬝ loop₂ -end whiskering +end Whiskering end GroundZero.Types diff --git a/GroundZero/Types/Nat.lean b/GroundZero/Types/Nat.lean index f327b6a..8c46964 100644 --- a/GroundZero/Types/Nat.lean +++ b/GroundZero/Types/Nat.lean @@ -1,6 +1,7 @@ import GroundZero.HITs.Colimit import GroundZero.Structures +open GroundZero.Types.Id (ap) open GroundZero.Structures open GroundZero.Types open GroundZero @@ -35,9 +36,9 @@ begin existsi f; apply Prod.mk <;> existsi g; { intro x; induction x using Sum.casesOn; - apply Id.map Sum.inl; apply e.leftForward; reflexivity }; + apply ap Sum.inl; apply e.leftForward; reflexivity }; { intro x; induction x using Sum.casesOn; - apply Id.map Sum.inl; apply e.forwardLeft; reflexivity } + apply ap Sum.inl; apply e.forwardLeft; reflexivity } end example : ℕ ≃ (ℕ + 𝟏) + 𝟏 := @@ -77,11 +78,11 @@ hott def 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.succ n, p => Id.map Nat.succ (decode p) +| Nat.succ m, Nat.succ n, p => ap Nat.succ (decode p) hott def decodeEncodeIdp : Π m, decode (encode (idp m)) = idp m | Nat.zero => idp _ -| Nat.succ m => Id.map _ (decodeEncodeIdp m) +| Nat.succ m => ap _ (decodeEncodeIdp m) hott def decodeEncode {m n : ℕ} (p : m = n) : decode (encode p) = p := begin induction p; apply decodeEncodeIdp end @@ -101,4 +102,4 @@ end hott def recognize (m n : ℕ) : m = n ≃ code m n := ⟨encode, (⟨decode, decodeEncode⟩, ⟨decode, encodeDecode⟩)⟩ -end GroundZero.Types.Nat \ No newline at end of file +end GroundZero.Types.Nat diff --git a/GroundZero/Types/Precategory.lean b/GroundZero/Types/Precategory.lean index b44a70e..d7f4c2b 100644 --- a/GroundZero/Types/Precategory.lean +++ b/GroundZero/Types/Precategory.lean @@ -2,6 +2,7 @@ import GroundZero.Theorems.Functions import GroundZero.Theorems.Equiv open GroundZero.Theorems.Functions +open GroundZero.Types.Id (ap) open GroundZero.Types.Equiv open GroundZero.Structures open GroundZero.Theorems @@ -54,9 +55,9 @@ namespace Precategory intro ⟨g', (H₁, H₂)⟩ ⟨g, (G₁, G₂)⟩; fapply Sigma.prod; apply calc g' = id 𝒞 ∘ g' : idLeft _ _ - ... = (g ∘ f) ∘ g' : Id.map (compose · g') G₂⁻¹ + ... = (g ∘ f) ∘ g' : ap (compose · g') G₂⁻¹ ... = g ∘ (f ∘ g') : (assoc _ _ _ _)⁻¹ - ... = g ∘ id 𝒞 : Id.map (compose g) H₁ + ... = g ∘ id 𝒞 : ap (compose g) H₁ ... = g : (idRight _ _)⁻¹; apply productProp <;> apply set end @@ -112,4 +113,4 @@ namespace Precategory isProduct (op 𝒞) a b c end Precategory -end GroundZero.Types \ No newline at end of file +end GroundZero.Types diff --git a/GroundZero/Types/Sigma.lean b/GroundZero/Types/Sigma.lean index d8d7904..7261128 100644 --- a/GroundZero/Types/Sigma.lean +++ b/GroundZero/Types/Sigma.lean @@ -1,5 +1,7 @@ import GroundZero.Types.Equiv +open GroundZero.Types.Id (ap) + namespace GroundZero.Types universe u v w @@ -24,7 +26,7 @@ namespace Sigma end hott def mapFstOverProd {A : Type u} {B : A → Type v} : Π {u v : Sigma B} - (p : u.1 = v.1) (q : Equiv.subst p u.snd = v.snd), Id.map pr₁ (prod p q) = p := + (p : u.1 = v.1) (q : Equiv.subst p u.snd = v.snd), ap pr₁ (prod p q) = p := begin intro ⟨x, u⟩ ⟨y, v⟩ (p : x = y); induction p; intro (q : u = v); induction q; apply idp @@ -71,9 +73,9 @@ namespace Sigma begin existsi (map (λ x, (e x).forward)); apply Prod.mk; { existsi (map (λ x, (e x).left)); intro w; - apply Id.map (Sigma.mk w.1); apply (e w.1).leftForward }; + apply ap (Sigma.mk w.1); apply (e w.1).leftForward }; { existsi (map (λ x, (e x).right)); intro w; - apply Id.map (Sigma.mk w.1); apply (e w.1).forwardRight } + apply ap (Sigma.mk w.1); apply (e w.1).forwardRight } end hott def replaceIshae {A : Type u} {B : Type v} {C : A → Type w} @@ -84,7 +86,7 @@ namespace Sigma { apply @prod B (C ∘ g) ⟨ρ.1 (g w.1), _⟩ w (ρ.2.1 w.1); transitivity; apply Equiv.transportComp; transitivity; symmetry; apply Equiv.substComp; - transitivity; apply Id.map (λ p, Equiv.subst p w.2); + transitivity; apply ap (λ p, Equiv.subst p w.2); apply Id.compReflIfEq; symmetry; apply ρ.2.2.2; reflexivity }; { apply prod; apply Equiv.transportBackAndForward } end @@ -94,7 +96,7 @@ namespace Sigma begin existsi hmtpyInv f g; apply Qinv.toBiinv; existsi hmtpyInv g f; apply Prod.mk <;> - { intro w; apply Id.map (Sigma.mk w.1); apply Id.invInv } + { intro w; apply ap (Sigma.mk w.1); apply Id.invInv } end hott def sigmaEqOfEq {A : Type u} {B : A → Type v} {a b : Σ x, B x} @@ -121,4 +123,4 @@ namespace Sigma end end Sigma -end GroundZero.Types \ No newline at end of file +end GroundZero.Types