proposition: Lemma CoUA_diag : forall (u : CoUA) (a' : A) (f : F a' --> b), FMor F (CoUA_diese u f) o CoUA_mor u =_S f.
proof: Proof. intros u a' f; exact (Prf_isCoUA_law1 (u:=CoUA_mor u) u f). Qed.
imports: UniversalArrow Dual_Functor