feat: Groupoid model identity and Pi types

HoTTLean/ForMathlib.lean

@@ -583,4 +583,97 @@ theorem comp_heq_of_heq_id {A B : Type u} {C : Type*} [Category.{v} A] [Category
 
 end Functor
 
+lemma eqToHom_heq_id {C : Type*} [Category C] (x y z : C) (h : x = y)
+    (hz : z = x) : eqToHom h ≍ 𝟙 z := by cat_disch
+
+lemma Cat.inv_heq_inv {C C' : Cat} (hC : C ≍ C') {X Y : C} {X' Y' : C'}
+    (hX : X ≍ X') (hY : Y ≍ Y') {f : X ⟶ Y} {f' : X' ⟶ Y'} (hf : f ≍ f') [IsIso f] :
+    have : IsIso f' := by aesop
+    inv f ≍ inv f' := by
+  subst hC hX hY hf
+  rfl
+
+lemma inv_heq_of_heq_inv {C : Grpd} {X Y X' Y' : C}
+    (hX : X = X') (hY : Y = Y') {f : X ⟶ Y} {g : Y' ⟶ X'} (hf : f ≍ inv g) :
+    inv f ≍ g := by
+  aesop_cat
+
+lemma inv_heq_inv {C : Type*} [Category C] {X Y : C} {X' Y' : C}
+    (hX : X = X') (hY : Y = Y') {f : X ⟶ Y} {f' : X' ⟶ Y'} (hf : f ≍ f') [IsIso f] :
+    have : IsIso f' := by aesop
+    inv f ≍ inv f' := by
+  subst hX hY hf
+  rfl
+
+lemma Discrete.as_heq_as {α α' : Type u} (hα : α ≍ α') (x : Discrete α) (x' : Discrete α')
+    (hx : x ≍ x') : x.as ≍ x'.as := by
+  aesop_cat
+
+lemma Discrete.functor_ext' {X C : Type*} [Category C] {F G : X → C} (h : ∀ x : X, F x = G x) :
+    Discrete.functor F = Discrete.functor G := by
+  have : F = G := by aesop
+  subst this
+  rfl
+
+lemma Discrete.functor_eq {X C : Type*} [Category C] {F : Discrete X ⥤ C} :
+    F = Discrete.functor fun x ↦ F.obj ⟨x⟩ := by
+  fapply CategoryTheory.Functor.ext
+  · aesop
+  · intro x y f
+    cases x ; rcases f with ⟨⟨h⟩⟩
+    cases h
+    simp
+
+lemma Discrete.functor_ext {X C : Type*} [Category C] (F G : Discrete X ⥤ C)
+    (h : ∀ x : X, F.obj ⟨x⟩ = G.obj ⟨x⟩) :
+    F = G :=
+  calc F
+    _ = Discrete.functor (fun x => F.obj ⟨x⟩) := Discrete.functor_eq
+    _ = Discrete.functor (fun x => G.obj ⟨x⟩) := Discrete.functor_ext' h
+    _ = G := Discrete.functor_eq.symm
+
+lemma Discrete.hext {X Y : Type u} (a : Discrete X) (b : Discrete Y) (hXY : X ≍ Y)
+    (hab : a.1 ≍ b.1) : a ≍ b := by
+  aesop_cat
+
+lemma Discrete.Hom.hext {α β : Type u} {x y : Discrete α} (x' y' : Discrete β) (hαβ : α ≍ β)
+    (hx : x ≍ x') (hy : y ≍ y') (f : x ⟶ y) (f' : x' ⟶ y') : f ≍ f' := by
+  aesop_cat
+
+open Prod in
+lemma Prod.sectR_comp_snd {C : Type u₁} [Category.{v₁} C] (Z : C)
+    (D : Type u₂) [Category.{v₂} D] : sectR Z D ⋙ snd C D = 𝟭 D :=
+  rfl
+
+section
+variable {C : Type u} [Category.{v} C] {D : Type u₁} [Category.{v₁} D] (P Q : ObjectProperty D)
+  (F : C ⥤ D) (hF : ∀ X, P (F.obj X))
+
+theorem ObjectProperty.lift_comp_inclusion_eq :
+    P.lift F hF ⋙ P.ι = F :=
+  rfl
+
+end
+
+lemma eqToHom_heq_eqToHom {C : Type*} [Category C] (x y x' y' : C) (hx : x = x')
+    (h : x = y) (h' : x' = y') : eqToHom h ≍ eqToHom h' := by aesop
+
 end CategoryTheory
+
+lemma hcongr_fun {α α' : Type u} (hα : α ≍ α') (β : α → Type v) (β' : α' → Type v) (hβ : β ≍ β')
+    (f : (x : α) → β x) (f' : (x : α') → β' x) (hf : f ≍ f')
+    {x : α} {x' : α'} (hx : x ≍ x') : f x ≍ f' x' := by
+  subst hα hβ hf hx
+  rfl
+
+lemma fun_hext {α α' : Type u} (hα : α ≍ α') (β : α → Type v) (β' : α' → Type v) (hβ : β ≍ β')
+    (f : (x : α) → β x) (f' : (x : α') → β' x)
+    (hf : {x : α} → {x' : α'} → (hx : x ≍ x') → f x ≍ f' x') : f ≍ f' := by
+  aesop
+
+lemma Subtype.hext {α α' : Sort u} (hα : α ≍ α') {p : α → Prop} {p' : α' → Prop}
+    (hp : p ≍ p') {a : { x // p x }} {a' : { x // p' x }} (ha : a.1 ≍ a'.1) : a ≍ a' := by
+  subst hα hp
+  simp only [heq_eq_eq]
+  ext
+  simpa [← heq_eq_eq]

HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean

@@ -585,6 +585,43 @@ def toTransport_fiber (x : ∫ F) {c : C} (t : x.base ⟶ c) :
     (toTransport x t).fiber = 𝟙 _ :=
   rfl
 
+lemma transport_id {x : ∫ F} :
+    transport x (𝟙 x.base) = x := by
+  fapply Grothendieck.ext <;> simp [transport]
+
+lemma transport_eqToHom {X: C} {X' : ∫ F} (hX': (forget F).obj X' = X):
+    X'.transport (eqToHom hX') = X' := by
+  subst hX'
+  simp [transport_id]
+
+lemma toTransport_id {X : ∫ F} :
+    toTransport X (𝟙 X.base) = eqToHom transport_id.symm := by
+  apply Grothendieck.Hom.ext <;> simp
+
+lemma toTransport_eqToHom {X: C} {X' : ∫ F} (hX': (forget F).obj X' = X):
+    toTransport X' (eqToHom hX') = eqToHom (by subst hX'; simp[transport_id]) := by
+  subst hX'
+  simp [toTransport_id]
+
+lemma transport_comp (x : ∫ F) {c d: C} (t : x.base ⟶ c) (t': c ⟶ d):
+      transport x (t ≫ t') = transport (c:= d) (transport x t) t' := by
+  simp [transport]
+
+lemma toTransport_comp (x : ∫ F) {c d: C} (t : x.base ⟶ c) (t': c ⟶ d):
+    toTransport x (t ≫ t') =
+    toTransport x t ≫ toTransport (transport x t) t' ≫ eqToHom (transport_comp x t t').symm := by
+  simp only [← Category.assoc, ← heq_eq_eq, heq_comp_eqToHom_iff]
+  simp only [toTransport, transport_base, transport_fiber]
+  fapply Grothendieck.Hom.hext'
+  · rfl
+  · rfl
+  · simp [transport_comp]
+  · simp
+  · simp only [transport_base, Hom.mk_base, transport_fiber, Hom.comp_base, Hom.comp_fiber, map_id,
+      Category.comp_id]
+    symm
+    apply eqToHom_heq_id_dom
+
 /--
 Construct an isomorphism in a Grothendieck construction from isomorphisms in its base and fiber.
 -/
@@ -851,6 +888,14 @@ lemma toPseudoFunctor'Iso.inv_comp_forget : toPseudoFunctor'Iso.inv F ⋙ forget
     Pseudofunctor.Grothendieck.forget _ :=
   rfl
 
+lemma map_eq_pseudofunctor_map {G} (α : F ⟶ G) : map α = (toPseudoFunctor'Iso F).hom ⋙
+    Pseudofunctor.Grothendieck.map α.toStrongTrans' ⋙
+    (toPseudoFunctor'Iso G).inv := by
+  fapply Functor.ext
+  · aesop
+  · intro _
+    aesop
+
 end Pseudofunctor
 
 section
@@ -1146,7 +1191,7 @@ include hom_id in
 lemma functorFromCompHom_id (c : C) : functorFromCompHom fib hom G (𝟙 c)
     = eqToHom (by simp [Cat.id_eq_id, Functor.id_comp]) := by
   ext x
-  simp [hom_id, functorFromCompHom]
+  simp [hom_id, eqToHom_map, functorFromCompHom]
 
 include hom_comp in
 lemma functorFromCompHom_comp (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃):
@@ -1155,7 +1200,7 @@ lemma functorFromCompHom_comp (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂
     Functor.whiskerLeft (F.map f) (functorFromCompHom fib hom G g) ≫
     eqToHom (by simp[Cat.comp_eq_comp, Functor.map_comp, Functor.assoc]) := by
   ext
-  simp [functorFromCompHom, hom_comp]
+  simp [functorFromCompHom, hom_comp, eqToHom_map]
 
 theorem functorFrom_comp : functorFrom fib hom hom_id hom_comp ⋙ G =
     functorFrom (functorFromCompFib fib G) (functorFromCompHom fib hom G)
@@ -1390,6 +1435,55 @@ def mapWhiskerRightAsSmallFunctor (α : F ⟶ G) :
 
 end AsSmall
 
+noncomputable section
+
+variable {F} {x y : ∫ F} (f : x ⟶ y) [IsIso f]
+
+instance : IsIso f.base := by
+  refine ⟨ (CategoryTheory.inv f).base , ?_, ?_ ⟩
+  · simp [← Grothendieck.Hom.comp_base]
+  · simp [← Grothendieck.Hom.comp_base]
+
+def invFiber : y.fiber ⟶ (F.map f.base).obj x.fiber :=
+  eqToHom (by simp [← Functor.comp_obj, ← Cat.comp_eq_comp, ← Functor.map_comp,
+      ← Grothendieck.Hom.comp_base]) ≫
+    (F.map f.base).map (CategoryTheory.inv f).fiber
+
+@[simp]
+lemma fiber_comp_invFiber : f.fiber ≫ invFiber f = 𝟙 ((F.map f.base).obj x.fiber) := by
+  have h := Functor.Grothendieck.Hom.comp_fiber f (CategoryTheory.inv f)
+  rw! [IsIso.hom_inv_id] at h
+  have h0 : F.map (CategoryTheory.inv f).base ⋙ F.map f.base = 𝟭 _ := by
+    simp [← Cat.comp_eq_comp, ← Functor.map_comp, ← Grothendieck.Hom.comp_base, Cat.id_eq_id]
+  have h1 := Functor.congr_map (F.map f.base) h
+  simp [← heq_eq_eq, eqToHom_map, ← Functor.comp_map, Functor.congr_hom h0] at h1
+  dsimp [invFiber]
+  rw! [← h1]
+  simp
+
+@[simp]
+lemma invFiber_comp_fiber : invFiber f ≫ f.fiber = 𝟙 _ := by
+  have h := Functor.Grothendieck.Hom.comp_fiber (CategoryTheory.inv f) f
+  rw! [IsIso.inv_hom_id] at h
+  simp [invFiber]
+  convert h.symm
+  · simp
+  · simp
+  · simpa using (eqToHom_heq_id_cod _ _ _).symm
+
+instance : IsIso f.fiber :=
+  ⟨invFiber f , fiber_comp_invFiber f, invFiber_comp_fiber f⟩
+
+lemma inv_base : CategoryTheory.inv f.base = Grothendieck.Hom.base (CategoryTheory.inv f) := by
+  apply IsIso.inv_eq_of_hom_inv_id
+  simp [← Hom.comp_base]
+
+lemma inv_fiber : CategoryTheory.inv f.fiber = invFiber f := by
+  apply IsIso.inv_eq_of_hom_inv_id
+  simp
+
+end
+
 end Grothendieck
 
 end Functor

HoTTLean/ForMathlib/CategoryTheory/Functor/IsPullback.lean

@@ -480,69 +480,69 @@ def isoIsPullback {P P' X Y Z : Type*} [Category P] [Category P']
     · intro A
       have e : ((h.toChosen ⋙ h'.fromChosen) ⋙ h'.toChosen ⋙ h.fromChosen) =
         (h.toChosen ⋙ (h'.fromChosen ⋙ h'.toChosen) ⋙ h.fromChosen) := by
-        simp[comp]
+        simp [comp]
       simp only[e,from_to_id,Functor.id_comp,to_from_id]
     · intro A B t
       have e : ((h.toChosen ⋙ h'.fromChosen) ⋙ h'.toChosen ⋙ h.fromChosen) =
         (h.toChosen ⋙ (h'.fromChosen ⋙ h'.toChosen) ⋙ h.fromChosen) := by
         simp[comp]
-      rw![e]
-      simp only[← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff]
-      rw[from_to_id,Functor.id_comp,to_from_id]
+      rw! [e]
+      simp only [← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff]
+      rw [from_to_id,Functor.id_comp,to_from_id]
   inv_hom_id := by
     fapply Functor.ext
     · intro A
       have e : ((h'.toChosen ⋙ h.fromChosen) ⋙ h.toChosen ⋙ h'.fromChosen) =
         (h'.toChosen ⋙ (h.fromChosen ⋙ h.toChosen) ⋙ h'.fromChosen) := by
         simp[comp]
-      simp only[e,from_to_id,Functor.id_comp,to_from_id]
+      simp only [e,from_to_id,Functor.id_comp,to_from_id]
     · intro A B t
       have e : ((h'.toChosen ⋙ h.fromChosen) ⋙ h.toChosen ⋙ h'.fromChosen) =
         (h'.toChosen ⋙ (h.fromChosen ⋙ h.toChosen) ⋙ h'.fromChosen) := by
-        simp[comp]
-      rw![e]
+        simp [comp]
+      rw! [e]
       simp only[← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff]
-      rw[from_to_id,Functor.id_comp,to_from_id]
+      rw [from_to_id,Functor.id_comp,to_from_id]
 
 lemma isoIsPullback.inv_comp_left {P P' X Y Z : Type*} [Category P] [Category P']
     [Category X] [Category Y] [Category Z]
     {fst : P ⥤ X} {snd : P ⥤  Y} {f : X ⥤  Z} {g : Y ⥤  Z}
     {fst' : P' ⥤  X} {snd' : P' ⥤ Y} (h : Functor.IsPullback fst snd f g)
     (h' : Functor.IsPullback fst' snd' f g):
     (isoIsPullback h h').inv ⋙ fst = fst' := by
-  dsimp[isoIsPullback]
+  dsimp [isoIsPullback]
   fapply Functor.ext
   · intro A
-    simp only[Functor.assoc,h.from_north]
-    rw[toChosen_north]
+    simp only [Functor.assoc,h.from_north]
+    rw [toChosen_north]
   · intros A B t
-    simp only[← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff]
-    rw![Functor.assoc,h.from_north]
-    rw[toChosen_north]
+    simp only [← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff]
+    rw! [Functor.assoc,h.from_north]
+    rw [toChosen_north]
 
 lemma isoIsPullback.hom_comp_left {P P' X Y Z : Type*} [Category P] [Category P']
     [Category X] [Category Y] [Category Z]
     {fst : P ⥤ X} {snd : P ⥤  Y} {f : X ⥤  Z} {g : Y ⥤  Z}
     {fst' : P' ⥤ X} {snd' : P' ⥤ Y} (h : Functor.IsPullback fst snd f g)
     (h' : Functor.IsPullback fst' snd' f g):
     (isoIsPullback h h').hom ⋙ fst' = fst := by
-  dsimp[isoIsPullback]
+  dsimp [isoIsPullback]
   fapply Functor.ext
   · intro A
-    simp only[Functor.assoc,h'.from_north]
-    rw[toChosen_north]
+    simp only [Functor.assoc,h'.from_north]
+    rw [toChosen_north]
   · intros A B t
-    simp only[← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff]
-    rw![Functor.assoc,h'.from_north]
-    rw[toChosen_north]
+    simp only [← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff]
+    rw! [Functor.assoc,h'.from_north]
+    rw [toChosen_north]
 
 lemma isoIsPullback.hom_comp_left' {P P' X Y Z : Type*} [Category P] [Category P']
     [Category X] [Category Y] [Category Z]
     {fst : P ⥤ X} {snd : P ⥤  Y} {f : X ⥤  Z} {g : Y ⥤  Z}
     {fst' : P' ⥤  X} {snd' : P' ⥤ Y} (h : Functor.IsPullback fst snd f g)
-    (h' : Functor.IsPullback fst' snd' f g) {hom } (e: hom =  (isoIsPullback h h').hom):
+    (h' : Functor.IsPullback fst' snd' f g) {hom } (e: hom = (isoIsPullback h h').hom):
     hom ⋙ fst' = fst := by
-  rw[e]
+  rw [e]
   apply isoIsPullback.hom_comp_left
 
 lemma isoIsPullback.hom_comp_right {P P' X Y Z : Type*} [Category P] [Category P']
@@ -553,29 +553,28 @@ lemma isoIsPullback.hom_comp_right {P P' X Y Z : Type*} [Category P] [Category P
     hom ⋙ snd' = snd := by
   rw[e]
   unfold isoIsPullback
-  simp
   fapply Functor.ext
   · intro A
-    simp only[Functor.assoc,h'.from_west]
+    simp only [Functor.assoc,h'.from_west]
     rw[toChosen_west]
   · intros A B t
-    simp only[← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff]
-    rw![Functor.assoc,h'.from_west]
-    rw[toChosen_west]
+    simp only [← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff]
+    rw! [Functor.assoc,h'.from_west]
+    rw [toChosen_west]
 
-def IsPullbackOfBotId {A A' B : Type*} [Category A] [Category A']
+def ofBotId {A A' B : Type*} [Category A] [Category A']
     [Category B]
     {i : A ≅≅ A'} {F1: A ⥤ B} {F2 : A' ⥤ B}
     (h' : F1 = i.hom ⋙ F2) : IsPullback i.hom F1 F2 (Functor.id B) := by
   fapply ofUniversal
   · aesop
   · intro C inst Cn Cw h
-    simp
+    simp only [Iso.cancel_iso_hom_right, forall_eq', imp_self, implies_true, and_true]
     have hinv : Cn ⋙ i.inv ⋙ i.hom = Cn ∧ Cn ⋙ i.inv ⋙ F1 = Cw := by
       aesop_cat
     exact ⟨ Cn ⋙ i.inv, hinv⟩
   · intro C inst Cn Cw h
-    simp
+    simp only [Iso.cancel_iso_hom_right, forall_eq', imp_self, implies_true, and_true]
     have hinv : Cn ⋙ i.inv ⋙ i.hom = Cn ∧ Cn ⋙ i.inv ⋙ F1 = Cw := by
       aesop_cat
     exact ⟨ Cn ⋙ i.inv, hinv⟩

HoTTLean/ForMathlib/CategoryTheory/Functor/Iso.lean

@@ -1,6 +1,8 @@
 import Mathlib.CategoryTheory.Functor.Category
 import Mathlib.CategoryTheory.Category.ULift
 
+universe v u v₁ u₁ v₂ u₂
+
 namespace CategoryTheory.Functor
 
 structure Iso (C D : Type*) [Category C] [Category D] where
@@ -321,6 +323,30 @@ def toEquivalence (h : X ≅≅ Y) : X ≌ Y where
   counitIso := eqToIso h.inv_hom_id
   functor_unitIso_comp x := by simp [eqToHom_map]
 
+lemma whiskerLeft_inv_hom_heq {C : Type u} [Category.{v} C] {D : Type u₁}
+    [Category.{v₁} D] {E : Type u₂} [Category.{v₂} E] (F : C ≅≅ D) (G H : D ⥤ E) (η : G ⟶ H) :
+    (F.inv ⋙ F.hom).whiskerLeft η ≍ η := by
+  rw [F.inv_hom_id]
+  aesop_cat
+
+lemma whiskerLeft_inv_hom {C : Type u} [Category.{v} C] {D : Type u₁} [Category.{v₁} D]
+    {E : Type u₂} [Category.{v₂} E] (F : C ≅≅ D) (G H : D ⥤ E) (η : G ⟶ H) :
+    (F.inv ⋙ F.hom).whiskerLeft η = eqToHom (by aesop) ≫ η ≫ eqToHom (by aesop) := by
+  simpa [← heq_eq_eq] using
+    whiskerLeft_inv_hom_heq F G H η
+
+lemma whiskerLeft_hom_inv_heq {C : Type u} [Category.{v} C] {D : Type u₁}
+    [Category.{v₁} D] {E : Type u₂} [Category.{v₂} E] (F : D ≅≅ C) (G H : D ⥤ E) (η : G ⟶ H) :
+    (F.hom ⋙ F.inv).whiskerLeft η ≍ η := by
+  rw [F.hom_inv_id]
+  aesop_cat
+
+lemma whiskerLeft_hom_inv {C : Type u} [Category.{v} C] {D : Type u₁} [Category.{v₁} D]
+    {E : Type u₂} [Category.{v₂} E] (F : D ≅≅ C) (G H : D ⥤ E) (η : G ⟶ H) :
+    (F.hom ⋙ F.inv).whiskerLeft η = eqToHom (by aesop) ≫ η ≫ eqToHom (by aesop) := by
+  simpa [← heq_eq_eq] using
+    whiskerLeft_hom_inv_heq F G H η
+
 end Iso
 
 end CategoryTheory.Functor