Build_NatEquiv' {A B : Type} `{IsGraph A} `{HasEquivs B} {F G : A -> B} `{!Is0Functor F, !Is0Functor G} (alpha : NatTrans F G) `{forall a, CatIsEquiv (alpha a)} : NatEquiv F G. Proof. snrapply Build_NatEquiv. - intro a. refine (Build_CatEquiv (alpha a)). - snrapply Build_Is1Natural'. + intros a a' f. refine ((cate_buildequiv_fun _ $@R _) $@ _ $@ (_ $@L cate_buildequiv_fun _)^$). apply (isnat alpha). + intros a a' f. refine ((_ $@L cate_buildequiv_fun _) $@ _ $@ (cate_buildequiv_fun _ $@R _)^$). apply (isnat_tr alpha). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.