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