fact: Record ff_struct := { ff_invmap :> forall {X Y}, D⦅F X;F Y⦆ -> C⦅X;Y⦆ ; ff_inv_proper : forall {X Y}, Proper (sim D ==> sim C) (@ff_invmap X Y) ; ff_section : forall {X Y} (f : D⦅F X;F Y⦆), fmap F (ff_invmap f) ∼ f ; ff_retraction : forall {X Y} (f : C⦅X;Y⦆), ff_invmap (fmap F f) ∼ f }.
imports: Coq(ssreflect ssrfun) Coq.Classes(RelationClasses Morphisms) Relational(Category)