Merge pull request #1766 from jdchristensen/wildcat-improvements

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/Basics/Notations.v

@@ -158,6 +158,7 @@ Reserved Infix "$o@" (at level 30).
 Reserved Infix "$@" (at level 30).
 Reserved Infix "$@L" (at level 30).
 Reserved Infix "$@R" (at level 30).
+Reserved Infix "$@@" (at level 30).
 Reserved Infix "$=>" (at level 99).
 Reserved Notation "T ^op" (at level 3, format "T ^op").
 Reserved Notation "f ^-1$" (at level 3, format "f '^-1$'").

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/Core.v

@@ -117,15 +117,7 @@ Definition cat_assoc_opp {A : Type} `{Is1Cat A}
   : h $o (g $o f) $== (h $o g) $o f
   := (cat_assoc f g h)^$.
 
-(*
-Definition Comp2 {A} `{Is1Cat A} {a b c : A}
-           {f g : a $-> b} {h k : b $-> c}
-           (q : h $-> k) (p : f $-> g)
-  : (h $o f $-> k $o g)
-  := ??
-
-Infix "$o@" := Comp2.
-*)
+(** Whiskering and horizontal composition of 2-cells. *)
 
 Definition cat_postwhisker {A} `{Is1Cat A} {a b c : A}
            {f g : a $-> b} (h : b $-> c) (p : f $== g)
@@ -139,6 +131,16 @@ Definition cat_prewhisker {A} `{Is1Cat A} {a b c : A}
   := fmap (cat_precomp c h) p.
 Notation "p $@R h" := (cat_prewhisker p h).
 
+Definition cat_comp2 {A} `{Is1Cat A} {a b c : A}
+  {f g : a $-> b} {h k : b $-> c}
+  (p : f $== g) (q : h $== k )
+  : h $o f $== k $o g
+  := (q $@R _) $@ (_ $@L p).
+
+Notation "q $@@ p" := (cat_comp2 q p).
+
+(** Monomorphisms and epimorphisms. *)
+
 Definition Monic {A} `{Is1Cat A} {b c: A} (f : b $-> c)
   := forall a (g h : a $-> b), f $o g $== f $o h -> g $== h.
 

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.
@@ -101,6 +101,39 @@ Proof.
   apply cate_buildequiv_fun'.
 Defined.
 
