Definition iscontr_X : ∏ b : B, iscontr (X b). Proof. intro b. assert (HH : isaprop (iscontr (X b))). apply isapropiscontr. apply (p b (tpair (λ x, isaprop x) (iscontr (X b)) HH)). intro t. exists (X_aux_type_center_of_contr b (pr1 t) (pr2 t)). apply (X_aux_type_contr_eq b (pr1 t) (pr2 t)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering.