`{Univalence} (A : Type@{i}) : loops [Type@{i}, A] <~>* [A <~> A, equiv_idmap]. Proof. apply issig_pequiv'. exists (equiv_equiv_path A A). reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Factorization Truncations.Core Truncations.Connectedness HProp. Require Import Pointed.Core Pointed.pEquiv. Require Import WildCat. Require Import Spaces.Nat.Core.