proposition: Lemma triL : TriangularLaws.left Eta Eps.
proof: Proof. move=> c; rewrite EpsE EtaE_hom hom_compA (functor_o F) /F -(functor_o_head F1). set X := [hom [\o _, _]]. evar (TY : Type). evar (Y : TY). have-> : F1 # X = F1 # Y by congr (F1 # _); rewrite hom_ext /X /= -(natural eps0); exact: erefl. rewrite (functor_o_head F1) FIdf. rewrite -!hom_compA triL1 compidf. rewrite -[in RHS](functor_id F1) -(functor_o F1); congr (F1 # _). by rewrite hom_ext /= triL0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)