Wildcat pullbacks

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.

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.

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.

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.

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]. *)

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.
 

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. *)

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}

theories/WildCat/Adjoint.v

@@ -67,13 +67,9 @@ Lemma fun01_profunctor {A B C D : Type} (F : A -> B) (G : C -> D)
 Proof.
   snapply Build_Fun01.
   1: exact (functor_prod F G).
-  rapply is0functor_prod_functor.
+  rapply is0functor_prod_functor.  (* Why not found by typeclass search? *)
 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. *)

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}

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)

theories/WildCat/Products.v

@@ -88,11 +88,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.
 

theories/WildCat/Sigma.v

@@ -3,7 +3,7 @@ Require Import WildCat.Core.
 
 (** * Indexed sum of categories *)
 
-(** We define a wild category structure on [sig B] where [B : A -> Type] is a family of wild categories.  In this construction, we implicitly regard [A] as a wild category using its path groupoid structure. *)
+(** We define a wild category structure on [sig B] where [B : A -> Type] is a family of wild categories.  In this construction, we implicitly regard [A] as a wild category using its path groupoid structure.  We only handle the case where each [B a] is a 0-groupoid, for now. *)
 
 Section Sigma.
 
@@ -41,7 +41,7 @@ Defined.
 
 End Sigma.
 
-Instance is0functor_sigma {A : Type} (B C : A -> Type)
+Instance is0functor_functor_sigma_id {A : Type} (B C : A -> Type)
        `{forall a, IsGraph (B a)} `{forall a, IsGraph (C a)}
        `{forall a, Is01Cat (B a)} `{forall a, Is01Cat (C a)}
        (F : forall a, B a -> C a) {ff : forall a, Is0Functor (F a)}

theories/WildCat/Yoneda.v

@@ -192,7 +192,7 @@ Definition opyon_cancel {A : Type} `{Is01Cat A} (a b : A)
 
 Definition opyon1 {A : Type} `{Is01Cat A} (a : A) : Fun01 A Type.
 Proof.
-  exact (Build_Fun01 _ _ (opyon a)).
+  exact (Build_Fun01 (opyon a)).
 Defined.
 
 Definition opyon11 {A : Type} `{Is1Cat A} `{!HasMorExt A} (a : A) : Fun11 A Type.
@@ -241,8 +241,7 @@ Instance is0functor_hom_0gpd {A : Type} `{Is1Cat A}
 Proof.
   napply Build_Is0Functor.
   intros [a1 a2] [b1 b2] [f1 f2]; unfold op in *; cbn in *.
-  rapply (Build_Fun01 (opyon_0gpd a1 a2) (opyon_0gpd b1 b2)
-          (cat_postcomp b1 f2 o cat_precomp a2 f1)).
+  rapply (Build_Fun01 (cat_postcomp b1 f2 o cat_precomp a2 f1)).
 Defined.
 
 Instance is1functor_hom_0gpd {A : Type} `{Is1Cat A}
@@ -280,7 +279,7 @@ Instance is0functor_opyon_0gpd {A : Type} `{Is1Cat A} (a : A)
 Proof.
   apply Build_Is0Functor.
   intros b c f.
-  exact (Build_Fun01 (opyon_0gpd a b) (opyon_0gpd a c) (cat_postcomp a f)).
+  exact (Build_Fun01 (cat_postcomp a f)).
 Defined.
 
 Instance is1functor_opyon_0gpd {A : Type} `{Is1Cat A} (a : A)
@@ -300,8 +299,7 @@ Definition opyoneda_0gpd {A : Type} `{Is1Cat A} (a : A)
   : F a -> (opyon_0gpd a $=> F).
 Proof.
   intros x b.
-  refine (Build_Fun01 (opyon_0gpd a b) (F b) (fun f => fmap F f x)).
-  rapply Build_Is0Functor.
+  refine (Build_Fun01' (A:=opyon_0gpd a b) (B:=F b) (fun f => fmap F f x) _).
   intros f1 f2 h.
   exact (fmap2 F h x).
 Defined.

theories/WildCat/ZeroGroupoid.v

@@ -103,9 +103,9 @@ Definition isequiv_0gpd_issurjinj {G H : ZeroGpd} (F : G $-> H)
 Proof.
   destruct e as [e0 e1]; unfold SplEssSurj in e0.
   stapply catie_adjointify.
-  - snapply Build_Fun01.
+  - snapply Build_Fun01'.
     1: exact (fun y => (e0 y).1).
-    snapply Build_Is0Functor; cbn beta.
+    cbn beta.
     intros y1 y2 m.
     apply e1.
     exact ((e0 y1).2 $@ m $@ ((e0 y2).2)^$).
@@ -126,9 +126,7 @@ Definition prod_0gpd_pr {I : Type} {G : I -> ZeroGpd}
   : forall i, prod_0gpd I G $-> G i.
 Proof.
   intros i.
-  snapply Build_Fun01.
-  1: exact (fun f => f i).
-  snapply Build_Is0Functor; cbn beta.
+  apply (Build_Fun01' (fun f => f i)); cbn beta.
   intros f g p.
   exact (p i).
 Defined.
@@ -139,10 +137,8 @@ Definition equiv_prod_0gpd_corec {I : Type} {G : ZeroGpd} {H : I -> ZeroGpd}
 Proof.
   snapply Build_Equiv.
   { intro f.
-    snapply Build_Fun01.
-    1: exact (fun x i => f i x).
-    snapply Build_Is0Functor; cbn beta.
-    intros x y p i; simpl.
+    apply (Build_Fun01' (fun x i => f i x)).
+    intros x y p i.
     exact (fmap (f i) p). }
   snapply Build_IsEquiv.
   - intro f.
@@ -162,15 +158,12 @@ Definition cate_prod_0gpd {I J : Type} (ie : I <~> J)
   : prod_0gpd I G $<~> prod_0gpd J H.
 Proof.
   snapply cate_adjointify.
-  - snapply Build_Fun01.
+  - snapply Build_Fun01'.
     + intros h j.
       exact (transport H (eisretr ie j) (cate_fun (f (ie^-1 j)) (h _))).
-    + napply Build_Is0Functor.
-      intros g h p j.
-      destruct (eisretr ie j).
-      refine (_ $o Hom_path (transport_1 _ _)).
-      apply Build_Fun01.
-      exact (p _).
+    + cbn. intros g h p j.
+      destruct (eisretr ie j); simpl.
+      exact (fmap _ (p _)).
   - exact (equiv_prod_0gpd_corec (fun i => (f i)^-1$ $o prod_0gpd_pr (ie i))).
   - intros h j.
     cbn.