fact: Record Epimorphism {C} x y := { Epimorphism_morphism :> morphism C x y; Epimorphism_IsEpimorphism :> IsEpimorphism Epimorphism_morphism }.
imports: Category.Core Functor.Core HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences