Merge pull request #2333 from jdchristensen/wildcat-pullbacks

jdchristensen · web-flow · commit 29a67bd431e9 · 2025-12-21T14:59:02.000-05:00
Add pullbacks of ZeroGroupoids and pullbacks in wild categories
diff --git a/theories/Algebra/AbGroups/AbHom.v b/theories/Algebra/AbGroups/AbHom.v
@@ -162,7 +162,7 @@ Defined.
 Instance is0functor_ab_hom01 `{Funext} {A : Group^op}
   : Is0Functor (ab_hom A).
 Proof.
-  snapply (Build_Is0Functor _ AbGroup); intros B B' f.
+  snapply Build_Is0Functor; intros B B' f.
   snapply Build_GroupHomomorphism.
   1: exact (fun g => grp_homo_compose f g).
   intros phi psi.
@@ -173,7 +173,7 @@ Defined.
 Instance is0functor_ab_hom10 `{Funext} {B : AbGroup@{u}}
   : Is0Functor (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B).
 Proof.
-  snapply (Build_Is0Functor (Group^op) AbGroup); intros A A' f.
+  snapply Build_Is0Functor; intros A A' f.
   snapply Build_GroupHomomorphism.
   1: exact (fun g => grp_homo_compose g f).
   intros phi psi.
diff --git a/theories/Algebra/Monoids/Monoid.v b/theories/Algebra/Monoids/Monoid.v
@@ -202,7 +202,7 @@ Proof.
 Defined.
 
 Instance is0functor_monoid_type : Is0Functor monoid_type
-  := Build_Is0Functor _ _ _ _ monoid_type (@mnd_homo_map).
+  := Build_Is0Functor monoid_type (@mnd_homo_map).
 
 Instance is1functor_monoid_type : Is1Functor monoid_type.
 Proof.
diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v
@@ -351,9 +351,7 @@ Instance is0functor_joinrecdata_0gpd (A B : Type) : Is0Functor (joinrecdata_0gpd
 Proof.
   apply Build_Is0Functor.
   intros P Q g.
-  snapply Build_Fun01.
-  - exact (joinrecdata_fun g).
-  - apply is0functor_joinrecdata_fun.
+  exact (Build_Fun01 (joinrecdata_fun g)).
 Defined.
 
 (** [joinrecdata_0gpd A B] is a 1-functor from [Type] to [ZeroGpd]. *)
@@ -685,14 +683,13 @@ Section JoinSym.
   Definition joinrecdata_sym (A B P : Type)
     : joinrecdata_0gpd A B P $-> joinrecdata_0gpd B A P.
   Proof.
-    snapply Build_Fun01.
+    snapply Build_Fun01'.
     (* The map of types [JoinRecData A B P -> JoinRecData B A P]: *)
     - intros [fl fr fg].
       snapply (Build_JoinRecData fr fl).
       intros b a; exact (fg a b)^.
     (* It respects the paths. *)
-    - apply Build_Is0Functor.
-      intros f g h; simpl.
+    - intros f g h; simpl.
       snapply Build_JoinRecPath; simpl.
       1, 2: intros; apply h.
       intros b a.
diff --git a/theories/Homotopy/Join/JoinAssoc.v b/theories/Homotopy/Join/JoinAssoc.v
@@ -12,7 +12,7 @@ From HoTT Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.
 Definition trijoinrecdata_twist (A B C P : Type)
   : trijoinrecdata_0gpd A B C P $-> trijoinrecdata_0gpd B A C P.
 Proof.
-  snapply Build_Fun01.
+  snapply Build_Fun01'.
   (* The map of types [TriJoinRecData A B C P -> TriJoinRecData B A C P]: *)
   - cbn.
     intros [f1 f2 f3 f12 f13 f23 f123].
@@ -24,8 +24,7 @@ Proof.
       apply moveR_Vp.
       symmetry; apply f123.
   (* It respects the paths. *)
-  - apply Build_Is0Functor.
-    intros f g h; cbn in *.
+  - intros f g h; cbn in *.
     snapply Build_TriJoinRecPath; intros; simpl.
     1, 2, 3, 5, 6: apply h.
     + cbn zeta.
diff --git a/theories/Homotopy/Join/TriJoin.v b/theories/Homotopy/Join/TriJoin.v
@@ -617,9 +617,7 @@ Instance is0functor_trijoinrecdata_0gpd (A B C : Type) : Is0Functor (trijoinrecd
 Proof.
   apply Build_Is0Functor.
   intros P Q g.
-  snapply Build_Fun01.
-  - exact (trijoinrecdata_fun g).
-  - apply is0functor_trijoinrecdata_fun.
+  exact (Build_Fun01 (trijoinrecdata_fun g)).
 Defined.
 
 (** [trijoinrecdata_0gpd A B C] is a 1-functor from [Type] to [ZeroGpd]. *)
diff --git a/theories/Homotopy/Suspension.v b/theories/Homotopy/Suspension.v
@@ -243,7 +243,7 @@ Proof.
 Defined.
 
 Instance is0functor_susp : Is0Functor Susp
-  := Build_Is0Functor _ _ _ _ Susp (@functor_susp).
+  := Build_Is0Functor Susp (@functor_susp).
 
 Instance is1functor_susp : Is1Functor Susp
   := Build_Is1Functor _ _ _ _ _ _ _ _ _ _ Susp _
@@ -418,7 +418,7 @@ Section UnivPropNat.
   Local Instance is0functor_functor_Susp_ind_data
     : Is0Functor functor_Susp_ind_data.
   Proof.
-    exact (is0functor_sigma _ _
+    exact (is0functor_functor_sigma_id _ _
            (fun NS => functor_Susp_ind_data' NS o functor_Susp_ind_data'' NS)).
   Defined.
 
diff --git a/theories/Pointed/pSusp.v b/theories/Pointed/pSusp.v
@@ -33,7 +33,7 @@ Definition psusp (X : Type) : pType
 (** [psusp] has a functorial action. *)
 (** TODO: make this a displayed functor *)
 Instance is0functor_psusp : Is0Functor psusp
-  := Build_Is0Functor _ _ _ _ psusp (fun X Y f
+  := Build_Is0Functor psusp (fun X Y f
       => Build_pMap (functor_susp f) 1).
 
 (** [psusp] is a 1-functor. *)
diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v
@@ -111,7 +111,7 @@ Section TruncationModality.
     := O_functor@{k k k} (Tr n) f.
 
   #[export] Instance is0functor_Tr : Is0Functor (Tr n)
-    := Build_Is0Functor _ _ _ _ (Tr n) (@Trunc_functor).
+    := Build_Is0Functor (Tr n) (@Trunc_functor).
 
   #[export] Instance Trunc_functor_isequiv {X Y : Type}
     (f : X -> Y) `{IsEquiv _ _ f}
diff --git a/theories/WildCat/Adjoint.v b/theories/WildCat/Adjoint.v
@@ -32,13 +32,13 @@ Record Adjunction {C D : Type} (F : C -> D) (G : D -> C)
   `{Is1Cat C, Is1Cat D, !Is0Functor F, !Is0Functor G} :=
 {
   equiv_adjunction (x : C) (y : D) : (F x $-> y) <~> (x $-> G y) ;
-  (** Naturality condition in both variable separately *)
+  (** Naturality condition in both variables separately. *)
   (** The left variable is a bit trickier to state since we have opposite categories involved. *)
   is1natural_equiv_adjunction_l (y : D)
     :: Is1Natural (A := C^op) (yon y o F)
         (** We have to explicitly give a witness to the functoriality of [yon y o F]. *)
         (is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _)
-        (yon (G y)) (fun x => equiv_adjunction _ y) ;
+        (yon (G y)) (fun x => equiv_adjunction x y) ;
   (** Naturality in the right variable *)
   is1natural_equiv_adjunction_r (x : C)
     :: Is1Natural (opyon (F x)) (opyon x o G) (equiv_adjunction x) ;
@@ -66,14 +66,10 @@ Lemma fun01_profunctor {A B C D : Type} (F : A -> B) (G : C -> D)
   : Fun01 (A^op * C) (B^op * D).
 Proof.
   snapply Build_Fun01.
-  1: exact (functor_prod F G).
-  rapply is0functor_prod_functor.
+  1: exact (functor_prod (F : A^op -> B^op) G).
+  rapply is0functor_prod_functor. (* Typeclass search gets confused by the opposite categories. *)
 Defined.
 
-Definition fun01_hom {C : Type} `{Is01Cat C}
-  : Fun01 (C^op * C) Type
-  := @Build_Fun01 _ _ _ _ _ is0functor_hom.
-
 (** ** Natural equivalences coming from adjunctions. *)
 
 (** There are various bits of data we would like to extract from adjunctions. *)
diff --git a/theories/WildCat/Core.v b/theories/WildCat/Core.v
@@ -86,6 +86,7 @@ Definition GpdHom_path {A} `{Is0Gpd A} {a b : A} (p : a = b) : a $== b
 Class Is0Functor {A B : Type} `{IsGraph A} `{IsGraph B} (F : A -> B)
   := { fmap : forall (a b : A) (f : a $-> b), F a $-> F b }.
 
+Arguments Build_Is0Functor {A B isgraph_A isgraph_B} F fmap : rename.
 Arguments fmap {A B isgraph_A isgraph_B} F {is0functor_F a b} f : rename.
 
 Class Is2Graph (A : Type) `{IsGraph A}
diff --git a/theories/WildCat/FunctorCat.v b/theories/WildCat/FunctorCat.v
@@ -16,13 +16,19 @@ Record Fun01 (A B : Type) `{IsGraph A} `{IsGraph B} := {
 
 Coercion fun01_F : Fun01 >-> Funclass.
 
-Arguments Build_Fun01 A B {isgraph_A isgraph_B} F {fun01_is0functor} : rename.
+Arguments Build_Fun01 {A B isgraph_A isgraph_B} F {fun01_is0functor} : rename.
 Arguments fun01_F {A B isgraph_A isgraph_B} : rename.
 
+(** An alternate constructor that expects the [fmap] argument. *)
+Definition Build_Fun01' {A B : Type} `{IsGraph A} `{IsGraph B}
+  (F : A -> B) (fmap : forall a b (f : a $-> b), F a $-> F b)
+  : Fun01 A B
+  := Build_Fun01 F (fun01_is0functor:=Build_Is0Functor F fmap).
+
 Definition issig_Fun01 (A B : Type) `{IsGraph A} `{IsGraph B}
   : _  <~> Fun01 A B := ltac:(issig).
 
-(* Note that even if [A] and [B] are fully coherent oo-categories, the objects of our "functor category" are not fully coherent.  Thus we cannot in general expect this "functor category" to itself be fully coherent.  However, it is at least a 0-coherent 1-category, as long as [B] is a 1-coherent 1-category. *)
+(** Note that even if [A] and [B] are fully coherent oo-categories, the objects of our "functor category" are not fully coherent.  Thus we cannot in general expect this "functor category" to itself be fully coherent.  However, it is at least a 0-coherent 1-category, as long as [B] is a 1-coherent 1-category. *)
 
 Instance isgraph_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : IsGraph (Fun01 A B).
 Proof.
@@ -104,7 +110,7 @@ Definition fun01_op (A B : Type) `{IsGraph A} `{IsGraph B}
   : Fun01 A B -> Fun01 A^op B^op.
 Proof.
   intros F.
-  exact (Build_Fun01 A^op B^op F).
+  exact (Build_Fun01 (A:=A^op) (B:=B^op) F).
 Defined.
 
 (** ** Categories of 1-coherent 1-functors *)
@@ -153,7 +159,7 @@ Instance hasequivs_fun11 {A B : Type} `{Is1Cat A} `{HasEquivs B}
 (** * Identity functors *)
 
 Definition fun01_id {A} `{IsGraph A} : Fun01 A A
-  := Build_Fun01 A A idmap.
+  := Build_Fun01 idmap.
 
 Definition fun11_id {A} `{Is1Cat A} : Fun11 A A
   := Build_Fun11 _ _ idmap.
@@ -162,7 +168,7 @@ Definition fun11_id {A} `{Is1Cat A} : Fun11 A A
 
 Definition fun01_compose {A B C} `{IsGraph A, IsGraph B, IsGraph C}
   : Fun01 B C -> Fun01 A B -> Fun01 A C
-  := fun G F => Build_Fun01 _ _ (G o F).
+  := fun G F => Build_Fun01 (G o F).
 
 Definition fun01_postcomp {A B C}
   `{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C)
diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v
@@ -2,12 +2,14 @@ Require Import Basics.Equivalences Basics.Overture Basics.Tactics.
 Require Import Types.Bool Types.Prod Types.Forall.
 Require Import WildCat.Bifunctor WildCat.Core WildCat.Equiv WildCat.EquivGpd
                WildCat.Forall WildCat.NatTrans WildCat.Opposite
-               WildCat.Universe WildCat.Yoneda WildCat.ZeroGroupoid
+               WildCat.Universe WildCat.Yoneda WildCat.Graph WildCat.ZeroGroupoid
                WildCat.Monoidal WildCat.MonoidalTwistConstruction
                WildCat.FunctorCat.
 
 (** * Categories with products *)
 
+(** ** Indexed products *)
+
 Definition cat_prod_corec_inv {I A : Type} `{Is1Cat A}
   (prod : A) (x : I -> A) (z : A) (pr : forall i, prod $-> x i)
   : yon_0gpd prod z $-> prod_0gpd I (fun i => yon_0gpd (x i) z).
@@ -17,7 +19,7 @@ Proof.
   exact (fmap (fun x => yon_0gpd x z) (pr i)).
 Defined.
 
-(* A product of an [I]-indexed family of objects of a category is an object of the category with an [I]-indexed family of projections such that the induced map is an equivalence. *)
+(** A product of an [I]-indexed family of objects of a category is an object of the category with an [I]-indexed family of projections such that the induced map is an equivalence. *)
 Class Product (I : Type) {A : Type} `{Is1Cat A} {x : I -> A} := Build_Product' {
   cat_prod : A;
   cat_pr : forall i : I, cat_prod $-> x i;
@@ -88,11 +90,10 @@ Section Lemmata.
   Proof.
     snapply Build_Is0Functor.
     intros a b f.
-    snapply Build_Fun01.
+    snapply Build_Fun01'.
     - intros g i.
       exact (f $o g i).
-    - snapply Build_Is0Functor.
-      intros g h p i.
+    - intros g h p i.
       exact (f $@L p i).
   Defined.
 
@@ -219,7 +220,7 @@ Proof.
     napply cat_assoc_opp.
 Defined.
 
-(** *** Categories with specific kinds of products *)
+(** *** An empty product is terminal *)
 
 Definition isterminal_prodempty {A : Type} {z : A}
   `{Product Empty A (fun _ => z)}
@@ -229,25 +230,25 @@ Proof.
   snrefine (cat_prod_corec _ _; fun f => cat_prod_pr_eta _ _); intros [].
 Defined.
 
-(** *** Binary products *)
+(** ** Binary products *)
 
 Class BinaryProduct {A : Type} `{Is1Cat A} (x y : A)
-  := binary_product :: Product Bool (fun b => if b then x else y).
+  := binary_product :: Product Bool (Bool_rec _ x y).
 
 (** A category with binary products is a category with a binary product for each pair of objects. *)
 Class HasBinaryProducts (A : Type) `{Is1Cat A}
   := has_binary_products :: forall x y : A, BinaryProduct x y.
 
 Instance hasbinaryproducts_hasproductsbool {A : Type} `{HasProducts Bool A}
   : HasBinaryProducts A
-  := fun x y => has_products (fun b : Bool => if b then x else y).
+  := fun x y => has_products (Bool_rec _ x y).
 
 Section BinaryProducts.
 
   Context {A : Type} `{Is1Cat A} {x y : A} `{!BinaryProduct x y}.
 
   Definition cat_binprod' : A
-    := cat_prod Bool (fun b : Bool => if b then x else y).
+    := cat_prod Bool (Bool_rec _ x y).
 
   Definition cat_pr1 : cat_binprod' $-> x := cat_pr true.
 
@@ -314,7 +315,7 @@ Definition Build_BinaryProduct {A : Type} `{Is1Cat A} {x y : A}
     cat_pr2 $o cat_binprod_corec z f g $== g)
   (cat_binprod_eta_pr : forall (z : A) (f g : z $-> cat_binprod'),
     cat_pr1 $o f $== cat_pr1 $o g -> cat_pr2 $o f $== cat_pr2 $o g -> f $== g)
-  : Product Bool (fun b => if b then x else y).
+  : Product Bool (Bool_rec _ x y).
 Proof.
   snapply (Build_Product _ cat_binprod').
   - intros [|].
@@ -562,7 +563,7 @@ Definition cat_pr2_fmap11_binprod {A : Type} `{HasBinaryProducts A}
 
 (** *** Diagonal *)
 
-(** Annoyingly this doesn't follow directly from the general diagonal since [fun b => if b then x else x] is not definitionally equal to [fun _ => x]. *)
+(** Annoyingly this doesn't follow directly from the general diagonal since [Bool_rec _ x x] is not definitionally equal to [fun _ => x]. *)
 Definition cat_binprod_diag {A : Type}
   `{Is1Cat A} (x : A) `{!BinaryProduct x x}
   : x $-> cat_binprod' x x.
@@ -679,7 +680,7 @@ Section Symmetry.
 
 End Symmetry.
 
-(** *** Associativity of binary products *)
+(** *** Binary product gives a symmetric monoidal structure *)
 
 Section Associativity.
 
@@ -1000,9 +1001,26 @@ Section Associativity.
 
 End Associativity.
 
+(** ** Examples *)
+
 (** *** Products in Type *)
 
 (** Since we use the Yoneda lemma in this file, we therefore depend on WildCat.Universe which means these instances have to live here. *)
+
+(** Assuming [Funext], [Type] has all products. *)
+Instance hasallproducts_type `{Funext} : HasAllProducts Type.
+Proof.
+  intros I x.
+  snapply Build_Product.
+  - exact (forall (i : I), x i).
+  - intros i f. exact (f i).
+  - intros A f a i. exact (f i a).
+  - reflexivity.
+  - intros A f g p a.
+    exact (path_forall _ _ (fun i => p i a)).
+Defined.
+
+(** It follows that [Type] has binary products, but we prove this separately to avoid [Funext]. *)
 Instance hasbinaryproducts_type : HasBinaryProducts Type.
 Proof.
   intros X Y.
@@ -1019,15 +1037,33 @@ Proof.
     + exact (q x).
 Defined.
 
-(** Assuming [Funext], [Type] has all products. *)
-Instance hasallproducts_type `{Funext} : HasAllProducts Type.
+(** *** Products in ZeroGpd *)
+
+(** Since we use products in ZeroGpd to define general products, we must depend on ZeroGroupoid, which means that these instances have to live here. *)
+
+(** Note that this does not rely on [Funext], since the 1-cells in the product 0-groupoid are *defined* to be homotopies. *)
+Instance hasallproducts_0gpd : HasAllProducts ZeroGpd.
 Proof.
   intros I x.
   snapply Build_Product.
-  - exact (forall (i : I), x i).
-  - intros i f. exact (f i).
-  - intros A f a i. exact (f i a).
+  - exact (prod_0gpd I x).
+  - exact prod_0gpd_pr.
+  - intro G. apply equiv_prod_0gpd_corec.
   - reflexivity.
-  - intros A f g p a.
-    exact (path_forall _ _ (fun i => p i a)).
+  - intros G f g p.  intro a.  intro i.
+    exact (p i a).
+Defined.
+
+(** This follows from the previous result, but we prove it separately because using these custom binary products can make certain things easier, and can sometimes avoid the need to use [Funext]. *)
+Instance hasbinaryproducts_0gpd : HasBinaryProducts ZeroGpd.
+Proof.
+  intros G H.
+  snapply Build_BinaryProduct.
+  - exact (binprod_0gpd G H).
+  - apply binprod_0gpd_pr1.
+  - apply binprod_0gpd_pr2.
+  - intro K. exact (fun f g => (equiv_binprod_0gpd_corec G H K (f, g))).
+  - reflexivity.
+  - reflexivity.
+  - intros K f g p q. intro k. exact (p k, q k).
 Defined.
diff --git a/theories/WildCat/Pullbacks.v b/theories/WildCat/Pullbacks.v
diff --git a/theories/WildCat/Sigma.v b/theories/WildCat/Sigma.v
diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
