fact: Record Monomorphism {C} x y := { Monomorphism_morphism :> morphism C x y; Monomorphism_IsMonomorphism :> IsMonomorphism Monomorphism_morphism }.
imports: Category.Core Functor.Core HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences