`{Univalence} (n : trunc_index) {A : pType@{u}} `{IsConnected n.+1 A} (P : A -> Type@{u}) `{forall a, IsTrunc n (P a)} (p0 : P (point A)) : forall a, P a. Proof. intro a. pose proof (p := center (Tr n ((point A) = a))). strip_truncations. exact (p # p0). Defined.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.