{A : Type} `{IsUnivalent1Cat A} (a b : A) : (a $<~> b) -> (a = b) := (cat_equiv_path a b)^-1.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.