(x : V) (y : V) : HProp := Build_HProp (forall z : V, z ∈ x -> z ∈ y). Notation "x ⊆ y" := ( x y) : set_scope. Local bisim_aux (A : Type) (f : A -> V) (H_f : A -> V -> HProp) : V -> HProp. Proof. apply V_rec' with (fun B g _ => Build_HProp ( (forall a, hexists (fun b => H_f a (g b))) * forall b, hexists (fun a => H_f a (g b)) ) ). - exact _. - intros B B' g g' eq_img H_g H_g' H_img; simpl. apply path_iff_hprop; simpl. + intros [H1 H2]; split. * intro a. refine (Trunc_rec _ (H1 a)). intros [b H3]. generalize (fst eq_img b). unfold hexists. refine (@Trunc_functor (-1) {b0 : B' & g b = g' b0} {b0 : B' & H_f a (g' b0)} _). intros [b' p]. exists b'. exact (transport (fun x => H_f a x) p H3). * intro b'. refine (Trunc_rec _ (snd eq_img b')). intros [b p]. generalize (H2 b). apply (Trunc_functor (-1)). intros [a H3]. exists a. exact (transport (fun x => H_f a x) p H3). + intros [H1 H2]; split. * intro a. refine (Trunc_rec _ (H1 a)). intros [b' H3]. generalize (snd eq_img b'). apply (Trunc_functor (-1)). intros [b p]. exists b. exact (transport (fun x => H_f a x) p^ H3). * intro b. refine (Trunc_rec _ (fst eq_img b)). intros [b' p]. generalize (H2 b'). apply (Trunc_functor (-1)). intros [a H3]. exists a. exact (transport (fun x => H_f a x) p^ H3). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.