+(** If [g] is a section of an equivalence, then it is the inverse. *)
+Definition cate_inverse_sect {A} `{HasEquivs A} {a b} (f : a $<~> b)
+  (g : b $-> a) (p : f $o g $== Id b)
+  : cate_fun f^-1$ $== g.
+Proof.
+  refine ((cat_idr _)^$ $@ _).
+  refine ((_ $@L p^$) $@ _).
+  refine (cat_assoc_opp _ _ _ $@ _).
+  refine (cate_issect f $@R _ $@ _).
+  apply cat_idl.
+Defined.
+
+(** If [g] is a retraction of an equivalence, then it is the inverse. *)
+Definition cate_inverse_retr {A} `{HasEquivs A} {a b} (f : a $<~> b)
+  (g : b $-> a) (p : g $o f $== Id a)
+  : cate_fun f^-1$ $== g.
+Proof.
+  refine ((cat_idl _)^$ $@ _).
+  refine ((p^$ $@R _) $@ _).
+  refine (cat_assoc _ _ _ $@ _).
+  refine (_ $@L cate_isretr f $@ _).
+  apply cat_idr.
+Defined.
+
+(** It follows that the inverse of the equivalence you get by adjointification is homotopic to the inverse [g] provided. *)
+Definition cate_inv_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)
+  : cate_fun (cate_adjointify f g r s)^-1$ $== g.
+Proof.
+  apply cate_inverse_sect.
+  exact ((cate_buildequiv_fun f $@R _) $@ r).
+Defined.
+
 (** The identity morphism is an equivalence *)
 Global Instance catie_id {A} `{HasEquivs A} (a : A)
   : CatIsEquiv (Id a)
@@ -119,10 +152,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 +169,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}
@@ -206,6 +244,81 @@ Definition compose_hV_h {A} `{HasEquivs A} {a b c : A} (f : b $-> c) (g : b $<~>
   (f $o g^-1$) $o g $== f :=
   cat_assoc _ _ _ $@ (f $@L cate_issect g) $@ cat_idr f.
 
+(** Equivalences are both monomorphisms and epimorphisms (but not the converse). *)
+
+Definition cate_monic_equiv {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
+  : Monic e.
+Proof.
+  intros c f g p.
+  refine ((compose_V_hh e _)^$ $@ _ $@ compose_V_hh e _).
+  exact (_ $@L p).
+Defined.
+
+Definition cate_epic_equiv {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
+  : Epic e.
+Proof.
+  intros c f g p.
+  refine ((compose_hh_V _ e)^$ $@ _ $@ compose_hh_V _ e).
+  exact (p $@R _).
+Defined.
+
+(** Some lemmas for moving equivalences around.  Naming based on EquivGroupoids.v.  More could be added. *)
+
+Definition cate_moveL_V1 {A} `{HasEquivs A} {a b : A} {e : a $<~> b} (f : b $-> a)
+  (p : e $o f $== Id _)
+  : f $== cate_fun e^-1$.
+Proof.
+  apply (cate_monic_equiv e).
+  exact (p $@ (cate_isretr e)^$).
+Defined.
+
+Definition cate_moveL_1V {A} `{HasEquivs A} {a b : A} {e : a $<~> b} (f : b $-> a)
+  (p : f $o e $== Id _)
+  : f $== cate_fun e^-1$.
+Proof.
+  apply (cate_epic_equiv e).
+  exact (p $@ (cate_issect e)^$).
+Defined.
+
+Definition cate_moveR_V1 {A} `{HasEquivs A} {a b : A} {e : a $<~> b} (f : b $-> a)
+  (p : Id _ $== e $o f)
+  : cate_fun e^-1$ $== f.
+Proof.
+  apply (cate_monic_equiv e).
+  exact (cate_isretr e $@ p).
+Defined.
+
+Definition cate_moveR_1V {A} `{HasEquivs A} {a b : A} {e : a $<~> b} (f : b $-> a)
+  (p : Id _ $== f $o e)
+  : cate_fun e^-1$ $== f.
+Proof.
+  apply (cate_epic_equiv e).
+  exact (cate_issect e $@ p).
+Defined.
+
+(** Lemmas about the underlying map of an equivalence. *)
+
+Definition cate_inv2 {A} `{HasEquivs A} {a b : A} {e f : a $<~> b} (p : cate_fun e $== cate_fun f)
+  : cate_fun e^-1$ $== cate_fun f^-1$.
+Proof.
+  apply cate_moveL_V1.
+  exact ((p^$ $@R _) $@ cate_isretr _).
+Defined.
+
+Definition cate_inv_compose {A} `{HasEquivs A} {a b c : A} (e : a $<~> b) (f : b $<~> c)
+  : cate_fun (f $oE e)^-1$ $== cate_fun (e^-1$ $oE f^-1$).
+Proof.
+  refine (_ $@ (compose_cate_fun _ _)^$).
+  apply cate_inv_adjointify.
+Defined.
+
+Definition cate_inv_V {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
+  : cate_fun (e^-1$)^-1$ $== cate_fun e.
+Proof.
+  apply cate_moveR_V1.
+  symmetry; apply cate_issect.
+Defined.
+
 (** Any sufficiently coherent functor preserves equivalences.  *)
 Global Instance iemap {A B : Type} `{HasEquivs A} `{HasEquivs B}
        (F : A -> B) `{!Is0Functor F, !Is1Functor F}
@@ -223,6 +336,46 @@ Definition emap {A B : Type} `{HasEquivs A} `{HasEquivs B}
   : F a $<~> F b
   := Build_CatEquiv (fmap F f).
 
+Definition emap_id {A B : Type} `{HasEquivs A} `{HasEquivs B}
+  (F : A -> B) `{!Is0Functor F, !Is1Functor F} {a : A}
+  : cate_fun (emap F (id_cate a)) $== cate_fun (id_cate (F a)).
+Proof.
+  refine (cate_buildequiv_fun _ $@ _).
+  refine (fmap2 F (id_cate_fun a) $@ _ $@ (id_cate_fun (F a))^$).
+  rapply fmap_id.
+Defined.
+
+Definition emap_compose {A B : Type} `{HasEquivs A} `{HasEquivs B}
+  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
+  {a b c : A} (f : a $<~> b) (g : b $<~> c)
+  : cate_fun (emap F (g $oE f)) $== fmap F (cate_fun g) $o fmap F (cate_fun f).
+Proof.
+  refine (cate_buildequiv_fun _ $@ _).
+  refine (fmap2 F (compose_cate_fun _ _) $@ _).
+  rapply fmap_comp.
+Defined.
+
+(** A variant. *)
+Definition emap_compose' {A B : Type} `{HasEquivs A} `{HasEquivs B}
+  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
+  {a b c : A} (f : a $<~> b) (g : b $<~> c)
+  : cate_fun (emap F (g $oE f)) $== cate_fun ((emap F g) $oE (emap F f)).
+Proof.
+  refine (emap_compose F f g $@ _).
+  symmetry.
+  refine (compose_cate_fun _ _ $@ _).
+  exact (cate_buildequiv_fun _ $@@ cate_buildequiv_fun _).
+Defined.
+
+Definition emap_inv {A B : Type} `{HasEquivs A} `{HasEquivs B}
+  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
+  {a b : A} (e : a $<~> b)
+  : cate_fun (emap F e)^-1$ $== cate_fun (emap F e^-1$).
+Proof.
+  refine (cate_inv_adjointify _ _ _ _ $@ _).
+  exact (cate_buildequiv_fun _)^$.
+Defined.
+
 (** When we have equivalences, we can define what it means for a category to be univalent. *)
 Definition cat_equiv_path {A : Type} `{HasEquivs A} (a b : A)
   : (a = b) -> (a $<~> b).
@@ -242,6 +395,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 +485,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. *)