Definition Y_iscontr (b b' : B) (f : b --> b') : iscontr (Y f). Proof. assert (HH : isaprop (iscontr (Y f))). apply isapropiscontr. apply (p b (tpair (λ x, isaprop x) (iscontr (Y f)) HH)). intros [a0 h0]. apply (p b' (tpair (λ x, isaprop x) (iscontr (Y f)) HH)). intros [a0' h0']. exists (Y_inhab b b' f a0 h0 a0' h0'). apply Y_contr_eq. 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.