From 8294fa6451b9e962aa34e7d848a85f9cec900e1c Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 26 Sep 2023 13:43:50 -0400 Subject: [PATCH] WildCat/Equiv: add lots of lemmas --- theories/Basics/Notations.v | 1 + theories/WildCat/Core.v | 20 ++--- theories/WildCat/Equiv.v | 148 ++++++++++++++++++++++++++++++++++++ 3 files changed, 160 insertions(+), 9 deletions(-) diff --git a/theories/Basics/Notations.v b/theories/Basics/Notations.v index 3bba75819ed..f88b7ded907 100644 --- a/theories/Basics/Notations.v +++ 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$'"). diff --git a/theories/WildCat/Core.v b/theories/WildCat/Core.v index 14b21db99fb..a5f5995f2b6 100644 --- a/theories/WildCat/Core.v +++ b/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. diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v index 2eb14784d56..61ed7acdeb1 100644 --- a/theories/WildCat/Equiv.v +++ b/theories/WildCat/Equiv.v @@ -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) @@ -211,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} @@ -228,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).