more movement lemmas for WildCat/Equiv.v

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Apr 12, 2024 · 506f4fd · 506f4fd
1 parent 202f97a
commit 506f4fd
Show file tree

Hide file tree

Showing 2 changed files with 77 additions and 19 deletions.
diff --git a/theories/WildCat/DisplayedEquiv.v b/theories/WildCat/DisplayedEquiv.v
@@ -338,24 +338,24 @@ Defined.
 (** Some lemmas for moving equivalences around.  Naming based on EquivGroupoids.v. *)
 
 Definition dcate_moveR_eM {A} {D : A -> Type} `{DHasEquivs A D}
-  {a b c : A} {e : b $<~> a} {f : b $<~> c} {g : a $<~> c}
-  {p : cate_fun g $== f $o e^-1$} {a' : D a} {b' : D b} {c' : D c}
-  (e' : DCatEquiv e b' a') (f' : DCatEquiv f b' c') (g' : DCatEquiv g a' c')
-  (p' : DGpdHom p (dcate_fun g') (dcate_fun f' $o' e'^-1$'))
-  : DGpdHom (cate_moveR_eM e f g p) (dcate_fun g' $o' e') (dcate_fun f').
+  {a b c : A} {e : b $<~> a} {f : a $-> c} {g : b $-> c}
+  {p : f $== g $o e^-1$} {a' : D a} {b' : D b} {c' : D c}
+  (e' : DCatEquiv e b' a') (f' : DHom f a' c') (g' : DHom g b' c')
+  (p' : DGpdHom p f' (g' $o' e'^-1$'))
+  : DGpdHom (cate_moveR_eM e f g p) (f' $o' e') g'.
 Proof.
   apply (dcate_epic_equiv e'^-1$').
   exact (dcompose_hh_V _ _ $@' p').
 Defined.
 
 Definition dcate_moveR_Ve {A} {D : A -> Type} `{DHasEquivs A D}
-  {a b c : A} {e : b $<~> a} {f : b $<~> c} {g : c $<~> a}
-  {p : cate_fun e $== g $o f} {a' : D a} {b' : D b} {c' : D c}
-  (e' : DCatEquiv e b' a') (f' : DCatEquiv f b' c') (g' : DCatEquiv g c' a')
-  (p' : DGpdHom p (dcate_fun e') (dcate_fun g' $o' f'))
-  : DGpdHom (cate_moveR_Ve e f g p) (dcate_fun g'^-1$' $o' e') (dcate_fun f').
+  {a b c : A} {e : b $<~> c} {f : a $-> c} {g : a $-> b}
+  {p : f $== e $o g} {a' : D a} {b' : D b} {c' : D c}
+  (e' : DCatEquiv e b' c') (f' : DHom f a' c') (g' : DHom g a' b')
+  (p' : DGpdHom p f' (dcate_fun e' $o' g'))
+  : DGpdHom (cate_moveR_Ve e f g p) (dcate_fun e'^-1$' $o' f') g'.
 Proof.
-  apply (dcate_monic_equiv g').
+  apply (dcate_monic_equiv e').
   exact (dcompose_h_Vh _ _ $@' p').
 Defined.
 

diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
@@ -282,21 +282,79 @@ Proof.
   exact (p $@R _).
 Defined.
 
-(** Some lemmas for moving equivalences around.  Naming based on EquivGroupoids.v.  More could be added. *)
+(** ** Movement Lemmas *)
 
-Definition cate_moveR_eM {A} `{HasEquivs A} {a b c : A} (e : b $<~> a) (f : b $<~> c) (g : a $<~> c)
-  (p : cate_fun g $== f $o e^-1$)
-  : g $o e $== f.
+(** These lemmas can be used to move equivalences around in an equation. *)
+
+Definition cate_moveL_eM {A} `{HasEquivs A} {a b c : A}
+  (e : a $<~> b) (f : a $-> c) (g : b $-> c)
+  (p : f $o e^-1$ $== g)
+  : f $== g $o e.
+Proof.
+  apply (cate_epic_equiv e^-1$).
+  exact (p $@ (compose_hh_V _ _)^$).
+Defined.
+
+Definition cate_moveR_eM {A} `{HasEquivs A} {a b c : A}
+  (e : b $<~> a) (f : a $-> c) (g : b $-> c)
+  (p : f $== g $o e^-1$)
+  : f $o e $== g.
 Proof.
   apply (cate_epic_equiv e^-1$).
   exact (compose_hh_V _ _ $@ p).
 Defined.
 
-Definition cate_moveR_Ve {A} `{HasEquivs A} {a b c : A} (e : b $<~> a) (f : b $<~> c) (g : c $<~> a)
-  (p : cate_fun e $== g $o f)
-  : g^-1$ $o e $== f.
+Definition cate_moveL_Me {A} `{HasEquivs A} {a b c : A}
+  (e : b $<~> c) (f : a $-> c) (g : a $-> b)
+  (p : e^-1$ $o f $== g)
+  : f $== e $o g.
+Proof.
+  apply (cate_monic_equiv e^-1$).
+  exact (p $@ (compose_V_hh _ _)^$).
+Defined.
+
+Definition cate_moveR_Me {A} `{HasEquivs A} {a b c : A}
+  (e : c $<~> b) (f : a $-> c) (g : a $-> b)
+  (p : f $== e^-1$ $o g)
+  : e $o f $== g.
+Proof.
+  apply (cate_monic_equiv e^-1$).
+  exact (compose_V_hh _ _ $@ p).
+Defined.
+
+Definition cate_moveL_eV {A} `{HasEquivs A} {a b c : A}
+  (e : a $<~> b) (f : b $-> c) (g : a $-> c)
+  (p : f $o e $== g)
+  : f $== g $o e^-1$.
 Proof.
-  apply (cate_monic_equiv g).
+  apply (cate_epic_equiv e).
+  exact (p $@ (compose_hV_h _ _)^$).
+Defined.
+
+Definition cate_moveR_eV {A} `{HasEquivs A} {a b c : A}
+  (e : b $<~> a) (f : b $-> c) (g : a $-> c)
+  (p : f $== g $o e)
+  : f $o e^-1$ $== g.
+Proof.
+  apply (cate_epic_equiv e).
+  exact (compose_hV_h _ _ $@ p).
+Defined.
+
+Definition cate_moveL_Ve {A} `{HasEquivs A} {a b c : A}
+  (e : b $<~> c) (f : a $-> b) (g : a $-> c)
+  (p : e $o f $== g)
+  : f $== e^-1$ $o g.
+Proof.
+  apply (cate_monic_equiv e).
+  exact (p $@ (compose_h_Vh _ _)^$).
+Defined.
+
+Definition cate_moveR_Ve {A} `{HasEquivs A} {a b c : A}
+  (e : b $<~> c) (f : a $-> c) (g : a $-> b)
+  (p : f $== e $o g)
+  : e^-1$ $o f $== g.
+Proof.
+  apply (cate_monic_equiv e).
   exact (compose_h_Vh _ _ $@ p).
 Defined.