`{Univalence} {X : Type} (x1 x2 : X) : paths x1 = paths x2 -> x1 = x2. Proof. refine (_ o @equiv_ap10 _ X Type (paths x1) (paths x2)). refine (_ o equiv_functor_forall_id (fun y => equiv_equiv_path (x1 = y) (x2 = y))). refine (_ o functor_forall_id (fun y => @equiv_fun (x1 = y) (x2 = y))). refine (_ o (equiv_paths_ind x1 (fun y p => x2 = y))^-1%equiv). exact (equiv_path_inverse x2 x1). Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.