Wildcat improvements

theories/Algebra/AbGroups/Abelianization.v

@@ -17,9 +17,9 @@ Definition group_precomp {a b} := @cat_precomp Group _ _ a b.
 
 Class IsAbelianization {G : Group} (G_ab : AbGroup)
       (eta : GroupHomomorphism G G_ab)
-  := isequiv0gpd_isabel : forall (A : AbGroup),
+  := issurjinj_isabel : forall (A : AbGroup),
       IsSurjInj (group_precomp A eta).
-Global Existing Instance isequiv0gpd_isabel.
+Global Existing Instance issurjinj_isabel.
 
 (** Here we define abelianization as a HIT. Specifically as a set-coequalizer of the following two maps: (a, b, c) |-> a (b c) and (a, b, c) |-> a (c b).
 

theories/Pointed/Core.v

@@ -712,6 +712,18 @@ Proof.
     + intros x; exact (s x).
 Defined.
 
+Global Instance hasmorext_core_ptype `{Funext} : HasMorExt (core pType).
+Proof.
+  snrapply Build_HasMorExt.
+  intros a b f g.
+  unfold GpdHom_path.
+  cbn in f, g.
+  (* [GpdHom_path] and the inverse of [equiv_path_pequiv] are not definitionally equal, but they compute to definitionally equal things on [idpath]. *)
+  apply (isequiv_homotopic (equiv_path_pequiv f g)^-1%equiv).
+  intro p; induction p; cbn.
+  reflexivity.
+Defined.
+
 (** pType is a univalent 1-coherent 1-category *)
 Global Instance isunivalent_ptype `{Univalence} : IsUnivalent1Cat pType.
 Proof.

theories/Types/Equiv.v

@@ -107,6 +107,16 @@ Section AssumeFunext.
     (* Coq can find this instance by itself, but it's slow. *)
     := equiv_isequiv (equiv_path_equiv e1 e2).
 
+  (** The inverse equivalence is homotopic to [ap equiv_fun], so that is also an equivalence. *)
+  Global Instance isequiv_ap_equiv_fun `{Funext} {A B : Type} (e1 e2 : A <~> B)
+    : IsEquiv (ap (x:=e1) (y:=e2) (@equiv_fun A B)).
+  Proof.
+    snrapply isequiv_homotopic.
+    - exact (equiv_path_equiv e1 e2)^-1%equiv.
+    - exact _.
+    - intro p. exact (ap_compose (fun v => (equiv_fun v; equiv_isequiv v)) pr1 p)^.
+  Defined.
+
   (** This implies that types of equivalences inherit truncation.  Note that we only state the theorem for [n.+1]-truncatedness, since it is not true for contractibility: if [B] is contractible but [A] is not, then [A <~> B] is not contractible because it is not inhabited.
 
    Don't confuse this lemma with [trunc_equiv], which says that if [A] is truncated and [A] is equivalent to [B], then [B] is truncated.  It would be nice to find a better pair of names for them. *)

theories/WildCat/Equiv.v

@@ -71,7 +71,7 @@ Definition cate_adjointify {A} `{HasEquivs A} {a b : A}
            (f : a $-> b) (g : b $-> a)
            (r : f $o g $== Id b) (s : g $o f $== Id a)
   : a $<~> b
-  := @Build_CatEquiv _ _ _ _ _ _ a b f (catie_adjointify f g r s).
+  := Build_CatEquiv f (fe:=catie_adjointify f g r s).
 
 (** This one we define to construct the whole inverse equivalence. *)
 Definition cate_inv {A} `{HasEquivs A} {a b : A} (f : a $<~> b) : b $<~> a.
@@ -119,10 +119,11 @@ Global Instance symmetric_cate {A} `{HasEquivs A}
   := fun a b f => cate_inv f.
 
 (** Equivalences can be composed. *)
-Definition compose_cate {A} `{HasEquivs A} {a b c : A}
-  (g : b $<~> c) (f : a $<~> b) : a $<~> c.
+Global Instance compose_catie {A} `{HasEquivs A} {a b c : A}
+  (g : b $<~> c) (f : a $<~> b)
+  : CatIsEquiv (g $o f).
 Proof.
-  refine (cate_adjointify (g $o f) (f^-1$ $o g^-1$) _ _).
+  refine (catie_adjointify _ (f^-1$ $o g^-1$) _ _).
   - refine (cat_assoc _ _ _ $@ _).
     refine ((_ $@L cat_assoc_opp _ _ _) $@ _).
     refine ((_ $@L (cate_isretr _ $@R _)) $@ _).
@@ -135,6 +136,10 @@ Proof.
     apply cate_issect.
 Defined.
 
+Definition compose_cate {A} `{HasEquivs A} {a b c : A}
+  (g : b $<~> c) (f : a $<~> b) : a $<~> c
+  := Build_CatEquiv (g $o f).
+
 Notation "g $oE f" := (compose_cate g f).
 
 Definition compose_cate_fun {A} `{HasEquivs A}
@@ -242,6 +247,7 @@ Definition cat_path_equiv {A : Type} `{IsUnivalent1Cat A} (a b : A)
 
 Record core (A : Type) := { uncore : A }.
 Arguments uncore {A} c.
+Arguments Build_core {A} a : rename.
 
 Global Instance isgraph_core {A : Type} `{HasEquivs A}
   : IsGraph (core A).
@@ -331,54 +337,25 @@ Proof.
   - apply cate_isretr.
 Defined.
 
-(** ** Pre/post-composition with equivalences *)
-
-(** Precomposition with a cat_equiv is an equivalence between the homs *)
-Definition equiv_precompose_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt A}
-  {x y z : A} (f : x $<~> y)
-  : (y $-> z) <~> (x $-> z).
+Global Instance hasequivs_core {A : Type} `{HasEquivs A}
+  : HasEquivs (core A).
 Proof.
-  snrapply equiv_adjointify.
-  1: exact (fun g => g $o f).
-  1: exact (fun h => h $o f^-1$).
-  { intros h.
-    apply path_hom.
-    refine (cat_assoc _ _ _ $@ _).
-    refine (_ $@ _).
-    { rapply cat_postwhisker.
-      apply cate_issect. }
-    apply cat_idr. }
-  intros g.
-  apply path_hom.
-  refine (cat_assoc _ _ _ $@ _).
-  refine (_ $@ _).
-  { rapply cat_postwhisker.
-    apply cate_isretr. }
-  apply cat_idr.
-Defined.
-
-(** Postcomposition with a cat_equiv is an equivalence between the homs *)
-Definition equiv_postcompose_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt A}
-  {x y z : A} (f : y $<~> z)
-  : (x $-> y) <~> (x $-> z).
-Proof.
-  snrapply equiv_adjointify.
-  1: exact (fun g => f $o g).
-  1: exact (fun h => f^-1$ $o h).
-  { intros h.
-    apply path_hom.
-    refine ((cat_assoc _ _ _)^$ $@ _).
-    refine (_ $@ _).
-    { rapply cat_prewhisker.
-      apply cate_isretr. }
-    apply cat_idl. }
-  intros g.
-  apply path_hom.
-  refine ((cat_assoc _ _ _)^$ $@ _).
-  refine (_ $@ _).
-  { rapply cat_prewhisker.
-    apply cate_issect. }
-  apply cat_idl.
+  srapply Build_HasEquivs.
+  1: exact (fun a b => a $-> b).  (* In [core A], i.e. [CatEquiv' (uncore a) (uncore b)]. *)
+  all: intros a b f; cbn; intros.
+  - exact Unit.  (* Or [CatIsEquiv' (uncore a) (uncore b) (cate_fun f)]? *)
+  - exact f.
+  - exact tt.    (* Or [cate_isequiv' _ _ _]? *)
+  - exact f.
+  - reflexivity.
+  - exact f^-1$.
+  - refine (compose_cate_fun _ _ $@ _).
+    refine (cate_issect _ $@ _).
+    symmetry; apply id_cate_fun.
+  - refine (compose_cate_fun _ _ $@ _).
+    refine (cate_isretr _ $@ _).
+    symmetry; apply id_cate_fun.
+  - exact tt.
 Defined.
 
 (** * Initial objects and terminal objects are all respectively equivalent. *)

theories/WildCat/NatTrans.v

@@ -192,42 +192,39 @@ Defined.
 Global Set Warnings "-ambiguous-paths".
 Coercion nattrans_natequiv : NatEquiv >-> NatTrans.
 
-Definition natequiv_compose {A B} {F G H : A -> B} `{IsGraph A} `{HasEquivs B}
-  `{!Is0Functor F, !Is0Functor G, !Is0Functor H}
-  : NatEquiv G H -> NatEquiv F G -> NatEquiv F H.
+Definition Build_NatEquiv' {A B : Type} `{IsGraph A} `{HasEquivs B}
+  {F G : A -> B} `{!Is0Functor F, !Is0Functor G}
+  (alpha : NatTrans F G) `{forall a, CatIsEquiv (alpha a)}
+  : NatEquiv F G.
 Proof.
-  intros alpha beta.
   snrapply Build_NatEquiv.
-  1: exact (fun a => alpha a $oE beta a).
-  hnf; intros x y f.
-  refine (cat_prewhisker (compose_cate_fun _ _) _ $@ _).
-  refine (_ $@ cat_postwhisker _ (compose_cate_fun _ _)^$).
-  revert x y f.
-  rapply is1natural_comp.
+  - intro a.
+    refine (Build_CatEquiv (alpha a)).
+  - intros a a' f.
+    refine (cate_buildequiv_fun _ $@R _ $@ _ $@ (_ $@L cate_buildequiv_fun _)^$).
+    apply (isnat alpha).
 Defined.
 
+Definition natequiv_compose {A B} {F G H : A -> B} `{IsGraph A} `{HasEquivs B}
+  `{!Is0Functor F, !Is0Functor G, !Is0Functor H}
+  (alpha : NatEquiv G H) (beta : NatEquiv F G)
+  : NatEquiv F H
+  := Build_NatEquiv' (nattrans_comp alpha beta).
+
 Definition natequiv_prewhisker {A B C} {H K : B -> C}
   `{IsGraph A, HasEquivs B, HasEquivs C, !Is0Functor H, !Is0Functor K}
   (alpha : NatEquiv H K) (F : A -> B) `{!Is0Functor F}
-  : NatEquiv (H o F) (K o F).
-Proof.
-  snrapply Build_NatEquiv.
-  1: exact (alpha o F).
-  exact (is1natural_prewhisker _ _).
-Defined.
+  : NatEquiv (H o F) (K o F)
+  := Build_NatEquiv' (nattrans_prewhisker alpha F).
 
 Definition natequiv_postwhisker {A B C} {F G : A -> B}
   `{IsGraph A, HasEquivs B, HasEquivs C, !Is0Functor F, !Is0Functor G}
    (K : B -> C) (alpha : NatEquiv F G) `{!Is0Functor K, !Is1Functor K}
   : NatEquiv (K o F) (K o G).
 Proof.
-  snrapply Build_NatEquiv.
-  1: exact (fun a => emap K (alpha a)).
-  hnf. intros x y f.
-  refine (cat_prewhisker (cate_buildequiv_fun _) _ $@ _).
-  refine (_ $@ cat_postwhisker _ (cate_buildequiv_fun _)^$).
-  revert x y f.
-  exact (is1natural_postwhisker _ _).
+  srefine (Build_NatEquiv' (nattrans_postwhisker K alpha)).
+  2: unfold nattrans_postwhisker, trans_postwhisker; cbn.
+  all: exact _.
 Defined.
 
 Definition natequiv_inverse {A B : Type} `{IsGraph A} `{HasEquivs B}

theories/WildCat/Prod.v

@@ -158,28 +158,20 @@ Defined.
 
 (** Swap functor *)
 
-Definition prod_swap {A B : Type} : A * B -> B * A
-  := fun '(a , b) => (b , a).
-
-Global Instance isequiv_prod_swap {A B}
-  : IsEquiv (@prod_swap A B)
-  := Build_IsEquiv _ _ prod_swap prod_swap
-    (fun _ => idpath) (fun _ => idpath) (fun _ => idpath).
-
-Global Instance is0functor_prod_swap {A B : Type} `{IsGraph A, IsGraph B}
-  : Is0Functor (@prod_swap A B).
+Global Instance is0functor_equiv_prod_symm {A B : Type} `{IsGraph A, IsGraph B}
+  : Is0Functor (equiv_prod_symm A B).
 Proof.
   snrapply Build_Is0Functor.
   intros a b.
-  apply prod_swap.
+  apply equiv_prod_symm.
 Defined.
 
-Global Instance is1functor_prod_swap {A B : Type} `{Is1Cat A, Is1Cat B}
-  : Is1Functor (@prod_swap A B).
+Global Instance is1functor_equiv_prod_symm {A B : Type} `{Is1Cat A, Is1Cat B}
+  : Is1Functor (equiv_prod_symm A B).
 Proof.
   snrapply Build_Is1Functor.
   - intros a b f g.
-    apply prod_swap.
+    apply equiv_prod_symm.
   - intros a.
     reflexivity.
   - reflexivity.

theories/WildCat/Universe.v

@@ -1,4 +1,4 @@
-Require Import Basics.Overture Basics.Tactics Basics.Equivalences.
+Require Import Basics.Overture Basics.Tactics Basics.Equivalences Types.Equiv.
 Require Import WildCat.Core.
 Require Import WildCat.Equiv.
 
@@ -76,6 +76,18 @@ Proof.
   - intros g r s; refine (isequiv_adjointify f g r s).
 Defined.
 
+Global Instance hasmorext_core_type `{Funext}: HasMorExt (core Type).
+Proof.
+  snrapply Build_HasMorExt.
+  intros A B f g; cbn in *.
+  snrapply isequiv_homotopic.
+  - exact (GpdHom_path o (ap (x:=f) (y:=g) equiv_fun)).
+  - nrapply isequiv_compose.
+    1: apply isequiv_ap_equiv_fun.
+    exact (isequiv_Htpy_path (uncore A) (uncore B) f g).
+  - intro p; by induction p.
+Defined.
+
 Definition catie_isequiv {A B : Type} {f : A $-> B}
        `{IsEquiv A B f} : CatIsEquiv f.
 Proof.