(xa yb : StrX) (f : xa <~=~> yb) : xa.1 <~=~> yb.1. Proof. exists (PreCategoryOfStructures.f (f : morphism _ _ _)). exists (PreCategoryOfStructures.f f^-1). - exact (ap (@PreCategoryOfStructures.f _ _ _ _) (@left_inverse _ _ _ _ f)). - exact (ap (@PreCategoryOfStructures.f _ _ _ _) (@right_inverse _ _ _ _ f)). Defined.
Require Import Category.Core Category.Univalent Category.Morphisms. Require Import Structure.Core. Require Import Types.Sigma Trunc Equivalences. Require Import Basics.Iff Basics.Tactics.