From b91b53056facc790918e6771240210e927d2c15d Mon Sep 17 00:00:00 2001 From: jlh18 Date: Thu, 11 Dec 2025 13:05:10 -0500 Subject: [PATCH] chore: rename Path.Id to PathType.Path --- HoTTLean/Groupoids/Id.lean | 346 +++++++++++----------- HoTTLean/Model/Unstructured/Hurewicz.lean | 268 ++++++++--------- 2 files changed, 307 insertions(+), 307 deletions(-) diff --git a/HoTTLean/Groupoids/Id.lean b/HoTTLean/Groupoids/Id.lean index 7e0207f6..6b418552 100644 --- a/HoTTLean/Groupoids/Id.lean +++ b/HoTTLean/Groupoids/Id.lean @@ -88,47 +88,47 @@ abbrev ttm {x y : Γ} (f : x ⟶ y) : tt x ⟶ tt y := ⟨𝟙 _, f⟩ abbrev ft (x : Γ) : ff x ⟶ tt x := ⟨⟨⟨⟩⟩, 𝟙 x⟩ abbrev tf (x : Γ) : tt x ⟶ ff x := ⟨⟨⟨⟩⟩, 𝟙 x⟩ -abbrev unPath0 : Γ ⥤ PGrpd := sectR ⟨⟨.false⟩⟩ _ ⋙ p +abbrev path0 : Γ ⥤ PGrpd := sectR ⟨⟨.false⟩⟩ _ ⋙ p -abbrev unPath1 : Γ ⥤ PGrpd := sectR ⟨⟨.true⟩⟩ _ ⋙ p +abbrev path1 : Γ ⥤ PGrpd := sectR ⟨⟨.true⟩⟩ _ ⋙ p variable {p} (p_tp : p ⋙ PGrpd.forgetToGrpd = snd _ _ ⋙ A) include p_tp in @[simp] -lemma unPath0_comp_forgetToGrpd : unPath0 p ⋙ PGrpd.forgetToGrpd = A := by +lemma path0_comp_forgetToGrpd : path0 p ⋙ PGrpd.forgetToGrpd = A := by rw [Functor.assoc, p_tp, ← Functor.assoc, sectR_comp_snd, Functor.id_comp] include p_tp in @[simp] -lemma unPath1_comp_forgetToGrpd : unPath1 p ⋙ PGrpd.forgetToGrpd = A := by +lemma path1_comp_forgetToGrpd : path1 p ⋙ PGrpd.forgetToGrpd = A := by rw [Functor.assoc, p_tp, ← Functor.assoc, sectR_comp_snd, Functor.id_comp] -lemma objFiber'_unPath0 (x) : PGrpd.objFiber' (unPath0_comp_forgetToGrpd p_tp) x = +lemma objFiber'_path0 (x) : PGrpd.objFiber' (path0_comp_forgetToGrpd p_tp) x = PGrpd.objFiber' p_tp (ff x) := by dsimp [PGrpd.objFiber', PGrpd.objFiber] @[simp] -abbrev unPathId : Γ ⥤ Grpd := - Id (A := A) (a0 := unPath0 p) (a1 := unPath1 p) - (unPath0_comp_forgetToGrpd p_tp) (unPath1_comp_forgetToGrpd p_tp) +abbrev pathId : Γ ⥤ Grpd := + Id (A := A) (a0 := path0 p) (a1 := path1 p) + (path0_comp_forgetToGrpd p_tp) (path1_comp_forgetToGrpd p_tp) @[simps!] -def unPathFibObj (x : Γ) : @IdObj _ _ A (unPath0 p) (unPath1 p) (unPath0_comp_forgetToGrpd p_tp) - (unPath1_comp_forgetToGrpd p_tp) x := - ⟨eqToHom (by simp [objFiber'_unPath0 p_tp]) ≫ PGrpd.mapFiber' p_tp (ft x)⟩ +def pathFibObj (x : Γ) : @IdObj _ _ A (path0 p) (path1 p) (path0_comp_forgetToGrpd p_tp) + (path1_comp_forgetToGrpd p_tp) x := + ⟨eqToHom (by simp [objFiber'_path0 p_tp]) ≫ PGrpd.mapFiber' p_tp (ft x)⟩ -lemma unPathFibObj_comp (x : Δ) : unPathFibObj (A := σ ⋙ A) (p := Functor.prod (𝟭 _) σ ⋙ p) - (by simp [Functor.assoc, p_tp]; rfl) x = unPathFibObj p_tp (σ.obj x) := by +lemma pathFibObj_comp (x : Δ) : pathFibObj (A := σ ⋙ A) (p := Functor.prod (𝟭 _) σ ⋙ p) + (by simp [Functor.assoc, p_tp]; rfl) x = pathFibObj p_tp (σ.obj x) := by apply Discrete.ext - simp only [Functor.comp_obj, unPathFibObj_as, Functor.comp_map, PGrpd.mapFiber', snd_obj, snd_map, + simp only [Functor.comp_obj, pathFibObj_as, Functor.comp_map, PGrpd.mapFiber', snd_obj, snd_map, Functor.prod_obj, Functor.id_obj, Functor.Grothendieck.forget_obj, PGrpd.objFiber'EqToHom, Functor.prod_map, Functor.id_map, PGrpd.mapFiber'EqToHom, Grpd.eqToHom_hom, eqToHom_trans_assoc] rw! [CategoryTheory.Functor.map_id] -lemma IdMap_unPath {x y} (f : x ⟶ y) : - ((IdMap (unPath0_comp_forgetToGrpd p_tp) (unPath1_comp_forgetToGrpd p_tp) f).obj - (unPathFibObj p_tp x)).as = (unPathFibObj p_tp y).as := by +lemma IdMap_path {x y} (f : x ⟶ y) : + ((IdMap (path0_comp_forgetToGrpd p_tp) (path1_comp_forgetToGrpd p_tp) f).obj + (pathFibObj p_tp x)).as = (pathFibObj p_tp y).as := by dsimp [IdMap] have comm : ft x ≫ ttm f = ffm f ≫ ft y := by ext; rfl; simp have h1 := (PGrpd.mapFiber'_comp' p_tp (ft x) (ttm f)).symm @@ -142,50 +142,50 @@ lemma IdMap_unPath {x y} (f : x ⟶ y) : rw! [h1] simp -def unPathFibMap {x y : Γ} (f : x ⟶ y) : - (IdMap (unPath0_comp_forgetToGrpd p_tp) (unPath1_comp_forgetToGrpd p_tp) f).obj - (unPathFibObj p_tp x) ⟶ unPathFibObj p_tp y := - ⟨⟨IdMap_unPath ..⟩⟩ +def pathFibMap {x y : Γ} (f : x ⟶ y) : + (IdMap (path0_comp_forgetToGrpd p_tp) (path1_comp_forgetToGrpd p_tp) f).obj + (pathFibObj p_tp x) ⟶ pathFibObj p_tp y := + ⟨⟨IdMap_path ..⟩⟩ -lemma unPathFibMap_id (x : Γ) : unPathFibMap p_tp (𝟙 x) = eqToHom (by simp [IdMap_id]) := by +lemma pathFibMap_id (x : Γ) : pathFibMap p_tp (𝟙 x) = eqToHom (by simp [IdMap_id]) := by aesop_cat -lemma unPathFibMap_comp {x y z : Γ} (f1 : x ⟶ y) (f2 : y ⟶ z) : - unPathFibMap p_tp (f1 ≫ f2) = +lemma pathFibMap_comp {x y z : Γ} (f1 : x ⟶ y) (f2 : y ⟶ z) : + pathFibMap p_tp (f1 ≫ f2) = eqToHom (by simp only [IdMap_comp]; rfl) ≫ - ((unPathId p_tp).map f2).map (unPathFibMap p_tp f1) ≫ unPathFibMap p_tp f2 := by + ((pathId p_tp).map f2).map (pathFibMap p_tp f1) ≫ pathFibMap p_tp f2 := by aesop_cat -def unPath : Γ ⥤ PGrpd := - PGrpd.functorTo (unPathId p_tp) (unPathFibObj p_tp) (unPathFibMap p_tp) - (unPathFibMap_id p_tp) (fun f1 f2 => by dsimp only; aesop_cat) +def path : Γ ⥤ PGrpd := + PGrpd.functorTo (pathId p_tp) (pathFibObj p_tp) (pathFibMap p_tp) + (pathFibMap_id p_tp) (fun f1 f2 => by dsimp only; aesop_cat) -lemma unPath_comp : unPath (A := σ ⋙ A) (p := Functor.prod (𝟭 _) σ ⋙ p) - (by simp [Functor.assoc, p_tp]; rfl) = σ ⋙ unPath p_tp := by +lemma path_comp : path (A := σ ⋙ A) (p := Functor.prod (𝟭 _) σ ⋙ p) + (by simp [Functor.assoc, p_tp]; rfl) = σ ⋙ path p_tp := by -- rw [PGrpd.functorTo] apply PGrpd.Functor.hext · rfl · intro x - simp only [unPath, Functor.comp_obj, heq_eq_eq] + simp only [path, Functor.comp_obj, heq_eq_eq] -- rw [PGrpd.functorTo_obj_fiber] --FIXME why timeout? - convert_to unPathFibObj (A := σ ⋙ A) (p := Functor.prod (𝟭 _) σ ⋙ p) + convert_to pathFibObj (A := σ ⋙ A) (p := Functor.prod (𝟭 _) σ ⋙ p) (by simp [Functor.assoc, p_tp]; rfl) x = - unPathFibObj (A := A) (p := p) p_tp (σ.obj x) - rw [unPathFibObj_comp] + pathFibObj (A := A) (p := p) p_tp (σ.obj x) + rw [pathFibObj_comp] · intro x y f - simp only [unPath, Functor.comp_map] + simp only [path, Functor.comp_map] -- rw [PGrpd.functorTo_map_fiber] - convert_to unPathFibMap (A := σ ⋙ A) (p := Functor.prod (𝟭 _) σ ⋙ p) + convert_to pathFibMap (A := σ ⋙ A) (p := Functor.prod (𝟭 _) σ ⋙ p) (by simp [Functor.assoc, p_tp]; rfl) f ≍ - unPathFibMap (A := A) (p := p) p_tp (σ.map f) - rw! (castMode := .all) [unPathFibObj_comp _ p_tp] - rw! (castMode := .all) [unPathFibObj_comp _ p_tp] + pathFibMap (A := A) (p := p) p_tp (σ.map f) + rw! (castMode := .all) [pathFibObj_comp _ p_tp] + rw! (castMode := .all) [pathFibObj_comp _ p_tp] rfl @[simp] -lemma unPath_comp_forgetToGrpd : unPath p_tp ⋙ PGrpd.forgetToGrpd = - Id (a0 := unPath0 p) (a1 := unPath1 p) (unPath0_comp_forgetToGrpd p_tp) - (unPath1_comp_forgetToGrpd p_tp) := +lemma path_comp_forgetToGrpd : path p_tp ⋙ PGrpd.forgetToGrpd = + Id (a0 := path0 p) (a1 := path1 p) (path0_comp_forgetToGrpd p_tp) + (path1_comp_forgetToGrpd p_tp) := rfl end @@ -195,21 +195,21 @@ section variable {p : Γ ⥤ PGrpd} (p_tp : p ⋙ PGrpd.forgetToGrpd = FunctorOperation.Id a0_tp a1_tp) -def pathFibObj : (x : Grpd.Interval × Γ) → A.obj x.2 +def unpathFibObj : (x : Grpd.Interval × Γ) → A.obj x.2 | ⟨⟨⟨.false⟩⟩, x2⟩ => PGrpd.objFiber' a0_tp x2 | ⟨⟨⟨.true⟩⟩, x2⟩ => PGrpd.objFiber' a1_tp x2 -def pathFibMap : {x y : Grpd.Interval × Γ} → (f : x ⟶ y) → - ((A.map f.2).obj (pathFibObj a0_tp a1_tp x) ⟶ pathFibObj a0_tp a1_tp y) +def unpathFibMap : {x y : Grpd.Interval × Γ} → (f : x ⟶ y) → + ((A.map f.2).obj (unpathFibObj a0_tp a1_tp x) ⟶ unpathFibObj a0_tp a1_tp y) | ⟨⟨⟨.false⟩⟩, _⟩, ⟨⟨⟨.false⟩⟩, _⟩, f => PGrpd.mapFiber' a0_tp f.2 | ⟨⟨⟨.false⟩⟩, _⟩, ⟨⟨⟨.true⟩⟩, y2⟩, f => (PGrpd.mapFiber' a0_tp f.2) ≫ (PGrpd.objFiber' p_tp y2).1 | ⟨⟨⟨.true⟩⟩, _⟩, ⟨⟨⟨.false⟩⟩, y2⟩, f => (PGrpd.mapFiber' a1_tp f.2) ≫ inv (PGrpd.objFiber' p_tp y2).1 | ⟨⟨⟨.true⟩⟩, _⟩, ⟨⟨⟨.true⟩⟩, _⟩, f => PGrpd.mapFiber' a1_tp f.2 -lemma pathFibMap_id (x : Grpd.Interval × Γ) : pathFibMap a0_tp a1_tp p_tp (𝟙 x) = +lemma unpathFibMap_id (x : Grpd.Interval × Γ) : unpathFibMap a0_tp a1_tp p_tp (𝟙 x) = eqToHom (by simp) := by - rcases x with ⟨⟨⟨_|_⟩⟩ , x⟩ <;> simp [pathFibMap] + rcases x with ⟨⟨⟨_|_⟩⟩ , x⟩ <;> simp [unpathFibMap] open PGrpd in lemma map_objFiber'_mapFiber' {x y} (f : x ⟶ y) : @@ -231,11 +231,11 @@ lemma mapFiber'_inv_objFiber' {x y} (f : x ⟶ y) : mapFiber' a1_tp f ≫ inv (o slice_lhs 1 2 => rw [map_objFiber'_mapFiber'] simp -attribute [simp] pathFibMap pathFibObj PGrpd.mapFiber'_comp' Grpd.forgetToCat in -lemma pathFibMap_comp {x y z : Grpd.Interval × Γ} (f : x ⟶ y) (g : y ⟶ z) : - pathFibMap a0_tp a1_tp p_tp (f ≫ g) = - eqToHom (by simp) ≫ (A.map g.2).map (pathFibMap a0_tp a1_tp p_tp f) ≫ - pathFibMap a0_tp a1_tp p_tp g := by +attribute [simp] unpathFibMap unpathFibObj PGrpd.mapFiber'_comp' Grpd.forgetToCat in +lemma unpathFibMap_comp {x y z : Grpd.Interval × Γ} (f : x ⟶ y) (g : y ⟶ z) : + unpathFibMap a0_tp a1_tp p_tp (f ≫ g) = + eqToHom (by simp) ≫ (A.map g.2).map (unpathFibMap a0_tp a1_tp p_tp f) ≫ + unpathFibMap a0_tp a1_tp p_tp g := by rcases x with ⟨⟨⟨_|_⟩⟩ , x⟩ · rcases y with ⟨⟨⟨_|_⟩⟩ , y⟩ · rcases z with ⟨⟨⟨_|_⟩⟩ , z⟩ <;> simp @@ -244,116 +244,116 @@ lemma pathFibMap_comp {x y z : Grpd.Interval × Γ} (f : x ⟶ y) (g : y ⟶ z) · rcases y with ⟨⟨⟨_|_⟩⟩ , y⟩ · rcases z with ⟨⟨⟨_|_⟩⟩ , z⟩ · simp; simp [mapFiber'_inv_objFiber'] - · simp only [prod_comp, pathFibObj, pathFibMap, PGrpd.mapFiber'_comp', Functor.map_comp, + · simp only [prod_comp, unpathFibObj, unpathFibMap, PGrpd.mapFiber'_comp', Functor.map_comp, Functor.map_inv, Category.assoc] slice_rhs 3 4 => rw [← mapFiber'_inv_objFiber'] simp · rcases z with ⟨⟨⟨_|_⟩⟩ , z⟩ <;> simp -def path : Grpd.Interval × Γ ⥤ PGrpd := - Functor.Grothendieck.functorTo (snd _ _ ⋙ A) (pathFibObj a0_tp a1_tp) - (pathFibMap a0_tp a1_tp p_tp) (pathFibMap_id a0_tp a1_tp p_tp) - (pathFibMap_comp a0_tp a1_tp p_tp) +def unpath : Grpd.Interval × Γ ⥤ PGrpd := + Functor.Grothendieck.functorTo (snd _ _ ⋙ A) (unpathFibObj a0_tp a1_tp) + (unpathFibMap a0_tp a1_tp p_tp) (unpathFibMap_id a0_tp a1_tp p_tp) + (unpathFibMap_comp a0_tp a1_tp p_tp) @[simp] -lemma path_comp_forgetToGrpd : path a0_tp a1_tp p_tp ⋙ PGrpd.forgetToGrpd = snd _ _ ⋙ A := by +lemma unpath_comp_forgetToGrpd : unpath a0_tp a1_tp p_tp ⋙ PGrpd.forgetToGrpd = snd _ _ ⋙ A := by rfl @[simp] -lemma sectR_false_comp_path : sectR ⟨⟨.false⟩⟩ _ ⋙ path a0_tp a1_tp p_tp = a0 := by +lemma sectR_false_comp_unpath : sectR ⟨⟨.false⟩⟩ _ ⋙ unpath a0_tp a1_tp p_tp = a0 := by apply Functor.Grothendieck.FunctorTo.hext - · rw [Functor.assoc, path, Functor.Grothendieck.functorTo_forget, ← Functor.assoc, + · rw [Functor.assoc, unpath, Functor.Grothendieck.functorTo_forget, ← Functor.assoc, sectR_comp_snd, a0_tp, Functor.id_comp] · intro x - simp [path, PGrpd.objFiber', PGrpd.objFiber, Grpd.eqToHom_obj] + simp [unpath, PGrpd.objFiber', PGrpd.objFiber, Grpd.eqToHom_obj] · intro x y f - simp [path, PGrpd.mapFiber', PGrpd.mapFiber'EqToHom, Grpd.eqToHom_hom] + simp [unpath, PGrpd.mapFiber', PGrpd.mapFiber'EqToHom, Grpd.eqToHom_hom] apply HEq.trans (eqToHom_comp_heq _ _) simp @[simp] -lemma sectR_true_comp_path : sectR ⟨⟨.true⟩⟩ _ ⋙ path a0_tp a1_tp p_tp = a1 := by +lemma sectR_true_comp_unpath : sectR ⟨⟨.true⟩⟩ _ ⋙ unpath a0_tp a1_tp p_tp = a1 := by apply Functor.Grothendieck.FunctorTo.hext - · rw [Functor.assoc, path, Functor.Grothendieck.functorTo_forget, ← Functor.assoc, + · rw [Functor.assoc, unpath, Functor.Grothendieck.functorTo_forget, ← Functor.assoc, sectR_comp_snd, a1_tp, Functor.id_comp] · intro x - simp [path, PGrpd.objFiber', PGrpd.objFiber, Grpd.eqToHom_obj] + simp [unpath, PGrpd.objFiber', PGrpd.objFiber, Grpd.eqToHom_obj] · intro x y f - simp [path, PGrpd.mapFiber', PGrpd.mapFiber'EqToHom, Grpd.eqToHom_hom] + simp [unpath, PGrpd.mapFiber', PGrpd.mapFiber'EqToHom, Grpd.eqToHom_hom] apply HEq.trans (eqToHom_comp_heq _ _) simp -lemma unPath0_path : unPath0 (path a0_tp a1_tp p_tp) = a0 := by +lemma path0_unpath : path0 (unpath a0_tp a1_tp p_tp) = a0 := by apply Functor.Grothendieck.FunctorTo.hext · simp · intro x - simpa [path] using PGrpd.objFiber'_heq a0_tp + simpa [unpath] using PGrpd.objFiber'_heq a0_tp · intro x y f - simpa [path] using PGrpd.mapFiber'_heq a0_tp f + simpa [unpath] using PGrpd.mapFiber'_heq a0_tp f -lemma unPath1_path : unPath1 (path a0_tp a1_tp p_tp) = a1 := by +lemma path1_unpath : path1 (unpath a0_tp a1_tp p_tp) = a1 := by apply Functor.Grothendieck.FunctorTo.hext · simp · intro x - simpa [path] using PGrpd.objFiber'_heq a1_tp + simpa [unpath] using PGrpd.objFiber'_heq a1_tp · intro x y f - simpa [path] using PGrpd.mapFiber'_heq a1_tp f + simpa [unpath] using PGrpd.mapFiber'_heq a1_tp f -lemma unPathFibObj_path (x) : unPathFibObj (path_comp_forgetToGrpd a0_tp a1_tp p_tp) x = +lemma pathFibObj_unpath (x) : pathFibObj (unpath_comp_forgetToGrpd a0_tp a1_tp p_tp) x = PGrpd.objFiber' p_tp x := by - dsimp only [unPathFibObj] + dsimp only [pathFibObj] apply Discrete.ext - simp [PGrpd.mapFiber, path] + simp [PGrpd.mapFiber, unpath] -lemma mapFiber_path_ft (x) : PGrpd.mapFiber (path a0_tp a1_tp p_tp) (ft x) = - eqToHom (by simp [PGrpd.mapObjFiber, path, PGrpd.objFiber]) ≫ +lemma mapFiber_unpath_ft (x) : PGrpd.mapFiber (unpath a0_tp a1_tp p_tp) (ft x) = + eqToHom (by simp [PGrpd.mapObjFiber, unpath, PGrpd.objFiber]) ≫ (PGrpd.objFiber' p_tp x).as := by - dsimp [path, PGrpd.mapFiber] + dsimp [unpath, PGrpd.mapFiber] simp -lemma unPath_path : unPath (A := A) (path_comp_forgetToGrpd a0_tp a1_tp p_tp) = p := by +lemma path_unpath : path (A := A) (unpath_comp_forgetToGrpd a0_tp a1_tp p_tp) = p := by apply Functor.Grothendieck.FunctorTo.hext - · rw [unPath_comp_forgetToGrpd, p_tp] - rw! [unPath0_path, unPath1_path] + · rw [path_comp_forgetToGrpd, p_tp] + rw! [path0_unpath, path1_unpath] · intro x - exact heq_of_eq_of_heq (unPathFibObj_path ..) (PGrpd.objFiber'_heq p_tp) + exact heq_of_eq_of_heq (pathFibObj_unpath ..) (PGrpd.objFiber'_heq p_tp) · intro x y f - dsimp only [unPath] - apply heq_of_eq_of_heq (PGrpd.functorTo_map_fiber _ _ _ _ (unPathFibMap_comp _) _) - dsimp only [unPathFibMap] + dsimp only [path] + apply heq_of_eq_of_heq (PGrpd.functorTo_map_fiber _ _ _ _ (pathFibMap_comp _) _) + dsimp only [pathFibMap] apply HEq.trans _ (PGrpd.mapFiber'_heq p_tp f) apply Discrete.Hom.hext · simp · simp only [heq_eq_eq] ext - simp [IdMap_unPath, map_objFiber'_mapFiber', mapFiber_path_ft] - · simp [unPathFibObj_path] + simp [IdMap_path, map_objFiber'_mapFiber', mapFiber_unpath_ft] + · simp [pathFibObj_unpath] end section variable {p : Grpd.Interval × Γ ⥤ PGrpd} (p_tp : p ⋙ PGrpd.forgetToGrpd = snd _ _ ⋙ A) - (δ0_p : unPath0 p = a0) (δ1_p : unPath1 p = a1) + (δ0_p : path0 p = a0) (δ1_p : path1 p = a1) include δ0_p p_tp in lemma a0_comp_forgetToGrpd : a0 ⋙ PGrpd.forgetToGrpd = A := by - rw [← δ0_p, unPath0, Functor.assoc, p_tp, ← Functor.assoc, sectR_comp_snd, Functor.id_comp] + rw [← δ0_p, path0, Functor.assoc, p_tp, ← Functor.assoc, sectR_comp_snd, Functor.id_comp] include δ1_p p_tp in lemma a1_comp_forgetToGrpd : a1 ⋙ PGrpd.forgetToGrpd = A := by - rw [← δ1_p, unPath1, Functor.assoc, p_tp, ← Functor.assoc, sectR_comp_snd, Functor.id_comp] + rw [← δ1_p, path1, Functor.assoc, p_tp, ← Functor.assoc, sectR_comp_snd, Functor.id_comp] lemma obj_ff_fiber (x) : (p.obj (ff x)).fiber ≍ PGrpd.objFiber' (a0_comp_forgetToGrpd p_tp δ0_p) x := by symm - convert PGrpd.objFiber'_heq (unPath0_comp_forgetToGrpd p_tp) (x := x) + convert PGrpd.objFiber'_heq (path0_comp_forgetToGrpd p_tp) (x := x) rw [← δ0_p] lemma obj_tt_fiber (x) : (p.obj (tt x)).fiber ≍ PGrpd.objFiber' (a1_comp_forgetToGrpd p_tp δ1_p) x := by symm - convert PGrpd.objFiber'_heq (unPath1_comp_forgetToGrpd p_tp) (x := x) + convert PGrpd.objFiber'_heq (path1_comp_forgetToGrpd p_tp) (x := x) rw [← δ1_p] lemma map_ff_fiber {x y : Γ} (f : ff x ⟶ ff y) : (p.map f).fiber ≍ @@ -364,7 +364,7 @@ lemma map_ff_fiber {x y : Γ} (f : ff x ⟶ ff y) : (p.map f).fiber ≍ rw! [PGrpd.objFiber'_heq p_tp] · rw! [← obj_ff_fiber p_tp δ0_p y] rw! [PGrpd.objFiber'_heq p_tp] - · rw! [← δ0_p, unPath0, PGrpd.mapFiber'_naturality p_tp (sectR { down := { as := false } } Γ)] + · rw! [← δ0_p, path0, PGrpd.mapFiber'_naturality p_tp (sectR { down := { as := false } } Γ)] rw! [PGrpd.mapFiber'_heq p_tp] rw! [PGrpd.mapFiber'_heq p_tp f] rfl @@ -377,7 +377,7 @@ lemma map_tt_fiber {x y : Γ} (f : tt x ⟶ tt y) : (p.map f).fiber ≍ rw! [PGrpd.objFiber'_heq p_tp] · rw! [← obj_tt_fiber p_tp δ1_p y] rw! [PGrpd.objFiber'_heq p_tp] - · rw! [← δ1_p, unPath1, PGrpd.mapFiber'_naturality p_tp (sectR { down := { as := true } } Γ)] + · rw! [← δ1_p, path1, PGrpd.mapFiber'_naturality p_tp (sectR { down := { as := true } } Γ)] rw! [PGrpd.mapFiber'_heq p_tp] rw! [PGrpd.mapFiber'_heq p_tp f] rfl @@ -393,17 +393,17 @@ lemma mapFiber'_ttm {x y : Γ} (f : x ⟶ y) : PGrpd.mapFiber' p_tp (ttm f) ≍ simp @[simp] -lemma objFiber_unPath (x) : PGrpd.objFiber (unPath p_tp) x = unPathFibObj p_tp x := +lemma objFiber_path (x) : PGrpd.objFiber (path p_tp) x = pathFibObj p_tp x := rfl -lemma objFiber'_unPath_as (x) : (PGrpd.objFiber' (unPath_comp_forgetToGrpd p_tp) x).as = - eqToHom (by simp [objFiber'_unPath0 p_tp]) ≫ PGrpd.mapFiber' p_tp (ft x) := by +lemma objFiber'_path_as (x) : (PGrpd.objFiber' (path_comp_forgetToGrpd p_tp) x).as = + eqToHom (by simp [objFiber'_path0 p_tp]) ≫ PGrpd.mapFiber' p_tp (ft x) := by rfl lemma mapFiber_ft (x) : PGrpd.mapFiber p (ft x) ≍ - (PGrpd.objFiber' (unPath_comp_forgetToGrpd p_tp) x).as := by + (PGrpd.objFiber' (path_comp_forgetToGrpd p_tp) x).as := by symm - rw [objFiber'_unPath_as] + rw [objFiber'_path_as] simp only [Functor.comp_obj, snd_obj, Functor.comp_map, snd_map, PGrpd.mapFiber', Grpd.forgetToCat, Functor.Grothendieck.forget_obj, PGrpd.objFiber'EqToHom, PGrpd.mapFiber'EqToHom, Grpd.eqToHom_hom, eqToHom_trans_assoc, PGrpd.mapFiber] @@ -444,14 +444,14 @@ lemma inv_mapFiber_tf_heq (y : Γ) : simp open PGrpd in -lemma path_map_ft_fiber {x y} (f : ff x ⟶ tt y) : - ((path (a0_comp_forgetToGrpd p_tp δ0_p) (a1_comp_forgetToGrpd p_tp δ1_p) - (p := FunctorOperation.Path.unPath p_tp) - (by rw [unPath_comp_forgetToGrpd]; congr)).map f).fiber ≍ (p.map f).fiber := by - simp only [Grpd.forgetToCat, path, Functor.Grothendieck.functorTo_obj_base, +lemma unpath_map_ft_fiber {x y} (f : ff x ⟶ tt y) : + ((unpath (a0_comp_forgetToGrpd p_tp δ0_p) (a1_comp_forgetToGrpd p_tp δ1_p) + (p := FunctorOperation.Path.path p_tp) + (by rw [path_comp_forgetToGrpd]; congr)).map f).fiber ≍ (p.map f).fiber := by + simp only [Grpd.forgetToCat, unpath, Functor.Grothendieck.functorTo_obj_base, Functor.comp_obj, snd_obj, Cat.of_α, Functor.Grothendieck.functorTo_map_base, - Functor.comp_map, snd_map, id_eq, Functor.Grothendieck.functorTo_obj_fiber, pathFibObj, - Functor.Grothendieck.functorTo_map_fiber, pathFibMap] + Functor.comp_map, snd_map, id_eq, Functor.Grothendieck.functorTo_obj_fiber, unpathFibObj, + Functor.Grothendieck.functorTo_map_fiber, unpathFibMap] -- have hf : f = ttm f.2 ≫ ft y := by aesop_cat -- TODO: mwe and report: this should not type check have hf : f = ffm f.2 ≫ ft y := by aesop_cat @@ -469,14 +469,14 @@ lemma path_map_ft_fiber {x y} (f : ff x ⟶ tt y) : Functor.comp_map, Functor.Grothendieck.forget_map, snd_obj, snd_map, Grpd.comp_eq_comp] at H erw [Functor.congr_hom p_tp (ft y)] - rw! [← δ0_p, unPath0, objFiber'_naturality (sectR ..) p_tp, objFiber'_heq] + rw! [← δ0_p, path0, objFiber'_naturality (sectR ..) p_tp, objFiber'_heq] simp [mapObjFiber, Grpd.eqToHom_obj, objFiber, Functor.congr_obj H, Grpd.eqToHom_obj] · simp only [Functor.Grothendieck.forget_map] - rw! [← δ0_p, unPath0, objFiber'_naturality (sectR ..) p_tp, objFiber'_heq, + rw! [← δ0_p, path0, objFiber'_naturality (sectR ..) p_tp, objFiber'_heq, map_ft_base p_tp, Grpd.eqToHom_obj] simp [objFiber] - · rw! [← δ1_p, unPath1, objFiber'_naturality (sectR ..) p_tp, objFiber'_heq] + · rw! [← δ1_p, path1, objFiber'_naturality (sectR ..) p_tp, objFiber'_heq] simp [objFiber] · simp only [Functor.comp_obj, snd_obj, Functor.comp_map, snd_map, Grpd.forgetToCat, Functor.Grothendieck.forget_obj, Functor.Grothendieck.forget_map, cast_heq_iff_heq] @@ -493,14 +493,14 @@ lemma path_map_ft_fiber {x y} (f : ff x ⟶ tt y) : simp [objFiber] open PGrpd in -lemma path_map_tf_fiber {x y} (f : tt x ⟶ ff y) : - ((path (a0_comp_forgetToGrpd p_tp δ0_p) (a1_comp_forgetToGrpd p_tp δ1_p) - (p := FunctorOperation.Path.unPath p_tp) - (by rw [unPath_comp_forgetToGrpd]; congr)).map f).fiber ≍ (p.map f).fiber := by - simp only [Grpd.forgetToCat, path, Functor.Grothendieck.functorTo_obj_base, Functor.comp_obj, +lemma unpath_map_tf_fiber {x y} (f : tt x ⟶ ff y) : + ((unpath (a0_comp_forgetToGrpd p_tp δ0_p) (a1_comp_forgetToGrpd p_tp δ1_p) + (p := FunctorOperation.Path.path p_tp) + (by rw [path_comp_forgetToGrpd]; congr)).map f).fiber ≍ (p.map f).fiber := by + simp only [Grpd.forgetToCat, unpath, Functor.Grothendieck.functorTo_obj_base, Functor.comp_obj, snd_obj, Cat.of_α, Functor.Grothendieck.functorTo_map_base, Functor.comp_map, snd_map, id_eq, - Functor.Grothendieck.functorTo_obj_fiber, pathFibObj, Functor.Grothendieck.functorTo_map_fiber, - pathFibMap] + Functor.Grothendieck.functorTo_obj_fiber, unpathFibObj, Functor.Grothendieck.functorTo_map_fiber, + unpathFibMap] have hf : f = ttm f.2 ≫ tf y := by aesop_cat conv => rhs; rw! (castMode := .all) [hf] simp only [heq_eqRec_iff_heq] @@ -510,7 +510,7 @@ lemma path_map_tf_fiber {x y} (f : tt x ⟶ ff y) : apply HEq.trans _ (eqToHom_comp_heq ..).symm have : A.obj y ≍ forgetToGrpd.obj (p.obj (ff y)) := by erw [Functor.congr_obj p_tp (ff y)]; simp have : objFiber' (a0_comp_forgetToGrpd p_tp δ0_p) y ≍ objFiber p (ff y) := by - rw! [← δ0_p, unPath0, objFiber'_naturality (sectR ..) p_tp, objFiber'_heq] + rw! [← δ0_p, path0, objFiber'_naturality (sectR ..) p_tp, objFiber'_heq] simp [objFiber] apply Grpd.comp_heq_comp · assumption @@ -519,11 +519,11 @@ lemma path_map_tf_fiber {x y} (f : tt x ⟶ ff y) : Functor.comp_map, Functor.Grothendieck.forget_map, snd_obj, snd_map, Grpd.comp_eq_comp] at H erw [Functor.congr_hom p_tp (tf y)] - rw! [← δ1_p, unPath1, objFiber'_naturality (sectR ..) p_tp, objFiber'_heq] + rw! [← δ1_p, path1, objFiber'_naturality (sectR ..) p_tp, objFiber'_heq] simp [mapObjFiber, Grpd.eqToHom_obj, objFiber, Functor.congr_obj H, Grpd.eqToHom_obj] · simp only [Functor.Grothendieck.forget_map] - rw! [← δ1_p, unPath1, objFiber'_naturality (sectR ..) p_tp, objFiber'_heq, + rw! [← δ1_p, path1, objFiber'_naturality (sectR ..) p_tp, objFiber'_heq, map_tf_base p_tp, Grpd.eqToHom_obj] simp [objFiber] · assumption @@ -537,35 +537,35 @@ lemma path_map_tf_fiber {x y} (f : tt x ⟶ ff y) : · rw! [← obj_tt_fiber p_tp δ1_p] simp [mapObjFiber, objFiber, map_tf_base p_tp, Grpd.eqToHom_obj] · simp [objFiber', Grpd.eqToHom_obj] - apply HEq.trans (b := (unPathFibObj p_tp y).as) + apply HEq.trans (b := (pathFibObj p_tp y).as) · apply Discrete.as_heq_as · congr 1 · rw! [← δ0_p] - simp [unPath0, objFiber_naturality, Grpd.eqToHom_obj, objFiber'] + simp [path0, objFiber_naturality, Grpd.eqToHom_obj, objFiber'] · rw! [← δ1_p] - simp [unPath1, objFiber_naturality, Grpd.eqToHom_obj, objFiber'] + simp [path1, objFiber_naturality, Grpd.eqToHom_obj, objFiber'] · simp · simp apply HEq.trans (eqToHom_comp_heq ..) rw! [inv_mapFiber_tf_heq p_tp, mapFiber'_heq] simp [mapFiber] -lemma path_unPath : path (a0_comp_forgetToGrpd p_tp δ0_p) (a1_comp_forgetToGrpd p_tp δ1_p) - (p := FunctorOperation.Path.unPath p_tp) (by rw [unPath_comp_forgetToGrpd]; congr) = p := by +lemma unpath_path : unpath (a0_comp_forgetToGrpd p_tp δ0_p) (a1_comp_forgetToGrpd p_tp δ1_p) + (p := FunctorOperation.Path.path p_tp) (by rw [path_comp_forgetToGrpd]; congr) = p := by apply Functor.Grothendieck.FunctorTo.hext - · simp only [path, Functor.Grothendieck.functorTo_forget, p_tp] + · simp only [unpath, Functor.Grothendieck.functorTo_forget, p_tp] · intro x rcases x with ⟨⟨⟨_|_⟩⟩ , x⟩ - · simpa [path] using (obj_ff_fiber p_tp δ0_p x).symm - · simpa [path] using (obj_tt_fiber p_tp δ1_p x).symm + · simpa [unpath] using (obj_ff_fiber p_tp δ0_p x).symm + · simpa [unpath] using (obj_tt_fiber p_tp δ1_p x).symm · intro x y f rcases x with ⟨⟨⟨_|_⟩⟩ , x⟩ · rcases y with ⟨⟨⟨_|_⟩⟩ , y⟩ - · simpa [path] using (map_ff_fiber p_tp δ0_p f).symm - · exact path_map_ft_fiber p_tp δ0_p δ1_p f + · simpa [unpath] using (map_ff_fiber p_tp δ0_p f).symm + · exact unpath_map_ft_fiber p_tp δ0_p δ1_p f · rcases y with ⟨⟨⟨_|_⟩⟩ , y⟩ - · exact path_map_tf_fiber p_tp δ0_p δ1_p f - · simpa [path] using (map_tt_fiber p_tp δ1_p f).symm + · exact unpath_map_tf_fiber p_tp δ0_p δ1_p f + · simpa [unpath] using (map_tt_fiber p_tp δ1_p f).symm end @@ -604,25 +604,25 @@ section variable (p : cylinder.I.obj Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = cylinder.π.app Γ ≫ A) -def unPath : Γ ⟶ U.{v}.Tm := toCoreAsSmallEquiv.symm <| - FunctorOperation.Path.unPath (A := toCoreAsSmallEquiv A) (p := toCoreAsSmallEquiv p) (by +def path : Γ ⟶ U.{v}.Tm := toCoreAsSmallEquiv.symm <| + FunctorOperation.Path.path (A := toCoreAsSmallEquiv A) (p := toCoreAsSmallEquiv p) (by rw [← toCoreAsSmallEquiv_apply_comp_left] rw [← toCoreAsSmallEquiv_apply_comp_right, EmbeddingLike.apply_eq_iff_eq] exact p_tp) -lemma unPath_comp : unPath (A := σ ≫ A) (cylinder.I.map σ ≫ p) (by rw [Category.assoc, p_tp, +lemma path_comp : path (A := σ ≫ A) (cylinder.I.map σ ≫ p) (by rw [Category.assoc, p_tp, ← Category.assoc, cylinder.π.naturality, Category.assoc, Functor.id_map]) = - σ ≫ unPath p p_tp := by - dsimp [unPath] - rw [← toCoreAsSmallEquiv_symm_apply_comp_left, ← FunctorOperation.Path.unPath_comp] + σ ≫ path p p_tp := by + dsimp [path] + rw [← toCoreAsSmallEquiv_symm_apply_comp_left, ← FunctorOperation.Path.path_comp] -lemma unPath_tp (δ0_p : cylinder.δ0.app Γ ≫ p = a0) (δ1_p : cylinder.δ1.app Γ ≫ p = a1) : - unPath p p_tp ≫ U.tp = UId.Id (A := A) a0 a1 +lemma path_tp (δ0_p : cylinder.δ0.app Γ ≫ p = a0) (δ1_p : cylinder.δ1.app Γ ≫ p = a1) : + path p p_tp ≫ U.tp = UId.Id (A := A) a0 a1 (by rw [← δ0_p, Category.assoc, p_tp, Cylinder.δ0_π'_app_assoc]) (by rw [← δ1_p, Category.assoc, p_tp, Cylinder.δ1_π'_app_assoc]) := by - dsimp [unPath, U.tp, Id] - rw [← toCoreAsSmallEquiv_symm_apply_comp_right, FunctorOperation.Path.unPath_comp_forgetToGrpd] + dsimp [path, U.tp, Id] + rw [← toCoreAsSmallEquiv_symm_apply_comp_right, FunctorOperation.Path.path_comp_forgetToGrpd] congr 2 · rw [← δ0_p, Grpd.comp_eq_comp, toCoreAsSmallEquiv_apply_comp_left] rfl @@ -635,49 +635,49 @@ section variable (p : Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = UId.Id a0 a1 a0_tp a1_tp) -def path : cylinder.I.obj Γ ⟶ U.{v}.Tm := +def unpath : cylinder.I.obj Γ ⟶ U.{v}.Tm := have p_tp' : toCoreAsSmallEquiv p ⋙ PGrpd.forgetToGrpd = FunctorOperation.Id (pt_tp a0 a0_tp) (pt_tp a1 a1_tp) := by dsimp [U.tp, Id] at p_tp rw [← toCoreAsSmallEquiv_apply_comp_right, p_tp, Equiv.apply_symm_apply] - toCoreAsSmallEquiv.symm <| FunctorOperation.Path.path _ _ p_tp' + toCoreAsSmallEquiv.symm <| FunctorOperation.Path.unpath _ _ p_tp' -lemma path_tp : path a0 a1 a0_tp a1_tp p p_tp ≫ U.tp = cylinder.π.app Γ ≫ A := by - dsimp [path, U.tp] +lemma unpath_tp : unpath a0 a1 a0_tp a1_tp p p_tp ≫ U.tp = cylinder.π.app Γ ≫ A := by + dsimp [unpath, U.tp] rw [← toCoreAsSmallEquiv_symm_apply_comp_right, toCoreAsSmallEquiv.symm_apply_eq, - toCoreAsSmallEquiv_apply_comp_left, FunctorOperation.Path.path_comp_forgetToGrpd] + toCoreAsSmallEquiv_apply_comp_left, FunctorOperation.Path.unpath_comp_forgetToGrpd] rfl -lemma δ0_path : cylinder.δ0.app Γ ≫ path a0 a1 a0_tp a1_tp p p_tp = a0 := by - dsimp [path] +lemma δ0_unpath : cylinder.δ0.app Γ ≫ unpath a0 a1 a0_tp a1_tp p p_tp = a0 := by + dsimp [unpath] rw [← toCoreAsSmallEquiv_symm_apply_comp_left, toCoreAsSmallEquiv.symm_apply_eq] - apply FunctorOperation.Path.sectR_false_comp_path + apply FunctorOperation.Path.sectR_false_comp_unpath -lemma δ1_path : cylinder.δ1.app Γ ≫ path a0 a1 a0_tp a1_tp p p_tp = a1 := by - dsimp [path] +lemma δ1_unpath : cylinder.δ1.app Γ ≫ unpath a0 a1 a0_tp a1_tp p p_tp = a1 := by + dsimp [unpath] rw [← toCoreAsSmallEquiv_symm_apply_comp_left, toCoreAsSmallEquiv.symm_apply_eq] - apply FunctorOperation.Path.sectR_true_comp_path + apply FunctorOperation.Path.sectR_true_comp_unpath -lemma unPath_path : unPath (A := A) (path a0 a1 a0_tp a1_tp p p_tp) (path_tp ..) = p := by - dsimp [unPath, path] +lemma path_unpath : path (A := A) (unpath a0 a1 a0_tp a1_tp p p_tp) (unpath_tp ..) = p := by + dsimp [path, unpath] rw [toCoreAsSmallEquiv.symm_apply_eq] rw! (transparency := .default) [toCoreAsSmallEquiv.apply_symm_apply] - apply FunctorOperation.Path.unPath_path + apply FunctorOperation.Path.path_unpath end -lemma path_unPath (p : cylinder.I.obj Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = cylinder.π.app Γ ≫ A) +lemma unpath_path (p : cylinder.I.obj Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = cylinder.π.app Γ ≫ A) (δ0_p : cylinder.δ0.app Γ ≫ p = a0) (δ1_p : cylinder.δ1.app Γ ≫ p = a1) : - path (A := A) a0 a1 (by simp [← δ0_p, - Grpd.comp_eq_comp, p_tp]) - (by simp [← δ1_p, - Grpd.comp_eq_comp, p_tp]) (unPath p p_tp) - (unPath_tp a0 a1 p p_tp δ0_p δ1_p) = p := by - dsimp [path, unPath] + unpath (A := A) a0 a1 (by simp [← δ0_p, - Grpd.comp_eq_comp, p_tp]) + (by simp [← δ1_p, - Grpd.comp_eq_comp, p_tp]) (path p p_tp) + (path_tp a0 a1 p p_tp δ0_p δ1_p) = p := by + dsimp [unpath, path] rw [toCoreAsSmallEquiv.symm_apply_eq] rw! (transparency := .default) [toCoreAsSmallEquiv.apply_symm_apply] - apply FunctorOperation.Path.path_unPath - · simp [FunctorOperation.Path.unPath0, ← toCoreAsSmallEquiv_apply_comp_left, ← δ0_p] + apply FunctorOperation.Path.unpath_path + · simp [FunctorOperation.Path.path0, ← toCoreAsSmallEquiv_apply_comp_left, ← δ0_p] rfl - · simp [FunctorOperation.Path.unPath1, ← toCoreAsSmallEquiv_apply_comp_left, ← δ1_p] + · simp [FunctorOperation.Path.path1, ← toCoreAsSmallEquiv_apply_comp_left, ← δ1_p] rfl namespace hurewiczUTp @@ -896,18 +896,18 @@ end UId open UId hurewiczUTp -def UPath : GroupoidModel.U.{v}.Path cylinder where - Id := Id - Id_comp := Id_comp - unPath := unPath - unPath_comp := unPath_comp - unPath_tp := unPath_tp +def UPath : GroupoidModel.U.{v}.PathType cylinder where + Path := Id + Path_comp := Id_comp path := path + path_comp := path_comp path_tp := path_tp - δ0_path := δ0_path - δ1_path := δ1_path - path_unPath := path_unPath - unPath_path := unPath_path + unpath := unpath + unpath_tp := unpath_tp + δ0_unpath := δ0_unpath + δ1_unpath := δ1_unpath + unpath_path := unpath_path + path_unpath := path_unpath def hurewiczUTp : cylinder.Hurewicz U.{v}.tp where lift := lift diff --git a/HoTTLean/Model/Unstructured/Hurewicz.lean b/HoTTLean/Model/Unstructured/Hurewicz.lean index e2c5acb8..e3d2f1fb 100644 --- a/HoTTLean/Model/Unstructured/Hurewicz.lean +++ b/HoTTLean/Model/Unstructured/Hurewicz.lean @@ -210,9 +210,9 @@ Unlike the original, this formulation does not require an object `I`, exponentia or the presence of any limits (other than a terminal object and chosen pullbacks of the classifier) on the category of contexts. -`Id` constructs the identity type, +`Path` constructs the identity type, `unPath` and `path` form a natural (as in stable under precomposition) -bijection between terms of `Γ ⊢ e : Id_A (a,b)` +bijection between terms of `Γ ⊢ e : Path_A (a,b)` ``` e Γ ------> Tm @@ -221,7 +221,7 @@ bijection between terms of `Γ ⊢ e : Id_A (a,b)` ‖ | ‖ V Γ ------> Ty - Id_A(a,b) + Path_A(a,b) ``` and "cubical paths" `(i:I);Γ ⊢ p i : A` such that `p 0 = a` and `p 1 = b` ``` @@ -235,128 +235,128 @@ V V A ``` -/ -structure Path (U : UnstructuredUniverse Ctx) where - (Id : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm), (a0 ≫ U.tp = A) → a1 ≫ U.tp = A → +structure PathType (U : UnstructuredUniverse Ctx) where + (Path : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm), (a0 ≫ U.tp = A) → a1 ≫ U.tp = A → (Γ ⟶ U.Ty)) - (Id_comp : ∀ {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) + (Path_comp : ∀ {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (a0_tp : a0 ≫ U.tp = A) (a1_tp : a1 ≫ U.tp = A), - Id (A := σ ≫ A) (σ ≫ a0) (σ ≫ a1) (by simp [a0_tp]) (by simp [a1_tp]) = - σ ≫ Id a0 a1 a0_tp a1_tp) - (unPath : ∀ {Γ} {A : Γ ⟶ U.Ty} (p : cyl.I.obj Γ ⟶ U.Tm), + Path (A := σ ≫ A) (σ ≫ a0) (σ ≫ a1) (by simp [a0_tp]) (by simp [a1_tp]) = + σ ≫ Path a0 a1 a0_tp a1_tp) + (path : ∀ {Γ} {A : Γ ⟶ U.Ty} (p : cyl.I.obj Γ ⟶ U.Tm), p ≫ U.tp = cyl.π.app Γ ≫ A → (Γ ⟶ U.Tm)) - (unPath_comp : ∀ {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U.Ty} + (path_comp : ∀ {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U.Ty} (p : cyl.I.obj Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = cyl.π.app Γ ≫ A), - unPath (A := σ ≫ A) ((cyl.I.map σ) ≫ p) (by simp [p_tp]) = - σ ≫ unPath p p_tp) - (unPath_tp : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (p : cyl.I.obj Γ ⟶ U.Tm) + path (A := σ ≫ A) ((cyl.I.map σ) ≫ p) (by simp [p_tp]) = + σ ≫ path p p_tp) + (path_tp : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (p : cyl.I.obj Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = cyl.π.app Γ ≫ A) (δ0_p : cyl.δ0.app Γ ≫ p = a0) - (δ1_p : cyl.δ1.app Γ ≫ p = a1), unPath p p_tp ≫ U.tp = - Id (A := A) a0 a1 (by simp [← δ0_p, p_tp]) (by simp [← δ1_p, p_tp])) - (path : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (a0_tp : a0 ≫ U.tp = A) + (δ1_p : cyl.δ1.app Γ ≫ p = a1), path p p_tp ≫ U.tp = + Path (A := A) a0 a1 (by simp [← δ0_p, p_tp]) (by simp [← δ1_p, p_tp])) + (unpath : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (a0_tp : a0 ≫ U.tp = A) (a1_tp : a1 ≫ U.tp = A) (p : Γ ⟶ U.Tm), p ≫ U.tp = - Id a0 a1 a0_tp a1_tp → (cyl.I.obj Γ ⟶ U.Tm)) - (path_tp : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (a0_tp : a0 ≫ U.tp = A) - (a1_tp : a1 ≫ U.tp = A) (p : Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = Id a0 a1 a0_tp a1_tp), - path a0 a1 a0_tp a1_tp p p_tp ≫ U.tp = cyl.π.app _ ≫ A) - (δ0_path : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (a0_tp : a0 ≫ U.tp = A) - (a1_tp : a1 ≫ U.tp = A) (p : Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = Id a0 a1 a0_tp a1_tp), - cyl.δ0.app _ ≫ path a0 a1 a0_tp a1_tp p p_tp = a0) - (δ1_path : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (a0_tp : a0 ≫ U.tp = A) - (a1_tp : a1 ≫ U.tp = A) (p : Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = Id a0 a1 a0_tp a1_tp), - cyl.δ1.app _ ≫ path a0 a1 a0_tp a1_tp p p_tp = a1) - (path_unPath : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (p : cyl.I.obj Γ ⟶ U.Tm) + Path a0 a1 a0_tp a1_tp → (cyl.I.obj Γ ⟶ U.Tm)) + (unpath_tp : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (a0_tp : a0 ≫ U.tp = A) + (a1_tp : a1 ≫ U.tp = A) (p : Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = Path a0 a1 a0_tp a1_tp), + unpath a0 a1 a0_tp a1_tp p p_tp ≫ U.tp = cyl.π.app _ ≫ A) + (δ0_unpath : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (a0_tp : a0 ≫ U.tp = A) + (a1_tp : a1 ≫ U.tp = A) (p : Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = Path a0 a1 a0_tp a1_tp), + cyl.δ0.app _ ≫ unpath a0 a1 a0_tp a1_tp p p_tp = a0) + (δ1_unpath : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (a0_tp : a0 ≫ U.tp = A) + (a1_tp : a1 ≫ U.tp = A) (p : Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = Path a0 a1 a0_tp a1_tp), + cyl.δ1.app _ ≫ unpath a0 a1 a0_tp a1_tp p p_tp = a1) + (unpath_path : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (p : cyl.I.obj Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = cyl.π.app Γ ≫ A) (δ0_p : cyl.δ0.app Γ ≫ p = a0) (δ1_p : cyl.δ1.app Γ ≫ p = a1), - path (A := A) a0 a1 (by simp [← δ0_p, p_tp]) (by simp [← δ1_p, p_tp]) - (unPath p p_tp) (unPath_tp a0 a1 p p_tp δ0_p δ1_p) = p) - (unPath_path : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (a0_tp : a0 ≫ U.tp = A) - (a1_tp : a1 ≫ U.tp = A) (p : Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = Id a0 a1 a0_tp a1_tp), - unPath (A := A) (path a0 a1 a0_tp a1_tp p p_tp) - (path_tp ..) = p) + unpath (A := A) a0 a1 (by simp [← δ0_p, p_tp]) (by simp [← δ1_p, p_tp]) + (path p p_tp) (path_tp a0 a1 p p_tp δ0_p δ1_p) = p) + (path_unpath : ∀ {Γ} {A : Γ ⟶ U.Ty} (a0 a1 : Γ ⟶ U.Tm) (a0_tp : a0 ≫ U.tp = A) + (a1_tp : a1 ≫ U.tp = A) (p : Γ ⟶ U.Tm) (p_tp : p ≫ U.tp = Path a0 a1 a0_tp a1_tp), + path (A := A) (unpath a0 a1 a0_tp a1_tp p p_tp) + (unpath_tp ..) = p) -namespace Path +namespace PathType -variable {cyl} {U0 : UnstructuredUniverse Ctx} (P0 : Path cyl U0) +variable {cyl} {U0 : UnstructuredUniverse Ctx} (P0 : PathType cyl U0) @[reassoc (attr := simp)] -lemma unPath_tp' {Γ} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (p : cyl.I.obj Γ ⟶ U0.Tm) +lemma path_tp' {Γ} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (p : cyl.I.obj Γ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = cyl.π.app Γ ≫ A) (δ0_p : cyl.δ0.app Γ ≫ p = a0) - (δ1_p : cyl.δ1.app Γ ≫ p = a1) : P0.unPath p p_tp ≫ U0.tp = - P0.Id (A := A) a0 a1 (by simp [← δ0_p, p_tp]) (by simp [← δ1_p, p_tp]) := - P0.unPath_tp a0 a1 p p_tp δ0_p δ1_p + (δ1_p : cyl.δ1.app Γ ≫ p = a1) : P0.path p p_tp ≫ U0.tp = + P0.Path (A := A) a0 a1 (by simp [← δ0_p, p_tp]) (by simp [← δ1_p, p_tp]) := + P0.path_tp a0 a1 p p_tp δ0_p δ1_p @[reassoc (attr := simp)] -lemma path_tp' {Γ} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : a0 ≫ U0.tp = A) - (a1_tp : a1 ≫ U0.tp = A) (p : Γ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = P0.Id a0 a1 a0_tp a1_tp) : - P0.path a0 a1 a0_tp a1_tp p p_tp ≫ U0.tp = cyl.π.app _ ≫ A := - path_tp .. +lemma unpath_tp' {Γ} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : a0 ≫ U0.tp = A) + (a1_tp : a1 ≫ U0.tp = A) (p : Γ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = P0.Path a0 a1 a0_tp a1_tp) : + P0.unpath a0 a1 a0_tp a1_tp p p_tp ≫ U0.tp = cyl.π.app _ ≫ A := + unpath_tp .. @[reassoc (attr := simp)] -lemma path_unPath' {Γ} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (p : cyl.I.obj Γ ⟶ U0.Tm) +lemma unpath_path' {Γ} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (p : cyl.I.obj Γ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = cyl.π.app Γ ≫ A) (δ0_p : cyl.δ0.app Γ ≫ p = a0) (δ1_p : cyl.δ1.app Γ ≫ p = a1) : - P0.path (A := A) a0 (a1) (by simp [← δ0_p, p_tp]) (by simp [← δ1_p, p_tp]) - (P0.unPath p p_tp) (P0.unPath_tp a0 a1 p p_tp δ0_p δ1_p) = p := - P0.path_unPath a0 a1 p p_tp δ0_p δ1_p + P0.unpath (A := A) a0 (a1) (by simp [← δ0_p, p_tp]) (by simp [← δ1_p, p_tp]) + (P0.path p p_tp) (P0.path_tp a0 a1 p p_tp δ0_p δ1_p) = p := + P0.unpath_path a0 a1 p p_tp δ0_p δ1_p @[reassoc (attr := simp)] -lemma unPath_path' {Γ} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : a0 ≫ U0.tp = A) - (a1_tp : a1 ≫ U0.tp = A) (p : Γ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = P0.Id a0 a1 a0_tp a1_tp) : - P0.unPath (A := A) (P0.path a0 a1 a0_tp a1_tp p p_tp) (P0.path_tp ..) = p := - unPath_path .. +lemma path_unpath' {Γ} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : a0 ≫ U0.tp = A) + (a1_tp : a1 ≫ U0.tp = A) (p : Γ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = P0.Path a0 a1 a0_tp a1_tp) : + P0.path (A := A) (P0.unpath a0 a1 a0_tp a1_tp p p_tp) (P0.unpath_tp ..) = p := + path_unpath .. @[reassoc (attr := simp)] -lemma δ0_path' {Γ} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : a0 ≫ U0.tp = A) - (a1_tp : a1 ≫ U0.tp = A) (p : Γ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = P0.Id a0 a1 a0_tp a1_tp) : - cyl.δ0.app _ ≫ P0.path a0 a1 a0_tp a1_tp p p_tp = a0 := - δ0_path .. +lemma δ0_unpath' {Γ} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : a0 ≫ U0.tp = A) + (a1_tp : a1 ≫ U0.tp = A) (p : Γ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = P0.Path a0 a1 a0_tp a1_tp) : + cyl.δ0.app _ ≫ P0.unpath a0 a1 a0_tp a1_tp p p_tp = a0 := + δ0_unpath .. @[reassoc (attr := simp)] -lemma δ1_path' {Γ} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : a0 ≫ U0.tp = A) - (a1_tp : a1 ≫ U0.tp = A) (p : Γ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = P0.Id a0 a1 a0_tp a1_tp) : - cyl.δ1.app _ ≫ P0.path a0 a1 a0_tp a1_tp p p_tp = a1 := - δ1_path .. +lemma δ1_unpath' {Γ} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : a0 ≫ U0.tp = A) + (a1_tp : a1 ≫ U0.tp = A) (p : Γ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = P0.Path a0 a1 a0_tp a1_tp) : + cyl.δ1.app _ ≫ P0.unpath a0 a1 a0_tp a1_tp p p_tp = a1 := + δ1_unpath .. -lemma path_ext {Γ} (A : Γ ⟶ U0.Ty) (a0 a1 : Γ ⟶ U0.Tm) (p1 p2 : cyl.I.obj Γ ⟶ U0.Tm) +lemma unpath_ext {Γ} (A : Γ ⟶ U0.Ty) (a0 a1 : Γ ⟶ U0.Tm) (p1 p2 : cyl.I.obj Γ ⟶ U0.Tm) (p1_tp : p1 ≫ U0.tp = cyl.π.app Γ ≫ A) (p2_tp : p2 ≫ U0.tp = cyl.π.app Γ ≫ A) - (h : P0.unPath p1 p1_tp = P0.unPath p2 p2_tp) + (h : P0.path p1 p1_tp = P0.path p2 p2_tp) (δ0_p1 : cyl.δ0.app Γ ≫ p1 = a0) (δ1_p1 : cyl.δ1.app Γ ≫ p1 = a1) (δ0_p2 : cyl.δ0.app Γ ≫ p2 = a0) (δ1_p2 : cyl.δ1.app Γ ≫ p2 = a1) : p1 = p2 := by - rw [← P0.path_unPath (A := A) a0 a1 p1 p1_tp δ0_p1 δ1_p1] - rw [← P0.path_unPath a0 a1 p2 p2_tp δ0_p2 δ1_p2] + rw [← P0.unpath_path (A := A) a0 a1 p1 p1_tp δ0_p1 δ1_p1] + rw [← P0.unpath_path a0 a1 p2 p2_tp δ0_p2 δ1_p2] rw! [h] -lemma path_comp {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : a0 ≫ U0.tp = A) - (a1_tp : a1 ≫ U0.tp = A) (p : Γ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = P0.Id a0 a1 a0_tp a1_tp) : - P0.path (A := σ ≫ A) (σ ≫ a0) (σ ≫ a1) (by simp [a0_tp]) (by simp [a1_tp]) (σ ≫ p) - (by simp [p_tp, ← Id_comp]) = cyl.I.map σ ≫ P0.path a0 a1 a0_tp a1_tp p p_tp := by - apply P0.path_ext (σ ≫ A) (σ ≫ a0) (σ ≫ a1) <;> simp [unPath_comp, δ0_naturality_assoc, +lemma unpath_comp {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : a0 ≫ U0.tp = A) + (a1_tp : a1 ≫ U0.tp = A) (p : Γ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = P0.Path a0 a1 a0_tp a1_tp) : + P0.unpath (A := σ ≫ A) (σ ≫ a0) (σ ≫ a1) (by simp [a0_tp]) (by simp [a1_tp]) (σ ≫ p) + (by simp [p_tp, ← Path_comp]) = cyl.I.map σ ≫ P0.unpath a0 a1 a0_tp a1_tp p p_tp := by + apply P0.unpath_ext (σ ≫ A) (σ ≫ a0) (σ ≫ a1) <;> simp [path_comp, δ0_naturality_assoc, δ1_naturality_assoc] -/-- An alternative version of `unPath` that allows the domain context to be any context `Δ`, +/-- An alternative version of `path` that allows the domain context to be any context `Δ`, not just the context `Γ`. -/ @[simp] -abbrev unPath' {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (p : cyl.I.obj Δ ⟶ U0.Tm) +abbrev path' {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (p : cyl.I.obj Δ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = cyl.π.app Δ ≫ σ ≫ A) : Δ ⟶ U0.Tm := - P0.unPath (A := σ ≫ A) p p_tp + P0.path (A := σ ≫ A) p p_tp -/-- An alternative version of `path` that allows the domain context to be any context `Δ`, +/-- An alternative version of `unpath` that allows the domain context to be any context `Δ`, not just the context `Γ`. -/ @[simp] -abbrev path' {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : a0 ≫ U0.tp = A) - (a1_tp : a1 ≫ U0.tp = A) (p : Δ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = σ ≫ P0.Id a0 a1 a0_tp a1_tp) : +abbrev unpath' {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : a0 ≫ U0.tp = A) + (a1_tp : a1 ≫ U0.tp = A) (p : Δ ⟶ U0.Tm) (p_tp : p ≫ U0.tp = σ ≫ P0.Path a0 a1 a0_tp a1_tp) : cyl.I.obj Δ ⟶ U0.Tm := - P0.path (A := σ ≫ A) (σ ≫ a0) (σ ≫ a1) (by simp [a0_tp]) (by simp [a1_tp]) p - (by simp [p_tp, ← Id_comp]) + P0.unpath (A := σ ≫ A) (σ ≫ a0) (σ ≫ a1) (by simp [a0_tp]) (by simp [a1_tp]) p + (by simp [p_tp, ← Path_comp]) -/-- `Path` identity types give rise to +/-- Path types give rise to formation and introduction rules for traditional HoTT identity types. -/ @[simps] def polymorphicIdIntro : PolymorphicIdIntro U0 U0 where - Id := P0.Id - Id_comp := P0.Id_comp - refl {_ A} a a_tp := P0.unPath (A := A) (cyl.π.app _ ≫ a) (by simp [a_tp]) - refl_comp σ A a a_tp := by simp [← unPath_comp, a_tp] + Id := P0.Path + Id_comp := P0.Path_comp + refl {_ A} a a_tp := P0.path (A := A) (cyl.π.app _ ≫ a) (by simp [a_tp]) + refl_comp σ A a a_tp := by simp [← path_comp, a_tp] refl_tp a a_tp := by simp open PolymorphicIdIntro @@ -369,8 +369,8 @@ variable (hrwcz0 : Hurewicz cyl U0.tp) {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ `(i : I);(x : A).(p : Id(a,x)) ⊢ p' i : A`, satisfying equations `p' 0 = a` and `p' 1 = x`, proven in `δ0_substConsEv` and `δ1_substConsEv`. -It can be thought of as the "evaluation" of the path `p` at a point in the interval. -It is defined by taking `path` of the map `var : Γ.(x:A).Id(a,x) ⟶ Tm` +It can be thought of as the "evaluation" of the unpath `p` at a point in the interval. +It is defined by taking `unpath` of the map `var : Γ.(x:A).Id(a,x) ⟶ Tm` ``` var @@ -396,7 +396,7 @@ I;(Γ.(x:A).Id(a,x) ---> Tm -/ @[simp] abbrev ev : cyl.I.obj (U0.ext (P0.polymorphicIdIntro.weakenId a a_tp)) ⟶ U0.Tm := - P0.path' (A := disp .. ≫ A) (disp ..) (disp .. ≫ a) (var ..) + P0.unpath' (A := disp .. ≫ A) (disp ..) (disp .. ≫ a) (var ..) (by cat_disch) (by simp) (var ..) (by simp) /- @@ -423,9 +423,9 @@ lemma substConsEv_disp : P0.substConsEv a a_tp ≫ disp .. = cyl.π.app _ ≫ U0 simp [substConsEv] @[reassoc (attr := simp)] -lemma substConsEv_var : P0.substConsEv a a_tp ≫ var .. = P0.path (A := disp .. ≫ disp .. ≫ A) +lemma substConsEv_var : P0.substConsEv a a_tp ≫ var .. = P0.unpath (A := disp .. ≫ disp .. ≫ A) (U0.disp .. ≫ U0.disp A ≫ a) (U0.disp .. ≫ U0.var A) - (by cat_disch) (by simp) (U0.var ..) (by simp [← Id_comp]) := by + (by cat_disch) (by simp) (U0.var ..) (by simp [← Path_comp]) := by simp [substConsEv] @[reassoc (attr := simp)] @@ -445,19 +445,19 @@ lemma substConsEv_comp_substWk : P0.substConsEv (A := σ ≫ A) (σ ≫ a) (by s U0.substWk σ A = cyl.I.map (U0.substWk (U0.substWk σ A) (weakenId _ a a_tp) _ ((weakenId_comp ..).symm)) ≫ P0.substConsEv a a_tp := by - simp [substConsEv, ← path_comp, substWk] + simp [substConsEv, ← unpath_comp, substWk] @[reassoc] lemma I_map_reflInst_comp_substConsEv : cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫ P0.substConsEv a a_tp = cyl.π.app Γ ≫ U0.sec A a a_tp := by - apply (disp_pullback ..).hom_ext <;> simp [substConsEv, reflInst, ← path_comp, motiveInst] + apply (disp_pullback ..).hom_ext <;> simp [substConsEv, reflInst, ← unpath_comp, motiveInst] /-- An auxiliary definition for `connection`. -/ def connectionLift : cyl.I.obj (P0.polymorphicIdIntro.motiveCtx a a_tp) ⟶ U0.Tm := hrwcz0.lift (disp .. ≫ disp .. ≫ P0.polymorphicIdIntro.refl a a_tp) (P0.substConsEv a a_tp ≫ P0.polymorphicIdIntro.weakenId a a_tp) (by simp only [motiveCtx, polymorphicIdIntro_Id, polymorphicIdIntro_refl, Functor.id_obj, - Category.assoc, δ0_π'_app_assoc, δ1_π'_app_assoc, unPath_tp', ← Id_comp, weakenId] + Category.assoc, δ0_π'_app_assoc, δ1_π'_app_assoc, path_tp', ← Path_comp, weakenId] rw! (transparency := .default) [P0.δ0_substConsEv_assoc a a_tp, P0.δ0_substConsEv_assoc a a_tp, P0.δ0_substConsEv_assoc a a_tp] simp) @@ -472,28 +472,28 @@ lemma connectionLift_comp [hrwcz0.IsUniform] : cyl.I.map (P0.polymorphicIdIntro.motiveSubst σ a a_tp) ≫ P0.connectionLift hrwcz0 a a_tp := by simp only [motiveCtx, polymorphicIdIntro_Id, connectionLift, polymorphicIdIntro_refl, - Functor.id_obj, ← unPath_comp, NatTrans.naturality_assoc, Functor.id_map, weakenId, motiveSubst, + Functor.id_obj, ← path_comp, NatTrans.naturality_assoc, Functor.id_map, weakenId, motiveSubst, ← Hurewicz.lift_comp, substWk_disp_assoc] congr 1 erw [← P0.substConsEv_comp_substWk_assoc] - simp [← Id_comp] + simp [← Path_comp] lemma I_map_reflInst_comp_connectionLift [hrwcz0.IsUniform] [hrwcz0.IsNormal] : cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫ P0.connectionLift hrwcz0 a a_tp = - P0.unPath (A := cyl.π.app Γ ≫ A) (cyl.π.app _ ≫ cyl.π.app Γ ≫ a) (by simp [a_tp]) := by + P0.path (A := cyl.π.app Γ ≫ A) (cyl.π.app _ ≫ cyl.π.app Γ ≫ a) (by simp [a_tp]) := by simp only [connectionLift] rw [← Hurewicz.lift_comp] - rw [hrwcz0.isNormal _ _ _ (U0.sec A a a_tp ≫ P0.Id (A := U0.disp A ≫ A) (U0.disp A ≫ a) + rw [hrwcz0.isNormal _ _ _ (U0.sec A a a_tp ≫ P0.Path (A := U0.disp A ≫ A) (U0.disp A ≫ a) (U0.var A) (by simp [a_tp]) (by simp))] - · simp [← unPath_comp, reflInst, motiveInst] + · simp [← path_comp, reflInst, motiveInst] · simp [I_map_reflInst_comp_substConsEv_assoc] /-- Fix `Γ ⊢ a : A`, we think of `connection` as a cubical (as opposed to globular) homotopy `(i j : I);(x : A)(p : Id(a,x)) ⊢ χ i j : A` -such that `χ 0 j = refl a j` is the reflexive path at `a : A` and `χ 1 j = p j`. +such that `χ 0 j = refl a j` is the reflexive unpath at `a : A` and `χ 1 j = p j`. These are proven below as `δ0_connection` and `δ1_connection` respectively. It will also satisfy `χ i 0 = refl a i`, proven in `I_δ0_connection`. -Note that we do not know how the bottom path `χ i 1` computes. +Note that we do not know how the bottom unpath `χ i 1` computes. ``` i→ j↓ @@ -505,7 +505,7 @@ a -----> p 1 ``` -/ def connection : cyl.I.obj (cyl.I.obj (P0.polymorphicIdIntro.motiveCtx a a_tp)) ⟶ U0.Tm := - P0.path' (A := disp .. ≫ A) (substConsEv ..) (disp .. ≫ a) (var ..) (by simp [a_tp]) + P0.unpath' (A := disp .. ≫ A) (substConsEv ..) (disp .. ≫ a) (var ..) (by simp [a_tp]) (by simp) (P0.connectionLift hrwcz0 a a_tp) (by simp [connectionLift]) @[simp] @@ -523,15 +523,15 @@ lemma δ0_connection : cyl.δ0.app _ ≫ P0.connection hrwcz0 a a_tp = @[reassoc (attr := simp)] lemma δ1_connection : cyl.δ1.app _ ≫ P0.connection hrwcz0 a a_tp = P0.ev a a_tp := by - simp [connection, path', δ1_path', ev] + simp [connection, unpath', δ1_unpath', ev] @[simp] lemma I_δ0_connection : cyl.I.map (cyl.δ0.app _) ≫ P0.connection hrwcz0 a a_tp = cyl.π.app _ ≫ disp .. ≫ U0.disp A ≫ a := by - fapply P0.path_ext (disp .. ≫ U0.disp A ≫ A) (disp .. ≫ U0.disp A ≫ a) (disp .. ≫ U0.disp A ≫ a) - <;> simp [a_tp, connection, ← path_comp] + fapply P0.unpath_ext (disp .. ≫ U0.disp A ≫ A) (disp .. ≫ U0.disp A ≫ a) (disp .. ≫ U0.disp A ≫ a) + <;> simp [a_tp, connection, ← unpath_comp] erw [δ0_connectionLift] -- FIXME - simp [← unPath_comp] + simp [← path_comp] lemma connection_comp [hrwcz0.IsUniform] : P0.connection hrwcz0 (A := σ ≫ A) (σ ≫ a) (by simp [a_tp]) = @@ -539,17 +539,17 @@ lemma connection_comp [hrwcz0.IsUniform] : P0.connection hrwcz0 (a) a_tp := by simp only [connection] rw! [connectionLift_comp _ _ _ _ a_tp] - simp [← path_comp, motiveSubst] + simp [← unpath_comp, motiveSubst] lemma I_map_I_map_reflInst_comp_connection [hrwcz0.IsUniform] [hrwcz0.IsNormal] : cyl.I.map (cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp)) ≫ P0.connection hrwcz0 a a_tp = cyl.π.app (cyl.I.obj Γ) ≫ cyl.π.app Γ ≫ a := by - simp only [connection, path'] - fapply P0.path_ext + simp only [connection, unpath'] + fapply P0.unpath_ext (cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫ P0.substConsEv a a_tp ≫ U0.disp A ≫ A) (cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫ P0.substConsEv a a_tp ≫ U0.disp A ≫ a) (cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫ P0.substConsEv a a_tp ≫ U0.var A) - <;> simp [a_tp, ← path_comp, reflInst, motiveInst] + <;> simp [a_tp, ← unpath_comp, reflInst, motiveInst] erw [I_map_reflInst_comp_connectionLift] /-- `symmConnection` is the symmetrically flipped homotopy `j i ⊢ χ i j` (of `connection`), @@ -564,10 +564,10 @@ a ====== a p 0 ----> p 1 p j ``` -Note that we know the left path is `χ i 0 = refl a i` -but we do not know how the right path `χ i 1` computes. +Note that we know the left unpath is `χ i 0 = refl a i` +but we do not know how the right unpath `χ i 1` computes. We need to switch the indices using `cyl.symm` since -1. we need to do path lifting in the `j` direction (i.e. starting at `χ i 0 = refl a i`) +1. we need to do unpath lifting in the `j` direction (i.e. starting at `χ i 0 = refl a i`) 2. we ultimately want a homotopy in the `i` direction (i.e. from `χ 0 j` to `χ 1 j`) -/ def symmConnection := cyl.symm.app _ ≫ P0.connection hrwcz0 a a_tp @@ -617,46 +617,46 @@ lemma symmConnection_comp [hrwcz0.IsUniform] : simp [symmConnection, connection_comp _ _ _ _ a_tp, ← this] /-- An auxiliary definition for `substConnection`. -/ -def unPathSymmConnection : cyl.I.obj (U0.ext (P0.polymorphicIdIntro.weakenId a a_tp)) ⟶ U0.Tm := - P0.unPath (Γ := cyl.I.obj (P0.polymorphicIdIntro.motiveCtx a a_tp)) +def pathSymmConnection : cyl.I.obj (U0.ext (P0.polymorphicIdIntro.weakenId a a_tp)) ⟶ U0.Tm := + P0.path (Γ := cyl.I.obj (P0.polymorphicIdIntro.motiveCtx a a_tp)) (A := cyl.π.app _ ≫ disp .. ≫ disp .. ≫ A) (P0.symmConnection hrwcz0 a a_tp) (by simp) @[simp] -lemma unPathSymmConnection_tp : P0.unPathSymmConnection hrwcz0 a a_tp ≫ U0.tp = - P0.Id (A := cyl.π.app _ ≫ disp .. ≫ disp .. ≫ A) +lemma pathSymmConnection_tp : P0.pathSymmConnection hrwcz0 a a_tp ≫ U0.tp = + P0.Path (A := cyl.π.app _ ≫ disp .. ≫ disp .. ≫ A) (cyl.π.app _ ≫ disp .. ≫ disp .. ≫ a) (cyl.δ1.app _ ≫ P0.symmConnection hrwcz0 a a_tp) (by simp [a_tp]) (by simp) := by - simp [unPathSymmConnection] + simp [pathSymmConnection] rw! (transparency := .default) [δ0_symmConnection] congr 1 @[simp] -lemma δ0_unPathSymmConnection : cyl.δ0.app _ ≫ P0.unPathSymmConnection hrwcz0 a a_tp = +lemma δ0_pathSymmConnection : cyl.δ0.app _ ≫ P0.pathSymmConnection hrwcz0 a a_tp = disp .. ≫ disp .. ≫ P0.polymorphicIdIntro.refl a a_tp := by - simp only [polymorphicIdIntro_Id, Functor.id_obj, unPathSymmConnection, motiveCtx, ← unPath_comp, + simp only [polymorphicIdIntro_Id, Functor.id_obj, pathSymmConnection, motiveCtx, ← path_comp, δ0_π'_app_assoc, polymorphicIdIntro_refl, NatTrans.naturality_assoc, Functor.id_map] rw! (transparency := .default) [I_δ0_symmConnection] simp @[simp] -lemma δ1_unPathSymmConnection : cyl.δ1.app _ ≫ P0.unPathSymmConnection hrwcz0 a a_tp = +lemma δ1_pathSymmConnection : cyl.δ1.app _ ≫ P0.pathSymmConnection hrwcz0 a a_tp = U0.var _ := by - simp only [polymorphicIdIntro_Id, Functor.id_obj, unPathSymmConnection, motiveCtx, ← unPath_comp, + simp only [polymorphicIdIntro_Id, Functor.id_obj, pathSymmConnection, motiveCtx, ← path_comp, δ1_π'_app_assoc] rw! (transparency := .default) [I_δ1_symmConnection] simp -lemma unPathSymmConnection_comp [hrwcz0.IsUniform] : - P0.unPathSymmConnection hrwcz0 (A := σ ≫ A) (σ ≫ a) (by simp [a_tp]) = +lemma pathSymmConnection_comp [hrwcz0.IsUniform] : + P0.pathSymmConnection hrwcz0 (A := σ ≫ A) (σ ≫ a) (by simp [a_tp]) = cyl.I.map (U0.substWk (U0.substWk σ _ _ rfl) _ _ (by rw [weakenId_comp])) ≫ - P0.unPathSymmConnection hrwcz0 a a_tp := by - simp [unPathSymmConnection, ← unPath_comp, symmConnection_comp _ _ _ _ a_tp, motiveSubst] + P0.pathSymmConnection hrwcz0 a a_tp := by + simp [pathSymmConnection, ← path_comp, symmConnection_comp _ _ _ _ a_tp, motiveSubst] -lemma I_map_reflInst_comp_unPathSymmConnection [hrwcz0.IsUniform] [hrwcz0.IsNormal] : - cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫ P0.unPathSymmConnection hrwcz0 a a_tp = - cyl.π.app Γ ≫ P0.unPath (A := A) (cyl.π.app Γ ≫ a) (by simp [a_tp]) := by - simp only [unPathSymmConnection, ← unPath_comp] +lemma I_map_reflInst_comp_pathSymmConnection [hrwcz0.IsUniform] [hrwcz0.IsNormal] : + cyl.I.map (P0.polymorphicIdIntro.reflInst a a_tp) ≫ P0.pathSymmConnection hrwcz0 a a_tp = + cyl.π.app Γ ≫ P0.path (A := A) (cyl.π.app Γ ≫ a) (by simp [a_tp]) := by + simp only [pathSymmConnection, ← path_comp] congr 1 · simp [reflInst, motiveInst] · simp [I_map_I_map_reflInst_comp_symmConnection] @@ -670,19 +670,19 @@ def substConnection : cyl.I.obj (U0.ext ((polymorphicIdIntro P0).weakenId a a_tp P0.polymorphicIdIntro.motiveCtx a a_tp := let χi1 : cyl.I.obj (U0.ext (P0.polymorphicIdIntro.weakenId a a_tp)) ⟶ U0.Tm := (cyl.δ1.app _ ≫ P0.symmConnection hrwcz0 a a_tp) - -- the path `i ⊢ χ i 1 : A` is the endpoint of the homotopy `symmConnection` + -- the unpath `i ⊢ χ i 1 : A` is the endpoint of the homotopy `symmConnection` -- that we cannot compute let toΓ : cyl.I.obj (U0.ext ((polymorphicIdIntro P0).weakenId a a_tp)) ⟶ Γ := cyl.π.app _ ≫ disp .. ≫ disp .. let toExtA : cyl.I.obj (U0.ext ((polymorphicIdIntro P0).weakenId a a_tp)) ⟶ U0.ext A := U0.substCons toΓ A χi1 (by aesop_cat) U0.substCons toExtA (P0.polymorphicIdIntro.weakenId a a_tp) - (P0.unPathSymmConnection hrwcz0 a a_tp) (by - simp [unPathSymmConnection_tp, toExtA, toΓ, χi1, ← Id_comp]) + (P0.pathSymmConnection hrwcz0 a a_tp) (by + simp [pathSymmConnection_tp, toExtA, toΓ, χi1, ← Path_comp]) @[simp] lemma substConnection_var : P0.substConnection hrwcz0 a a_tp ≫ var .. = - P0.unPathSymmConnection hrwcz0 a a_tp := by + P0.pathSymmConnection hrwcz0 a a_tp := by simp [substConnection] @[reassoc (attr := simp)] @@ -690,7 +690,7 @@ lemma δ0_substConnection : cyl.δ0.app _ ≫ P0.substConnection hrwcz0 a a_tp = disp .. ≫ disp .. ≫ reflInst _ a a_tp := by simp only [polymorphicIdIntro_Id, Functor.id_obj, motiveCtx, substConnection, comp_substCons, δ0_π'_app_assoc, ← cyl.δ1_naturality_assoc, polymorphicIdIntro_refl] - rw! (transparency := .default) [δ0_unPathSymmConnection] + rw! (transparency := .default) [δ0_pathSymmConnection] apply (disp_pullback ..).hom_ext · simp · apply (disp_pullback ..).hom_ext @@ -704,7 +704,7 @@ lemma δ1_substConnection : cyl.δ1.app _ ≫ P0.substConnection hrwcz0 a a_tp = simp [substConnection] apply (disp_pullback ..).hom_ext · simp only [substCons_var, Category.id_comp] - rw! (transparency := .default) [δ1_unPathSymmConnection] + rw! (transparency := .default) [δ1_pathSymmConnection] simp · apply (disp_pullback ..).hom_ext · simp only [symmConnection, motiveCtx, polymorphicIdIntro_Id, Functor.comp_obj, @@ -721,7 +721,7 @@ lemma substConnection_comp_motiveSubst [hrwcz0.IsUniform] : apply (disp_pullback ..).hom_ext · simp only [Category.assoc, substWk_var] erw [substConnection_var] - simp [substConnection, unPathSymmConnection_comp _ _ _ _ a_tp] + simp [substConnection, pathSymmConnection_comp _ _ _ _ a_tp] · apply (disp_pullback ..).hom_ext · simp [substConnection, symmConnection_comp _ _ _ _ a_tp, δ1_naturality_assoc, motiveSubst] · simp [substConnection] @@ -733,7 +733,7 @@ lemma reflInst_comp_substConnection [hrwcz0.IsUniform] [hrwcz0.IsNormal] : P0.substConnection hrwcz0 a a_tp = cyl.π.app _ ≫ reflInst _ a a_tp := by simp only [substConnection] apply (disp_pullback ..).hom_ext - · simp [I_map_reflInst_comp_unPathSymmConnection] + · simp [I_map_reflInst_comp_pathSymmConnection] · apply (disp_pullback ..).hom_ext · simp [← δ1_naturality_assoc, I_map_I_map_reflInst_comp_symmConnection] · simp [reflInst, motiveInst] @@ -770,4 +770,4 @@ def polymorphicIdElim (hrwcz0 : Hurewicz cyl U0.tp) [hrwcz0.IsUniform] [hrwcz0.I rw [reflInst_comp_substConnection_assoc] _ = c := by simp [reflInst, motiveInst] -end Path +end PathType