{a b c d : V} : [a, b] = [c, d] <-> (a = c) * (b = d). Proof. split. - intro p. assert (p1 : a = c). + assert (H : V_singleton a ∈ [c, d]). { apply (snd extensionality p). simpl. apply tr; exists true; reflexivity. } refine (Trunc_rec _ H). intros [t p']; destruct t. * apply ((ap V_singleton)^-1 p'^). * symmetry; apply (fst pair_eq_singleton p'). + split. * exact p1. * assert (H : hor (b = c) (b = d)). { assert (H' : V_pair a b ∈ [c, d]). { apply (snd extensionality p). apply tr; exists false; reflexivity. } refine (Trunc_rec _ H'). intros [t p']; destruct t. - apply tr; left. apply (fst pair_eq_singleton p'^). - destruct (path_V_eqimg p') as (H1, H2). generalize (H2 false); apply (Trunc_functor (-1)). intros [t p'']; destruct t. + left; exact p''^. + right; exact p''^. } refine (Trunc_rec _ H). intro case; destruct case as [p'| p']. 2: assumption. assert (H' : [a, b] = V_singleton (V_singleton b)). { apply (snd pair_eq_singleton). split. - apply ap; exact (p1 @ p'^). - apply (snd pair_eq_singleton). split; [exact (p1 @ p'^) | reflexivity]. } assert (H'' : V_pair c d = V_singleton b) by apply (fst pair_eq_singleton (p^ @ H')). symmetry; apply (fst pair_eq_singleton H''). - intros (p, p'). apply path_pair. split. + apply ap; exact p. + apply path_pair. split; assumption; assumption. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.