{A} {D : A -> Type} `{DHasEquivs A D} {a b : A} (a' : D a) (b' : D b) : {p : a = b & p # a' = b'} -> {e : a $<~> b & DCatEquiv e a' b'} := functor_sigma (cat_equiv_path a b) (fun p => dcat_equiv_path p a' b'). Global Instance isunivalent1cat_total {A} `{IsUnivalent1Cat A} (D : A -> Type) `{!IsDGraph D, !IsD2Graph D, !IsD01Cat D, !IsD1Cat D, !DHasEquivs D} `{!IsDUnivalent1Cat D} : IsUnivalent1Cat (sig D). Proof. snrapply Build_IsUnivalent1Cat. intros aa' bb'. apply (isequiv_homotopic ( _ _ o (path_sigma_uncurried D aa' bb')^-1)). intros []; reflexivity. Defined.
Require Import Basics.Overture. Require Import Basics.Tactics. Require Import Basics.Equivalences. Require Import Types.Sigma. Require Import WildCat.Core. Require Import WildCat.Displayed. Require Import WildCat.Equiv.