{A} `{HasEquivs A} {a b c : A} (g : b $<~> c) (f : a $<~> b) : (f^-1$ $o g^-1$ $o (g $o f) $== Id a) := compose_catie_isretr (A:=A^op) (a:=c) (b:=b) (c:=a) f g. Global Instance compose_catie {A} `{HasEquivs A} {a b c : A} (g : b $<~> c) (f : a $<~> b) : CatIsEquiv (g $o f). Proof. refine (catie_adjointify _ (f^-1$ $o g^-1$) _ _). - apply compose_catie_isretr. - apply . Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.