Skip to content

Commit b65cda5

Browse files
Vtec234Jlh18
Vtec234
and
Jlh18
authored
Unstructured interpretation (#163)
* chore: use LargeCategory * feat: complete set of interpretation theorems * feat: progress on interpretation * three more * feat: j elim substitution * feat: eta * feat: idRec modulo composition lemma * feat: finish idRec * fix: Id renamed lemmas --------- Co-authored-by: jlh18 <josephhua73@yahoo.com>
1 parent d87f63e commit b65cda5

File tree

6 files changed

+456
-793
lines changed

6 files changed

+456
-793
lines changed

‎HoTTLean/Groupoids/Basic.lean‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -71,10 +71,10 @@ instance : HasFiniteLimits Ctx := inferInstanceAs (HasFiniteLimits Grpd)
7171

7272
namespace Ctx
7373

74-
def coreAsSmall (C : Type (v+1)) [Category.{v} C] : Ctx.{max u (v+1)} :=
74+
def coreAsSmall (C : Type (v+1)) [LargeCategory.{v} C] : Ctx.{max u (v+1)} :=
7575
Grpd.of (Core (AsSmall C))
7676

77-
def coreAsSmallFunctor {C : Type (v+1)} [Category.{v} C] {D : Type (w+1)} [Category.{w} D]
77+
def coreAsSmallFunctor {C : Type (v+1)} [LargeCategory.{v} C] {D : Type (w+1)} [LargeCategory.{w} D]
7878
(F : C ⥤ D) : coreAsSmall.{v, max u (v+1) (w+1)} C
7979
⟶ coreAsSmall.{w, max u (v+1) (w+1)} D :=
8080
Grpd.homOf $ Functor.core $ AsSmall.down ⋙ F ⋙ AsSmall.up
@@ -85,8 +85,9 @@ open Ctx
8585

8686
section
8787

88-
variable {Γ Δ : Type u} [Groupoid Γ] [Groupoid Δ] (σ : Δ ⥤ Γ) {C : Type (v+1)} [Category.{v} C]
89-
{D : Type (v+1)} [Category.{v} D]
88+
variable {Γ Δ : Type u} [Groupoid Γ] [Groupoid Δ] (σ : Δ ⥤ Γ)
89+
{C : Type (v+1)} [LargeCategory.{v} C]
90+
{D : Type (v+1)} [LargeCategory.{v} D]
9091

9192
def toCoreAsSmallEquiv : (Γ ⥤ coreAsSmall C) ≃ Γ ⥤ C :=
9293
Core.functorToCoreEquiv.symm.trans functorToAsSmallEquiv

‎HoTTLean/Model/Unstructured/Hurewicz.lean‎

Lines changed: 38 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -448,9 +448,9 @@ lemma substConsEv_comp_substWk : P0.substConsEv (A := σ ≫ A) (σ ≫ a) (by s
448448
simp [substConsEv, ← path_comp, substWk]
449449

450450
@[reassoc]
451-
lemma I_map_reflSubst_comp_substConsEv : cyl.I.map (P0.polymorphicIdIntro.reflSubst a a_tp) ≫
451+
lemma I_map_reflInst_comp_substConsEv : cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫
452452
P0.substConsEv a a_tp = cyl.π.app Γ ≫ U0.sec A a a_tp := by
453-
apply (disp_pullback ..).hom_ext <;> simp [substConsEv, reflSubst, ← path_comp]
453+
apply (disp_pullback ..).hom_ext <;> simp [substConsEv, reflInst, ← path_comp, motiveInst]
454454

455455
/-- An auxiliary definition for `connection`. -/
456456
def connectionLift : cyl.I.obj (P0.polymorphicIdIntro.motiveCtx a a_tp) ⟶ U0.Tm :=
@@ -478,15 +478,15 @@ lemma connectionLift_comp [hrwcz0.IsUniform] :
478478
erw [← P0.substConsEv_comp_substWk_assoc]
479479
simp [← Id_comp]
480480

481-
lemma I_map_reflSubst_comp_connectionLift [hrwcz0.IsUniform] [hrwcz0.IsNormal] :
482-
cyl.I.map (P0.polymorphicIdIntro.reflSubst a a_tp) ≫ P0.connectionLift hrwcz0 a a_tp =
481+
lemma I_map_reflInst_comp_connectionLift [hrwcz0.IsUniform] [hrwcz0.IsNormal] :
482+
cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫ P0.connectionLift hrwcz0 a a_tp =
483483
P0.unPath (A := cyl.π.app Γ ≫ A) (cyl.π.app _ ≫ cyl.π.app Γ ≫ a) (by simp [a_tp]) := by
484484
simp only [connectionLift]
485485
rw [← Hurewicz.lift_comp]
486486
rw [hrwcz0.isNormal _ _ _ (U0.sec A a a_tp ≫ P0.Id (A := U0.disp A ≫ A) (U0.disp A ≫ a)
487487
(U0.var A) (by simp [a_tp]) (by simp))]
488-
· simp [← unPath_comp, reflSubst]
489-
· simp [I_map_reflSubst_comp_substConsEv_assoc]
488+
· simp [← unPath_comp, reflInst, motiveInst]
489+
· simp [I_map_reflInst_comp_substConsEv_assoc]
490490

491491
/-- Fix `Γ ⊢ a : A`, we think of `connection` as a cubical (as opposed to globular)
492492
homotopy `(i j : I);(x : A)(p : Id(a,x)) ⊢ χ i j : A`
@@ -541,16 +541,16 @@ lemma connection_comp [hrwcz0.IsUniform] :
541541
rw! [connectionLift_comp _ _ _ _ a_tp]
542542
simp [← path_comp, motiveSubst]
543543

544-
lemma I_map_I_map_reflSubst_comp_connection [hrwcz0.IsUniform] [hrwcz0.IsNormal] :
545-
cyl.I.map (cyl.I.map (P0.polymorphicIdIntro.reflSubst a a_tp)) ≫ P0.connection hrwcz0 a a_tp =
544+
lemma I_map_I_map_reflInst_comp_connection [hrwcz0.IsUniform] [hrwcz0.IsNormal] :
545+
cyl.I.map (cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp)) ≫ P0.connection hrwcz0 a a_tp =
546546
cyl.π.app (cyl.I.obj Γ) ≫ cyl.π.app Γ ≫ a := by
547547
simp only [connection, path']
548548
fapply P0.path_ext
549-
(cyl.I.map (P0.polymorphicIdIntro.reflSubst a a_tp) ≫ P0.substConsEv a a_tp ≫ U0.disp A ≫ A)
550-
(cyl.I.map (P0.polymorphicIdIntro.reflSubst a a_tp) ≫ P0.substConsEv a a_tp ≫ U0.disp A ≫ a)
551-
(cyl.I.map (P0.polymorphicIdIntro.reflSubst a a_tp) ≫ P0.substConsEv a a_tp ≫ U0.var A)
552-
<;> simp [a_tp, ← path_comp, reflSubst]
553-
erw [I_map_reflSubst_comp_connectionLift]
549+
(cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫ P0.substConsEv a a_tp ≫ U0.disp A ≫ A)
550+
(cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫ P0.substConsEv a a_tp ≫ U0.disp A ≫ a)
551+
(cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫ P0.substConsEv a a_tp ≫ U0.var A)
552+
<;> simp [a_tp, ← path_comp, reflInst, motiveInst]
553+
erw [I_map_reflInst_comp_connectionLift]
554554

555555
/-- `symmConnection` is the symmetrically flipped homotopy `j i ⊢ χ i j` (of `connection`),
556556
visualised as
@@ -601,12 +601,12 @@ lemma I_δ1_symmConnection : cyl.I.map (cyl.δ1.app _) ≫ P0.symmConnection hrw
601601
I_map_δ1_app_comp_symm_app_assoc]
602602
erw [δ1_connection] -- FIXME
603603

604-
lemma I_map_I_map_reflSubst_comp_symmConnection [hrwcz0.IsUniform] [hrwcz0.IsNormal] :
605-
cyl.I.map (cyl.I.map (P0.polymorphicIdIntro.reflSubst a a_tp)) ≫
604+
lemma I_map_I_map_reflInst_comp_symmConnection [hrwcz0.IsUniform] [hrwcz0.IsNormal] :
605+
cyl.I.map (cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp)) ≫
606606
P0.symmConnection hrwcz0 a a_tp = cyl.π.app (cyl.I.obj Γ) ≫ cyl.π.app Γ ≫ a := by
607607
simp only [symmConnection]
608608
erw [cyl.symm.naturality_assoc]
609-
simp [I_map_I_map_reflSubst_comp_connection, symm_π_π'_app_assoc]
609+
simp [I_map_I_map_reflInst_comp_connection, symm_π_π'_app_assoc]
610610

611611
lemma symmConnection_comp [hrwcz0.IsUniform] :
612612
P0.symmConnection hrwcz0 (A := σ ≫ A) (σ ≫ a) (by simp [a_tp]) =
@@ -653,13 +653,13 @@ lemma unPathSymmConnection_comp [hrwcz0.IsUniform] :
653653
P0.unPathSymmConnection hrwcz0 a a_tp := by
654654
simp [unPathSymmConnection, ← unPath_comp, symmConnection_comp _ _ _ _ a_tp, motiveSubst]
655655

656-
lemma I_map_reflSubst_comp_unPathSymmConnection [hrwcz0.IsUniform] [hrwcz0.IsNormal] :
657-
cyl.I.map (P0.polymorphicIdIntro.reflSubst a a_tp) ≫ P0.unPathSymmConnection hrwcz0 a a_tp =
656+
lemma I_map_reflInst_comp_unPathSymmConnection [hrwcz0.IsUniform] [hrwcz0.IsNormal] :
657+
cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫ P0.unPathSymmConnection hrwcz0 a a_tp =
658658
cyl.π.app Γ ≫ P0.unPath (A := A) (cyl.π.app Γ ≫ a) (by simp [a_tp]) := by
659659
simp only [unPathSymmConnection, ← unPath_comp]
660660
congr 1
661-
· simp [reflSubst]
662-
· simp [I_map_I_map_reflSubst_comp_symmConnection]
661+
· simp [reflInst, motiveInst]
662+
· simp [I_map_I_map_reflInst_comp_symmConnection]
663663

664664
/-- Fixing `Γ ⊢ a : A`, `substConnection` is thought of as a substitution
665665
`(i : I); (x : A) (p : Id(a,x)) ⊢ (α i : A, β i : Id (a, α i))`
@@ -687,7 +687,7 @@ lemma substConnection_var : P0.substConnection hrwcz0 a a_tp ≫ var .. =
687687

688688
@[reassoc (attr := simp)]
689689
lemma δ0_substConnection : cyl.δ0.app _ ≫ P0.substConnection hrwcz0 a a_tp =
690-
disp .. ≫ disp .. ≫ reflSubst _ a a_tp := by
690+
disp .. ≫ disp .. ≫ reflInst _ a a_tp := by
691691
simp only [polymorphicIdIntro_Id, Functor.id_obj, motiveCtx, substConnection, comp_substCons,
692692
δ0_π'_app_assoc, ← cyl.δ1_naturality_assoc, polymorphicIdIntro_refl]
693693
rw! (transparency := .default) [δ0_unPathSymmConnection]
@@ -728,46 +728,46 @@ lemma substConnection_comp_motiveSubst [hrwcz0.IsUniform] :
728728

729729
/-- `substConnection` is *normal*. -/
730730
@[reassoc]
731-
lemma reflSubst_comp_substConnection [hrwcz0.IsUniform] [hrwcz0.IsNormal] :
732-
cyl.I.map (reflSubst _ a a_tp) ≫
733-
P0.substConnection hrwcz0 a a_tp = cyl.π.app _ ≫ reflSubst _ a a_tp := by
731+
lemma reflInst_comp_substConnection [hrwcz0.IsUniform] [hrwcz0.IsNormal] :
732+
cyl.I.map (reflInst _ a a_tp) ≫
733+
P0.substConnection hrwcz0 a a_tp = cyl.π.app _ ≫ reflInst _ a a_tp := by
734734
simp only [substConnection]
735735
apply (disp_pullback ..).hom_ext
736-
· simp [I_map_reflSubst_comp_unPathSymmConnection]
736+
· simp [I_map_reflInst_comp_unPathSymmConnection]
737737
· apply (disp_pullback ..).hom_ext
738-
· simp [← δ1_naturality_assoc, I_map_I_map_reflSubst_comp_symmConnection]
739-
· simp [reflSubst]
738+
· simp [← δ1_naturality_assoc, I_map_I_map_reflInst_comp_symmConnection]
739+
· simp [reflInst, motiveInst]
740740

741741
end connection
742742

743743
def polymorphicIdElim (hrwcz0 : Hurewicz cyl U0.tp) [hrwcz0.IsUniform] [hrwcz0.IsNormal]
744744
(U1 : UnstructuredUniverse Ctx) (hrwcz1 : Hurewicz cyl U1.tp) [Hurewicz.IsUniform hrwcz1]
745745
[Hurewicz.IsNormal hrwcz1] : PolymorphicIdElim (polymorphicIdIntro P0) U1 where
746-
j a a_tp C c c_tp := cyl.δ1.app _ ≫ hrwcz1.lift (disp .. ≫ disp .. ≫ c)
746+
jElim a a_tp C c c_tp := cyl.δ1.app _ ≫ hrwcz1.lift (disp .. ≫ disp .. ≫ c)
747747
(substConnection P0 hrwcz0 a a_tp ≫ C) (by rw [δ0_substConnection_assoc]; simp [c_tp]) -- FIXME simp failed
748-
comp_j σ A a a_tp C c c_tp := by
748+
jElim_comp σ A a a_tp C c c_tp := by
749749
slice_rhs 1 2 => rw [← δ1_naturality]
750750
slice_rhs 2 3 => rw [← hrwcz1.lift_comp]
751751
congr 2
752752
· simp [motiveSubst, substWk_disp_assoc]
753753
· rw [substConnection_comp_motiveSubst_assoc]
754-
j_tp a a_tp C c c_tp := by
754+
jElim_tp a a_tp C c c_tp := by
755755
simp only [motiveCtx, polymorphicIdIntro_Id, Category.assoc, Hurewicz.lift_comp_self']
756756
erw [δ1_substConnection_assoc] -- FIXME simp, rw failed
757-
reflSubst_j {Γ A} a a_tp C c c_tp := calc _
758-
_ = cyl.δ1.app Γ ≫ cyl.I.map (reflSubst _ a a_tp) ≫
757+
reflSubst_jElim {Γ A} a a_tp C c c_tp := calc _
758+
_ = cyl.δ1.app Γ ≫ cyl.I.map (reflInst _ a a_tp) ≫
759759
hrwcz1.lift (U0.disp (weakenId _ a a_tp) ≫ U0.disp A ≫ c)
760760
(P0.substConnection hrwcz0 a a_tp ≫ C) _ := by
761761
rw [← δ1_naturality_assoc]
762762
_ = cyl.δ1.app Γ ≫
763763
hrwcz1.lift
764-
(reflSubst _ a a_tp ≫ disp .. ≫ disp .. ≫ c)
765-
(cyl.I.map (reflSubst _ a a_tp) ≫ P0.substConnection hrwcz0 a a_tp ≫ C) _ := by
764+
(reflInst _ a a_tp ≫ disp .. ≫ disp .. ≫ c)
765+
(cyl.I.map (reflInst _ a a_tp) ≫ P0.substConnection hrwcz0 a a_tp ≫ C) _ := by
766766
rw [← Hurewicz.lift_comp]
767-
_ = cyl.δ1.app Γ ≫ cyl.π.app Γ ≫ P0.polymorphicIdIntro.reflSubst a a_tp ≫
767+
_ = cyl.δ1.app Γ ≫ cyl.π.app Γ ≫ P0.polymorphicIdIntro.reflInst a a_tp ≫
768768
U0.disp (P0.polymorphicIdIntro.weakenId a a_tp) ≫ U0.disp A ≫ c := by
769-
rw [Hurewicz.isNormal hrwcz1 _ _ _ (P0.polymorphicIdIntro.reflSubst a a_tp ≫ C)]
770-
rw [reflSubst_comp_substConnection_assoc]
771-
_ = c := by simp [reflSubst]
769+
rw [Hurewicz.isNormal hrwcz1 _ _ _ (P0.polymorphicIdIntro.reflInst a a_tp ≫ C)]
770+
rw [reflInst_comp_substConnection_assoc]
771+
_ = c := by simp [reflInst, motiveInst]
772772

773773
end Path

0 commit comments

Comments
 (0)