{A} `{HasEquivs A} {a b c d : A} (f : a $<~> b) (g : b $<~> c) (h : c $<~> d) : cate_fun ((h $oE g) $oE f) $== cate_fun (h $oE (g $oE f)). Proof. refine (compose_cate_fun _ f $@ _ $@ cat_assoc f g h $@ _ $@ compose_cate_funinv h _). - refine (compose_cate_fun h g $@R _). - refine (_ $@L compose_cate_funinv g f). Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.