Require Import
  HoTT.Basics
  HoTT.Types
  HoTT.Universes.HSet
  HoTT.Truncations.Core
  HoTT.Colimits.Quotient
  HoTT.Projective.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** The following is an alternative (0,-1)-projectivity predicate on [A]. Given a family of quotient equivalence classes [f : forall x : A, B x / R x], for [R : forall x : A, Relation (B x)], we merely have a choice function [g : forall x, B x], factoring [f] as [f x = class_of (g x)]. *)

Definition HasQuotientChoice (A : Type) :=
  forall (B : A -> Type), (forall x, IsHSet (B x)) ->
  forall (R : forall x, Relation (B x))
         (pR : forall x, is_mere_relation (B x) (R x)),
         (forall x, Reflexive (R x)) ->
         (forall x, Symmetric (R x)) ->
         (forall x, Transitive (R x)) ->
  forall (f : forall x : A, B x / R x),
  hexists (fun g : (forall x : A, B x) =>
                   forall x, class_of (R x) (g x) = f x).

Section choose_has_quotient_choice.
  Context `{Univalence}
    {A : Type} {B : A -> Type} `{!forall x, IsHSet (B x)}
    (P : forall x, B x -> Type) `{!forall x (a : B x), IsHProp (P x a)}.

  Local Definition RelClassEquiv (x : A) (a : B x) (b : B x) : Type
    := P x a <~> P x b.

  Local Instance reflexive_relclass
    : forall x, Reflexive (RelClassEquiv x).
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
forall x : A, Reflexive (RelClassEquiv x)
  Proof.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
forall x : A, Reflexive (RelClassEquiv x)
    intros a b.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b: B a
RelClassEquiv a b b exact equiv_idmap.
  Qed.

  Local Instance symmetric_relclass
    : forall x, Symmetric (RelClassEquiv x).
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
forall x : A, Symmetric (RelClassEquiv x)
  Proof.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
forall x : A, Symmetric (RelClassEquiv x)
    intros a b1 b2 p.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1, b2: B a
p: RelClassEquiv a b1 b2
RelClassEquiv a b2 b1 exact (equiv_inverse p).
  Qed.

  Local Instance transitive_relclass
    : forall x, Transitive (RelClassEquiv x).
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
forall x : A, Transitive (RelClassEquiv x)
  Proof.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
forall x : A, Transitive (RelClassEquiv x)
    intros a b1 b2 b3 p q.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1, b2, b3: B a
p: RelClassEquiv a b1 b2
q: RelClassEquiv a b2 b3
RelClassEquiv a b1 b3 exact (equiv_compose q p).
  Qed.

  Local Instance hprop_choose_cod (a : A)
    : IsHProp {c : B a / RelClassEquiv a
                 | forall b, in_class (RelClassEquiv a) c b <~> P a b}.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
IsHProp
  {c : B a / RelClassEquiv a &
  forall b : B a,
  in_class (RelClassEquiv a) c b <~> P a b}
  Proof.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
IsHProp
  {c : B a / RelClassEquiv a &
  forall b : B a,
  in_class (RelClassEquiv a) c b <~> P a b}
    apply ishprop_sigma_disjoint.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
forall x y : B a / RelClassEquiv a,
(forall b : B a,
 in_class (RelClassEquiv a) x b <~> P a b) ->
(forall b : B a,
 in_class (RelClassEquiv a) y b <~> P a b) -> x = y
    refine (Quotient_ind_hprop _ _ _).
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
forall (a0 : B a) (y : B a / RelClassEquiv a),
(forall b : B a,
 in_class (RelClassEquiv a)
   (class_of (RelClassEquiv a) a0) b <~> P a b) ->
(forall b : B a,
 in_class (RelClassEquiv a) y b <~> P a b) ->
class_of (RelClassEquiv a) a0 = y
    intro b1.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1: B a
forall y : B a / RelClassEquiv a,
(forall b : B a,
 in_class (RelClassEquiv a)
   (class_of (RelClassEquiv a) b1) b <~> P a b) ->
(forall b : B a,
 in_class (RelClassEquiv a) y b <~> P a b) ->
class_of (RelClassEquiv a) b1 = y
    refine (Quotient_ind_hprop _ _ _).
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1: B a
forall a0 : B a,
(forall b : B a,
 in_class (RelClassEquiv a)
   (class_of (RelClassEquiv a) b1) b <~> P a b) ->
(forall b : B a,
 in_class (RelClassEquiv a)
   (class_of (RelClassEquiv a) a0) b <~> P a b) ->
class_of (RelClassEquiv a) b1 =
class_of (RelClassEquiv a) a0
    intros b2 f g.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1, b2: B a
f: forall b : B a,
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b1) b <~> P a b
g: forall b : B a,
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b2) b <~> P a b
class_of (RelClassEquiv a) b1 =
class_of (RelClassEquiv a) b2
    apply qglue.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1, b2: B a
f: forall b : B a,
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b1) b <~> P a b
g: forall b : B a,
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b2) b <~> P a b
RelClassEquiv a b1 b2
    apply (f b2)^-1.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1, b2: B a
f: forall b : B a,
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b1) b <~> P a b
g: forall b : B a,
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b2) b <~> P a b
P a b2
    apply g.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1, b2: B a
f: forall b : B a,
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b1) b <~> P a b
g: forall b : B a,
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b2) b <~> P a b
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b2) b2
    apply reflexive_relclass.
  Qed.

  Local Definition prechoose (i : forall x, hexists (P x)) (a : A)
    : {c : B a / RelClassEquiv a
         | forall b : B a, in_class (RelClassEquiv a) c b <~> P a b}.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
i: forall x : A, hexists (P x)
a: A
{c : B a / RelClassEquiv a &
forall b : B a,
in_class (RelClassEquiv a) c b <~> P a b}
  Proof.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
i: forall x : A, hexists (P x)
a: A
{c : B a / RelClassEquiv a &
forall b : B a,
in_class (RelClassEquiv a) c b <~> P a b}
    specialize (i a).
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
i: hexists (P a)
{c : B a / RelClassEquiv a &
forall b : B a,
in_class (RelClassEquiv a) c b <~> P a b}
    strip_truncations.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
i: {x : _ & P a x}
{c : B a / RelClassEquiv a &
forall b : B a,
in_class (RelClassEquiv a) c b <~> P a b}
    destruct i as [b1 h].
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1: B a
h: P a b1
{c : B a / RelClassEquiv a &
forall b : B a,
in_class (RelClassEquiv a) c b <~> P a b}
    exists (class_of _ b1).
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1: B a
h: P a b1
forall b : B a,
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b1) b <~> P a b
    intro b2.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1: B a
h: P a b1
b2: B a
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b1) b2 <~> P a b2
    apply equiv_iff_hprop.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1: B a
h: P a b1
b2: B a
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b1) b2 -> P a b2
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1: B a
h: P a b1
b2: B a
P a b2 ->
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b1) b2
    -
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1: B a
h: P a b1
b2: B a
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b1) b2 -> P a b2 intro f.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1: B a
h: P a b1
b2: B a
f: in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b1) b2
P a b2 exact (f h).
    -
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1: B a
h: P a b1
b2: B a
P a b2 ->
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b1) b2 intro p.
H: Univalence
A: Type
B: A -> Type
H0: forall x : A, IsHSet (B x)
P: forall x : A, B x -> Type
H1: forall (x : A) (a : B x), IsHProp (P x a)
a: A
b1: B a
h: P a b1
b2: B a
p: P a b2
in_class (RelClassEquiv a)
  (class_of (RelClassEquiv a) b1) b2 by apply equiv_iff_hprop.
  Defined.

  Local Definition choose (i : forall x, hexists (P x)) (a : A)
    : B a / RelClassEquiv a
    := (prechoose i a).1.

End choose_has_quotient_choice.

(** The following section derives [HasTrChoice 0 A] from [HasQuotientChoice A]. *)

Section has_tr0_choice_quotientchoice.
  Context `{Funext} (A : Type) (qch : HasQuotientChoice A).

  Local Definition RelUnit (B : A -> Type) (a : A) (b1 b2 : B a) : HProp
    := Build_HProp Unit.

  Local Instance reflexive_relunit (B : A -> Type) (a : A)
    : Reflexive (RelUnit B a).
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
Reflexive (fun b1 b2 : B a => RelUnit B a b1 b2)
  Proof.
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
Reflexive (fun b1 b2 : B a => RelUnit B a b1 b2)
    done.
  Qed.

  Local Instance symmetric_relunit (B : A -> Type) (a : A)
    : Symmetric (RelUnit B a).
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
Symmetric (fun b1 b2 : B a => RelUnit B a b1 b2)
  Proof.
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
Symmetric (fun b1 b2 : B a => RelUnit B a b1 b2)
    done.
  Qed.

  Local Instance transitive_relunit (B : A -> Type) (a : A)
    : Transitive (RelUnit B a).
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
Transitive (fun b1 b2 : B a => RelUnit B a b1 b2)
  Proof.
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
Transitive (fun b1 b2 : B a => RelUnit B a b1 b2)
    done.
  Qed.

  Local Instance ishprop_quotient_relunit (B : A -> Type) (a : A)
    : IsHProp (B a / RelUnit B a).
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
IsHProp (B a / (fun b1 b2 : B a => RelUnit B a b1 b2))
  Proof.
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
IsHProp (B a / (fun b1 b2 : B a => RelUnit B a b1 b2))
    apply hprop_allpath.
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
forall
x y : B a / (fun b1 b2 : B a => RelUnit B a b1 b2),
x = y
    refine (Quotient_ind_hprop _ _ _).
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
forall (a0 : B a)
(y : B a / (fun b1 b2 : B a => RelUnit B a b1 b2)),
class_of (fun b1 b2 : B a => RelUnit B a b1 b2) a0 = y
    intro r.
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
r: B a
forall
y : B a / (fun b1 b2 : B a => RelUnit B a b1 b2),
class_of (fun b1 b2 : B a => RelUnit B a b1 b2) r = y
    refine (Quotient_ind_hprop _ _ _).
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
r: B a
forall a0 : B a,
class_of (fun b1 b2 : B a => RelUnit B a b1 b2) r =
class_of (fun b1 b2 : B a => RelUnit B a b1 b2) a0
    intro s.
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
a: A
r, s: B a
class_of (fun b1 b2 : B a => RelUnit B a b1 b2) r =
class_of (fun b1 b2 : B a => RelUnit B a b1 b2) s
    by apply qglue.
  Qed.

  Lemma has_tr0_choice_quotientchoice : HasTrChoice 0 A.
H: Funext
A: Type
qch: HasQuotientChoice A
HasTrChoice 0 A
  Proof.
H: Funext
A: Type
qch: HasQuotientChoice A
HasTrChoice 0 A
    intros B sB f.
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
sB: forall x : A,
ReflectiveSubuniverse.In (Tr 0) (B x)
f: forall x : A, merely (B x)
merely (forall x : A, B x)
    transparent assert (g : (forall a, B a / RelUnit B a)).
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
sB: forall x : A,
ReflectiveSubuniverse.In (Tr 0) (B x)
f: forall x : A, merely (B x)
forall a : A,
B a / (fun b1 b2 : B a => RelUnit B a b1 b2)
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
sB: forall x : A,
ReflectiveSubuniverse.In (Tr 0) (B x)
f: forall x : A, merely (B x)
g:= ?Goal: forall a : A,
B a / (fun b1 b2 : B a => RelUnit B a b1 b2)
merely (forall x : A, B x)
    -
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
sB: forall x : A,
ReflectiveSubuniverse.In (Tr 0) (B x)
f: forall x : A, merely (B x)
forall a : A,
B a / (fun b1 b2 : B a => RelUnit B a b1 b2) intro a.
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
sB: forall x : A,
ReflectiveSubuniverse.In (Tr 0) (B x)
f: forall x : A, merely (B x)
a: A
B a / (fun b1 b2 : B a => RelUnit B a b1 b2)
      specialize (f a).
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
sB: forall x : A,
ReflectiveSubuniverse.In (Tr 0) (B x)
a: A
f: merely (B a)
B a / (fun b1 b2 : B a => RelUnit B a b1 b2)
      strip_truncations.
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
sB: forall x : A,
ReflectiveSubuniverse.In (Tr 0) (B x)
a: A
f: B a
B a / (fun b1 b2 : B a => RelUnit B a b1 b2)
      exact (class_of _ f).
    -
H: Funext
A: Type
qch: HasQuotientChoice A
B: A -> Type
sB: forall x : A,
ReflectiveSubuniverse.In (Tr 0) (B x)
f: forall x : A, merely (B x)
g:= fun a : A =>
let f := f a in
Trunc_ind
  (fun _ : Trunc (-1) (B a) =>
   B a / (fun b1 b2 : B a => RelUnit B a b1 b2))
  (fun f0 : B a =>
   class_of (fun b1 b2 : B a => RelUnit B a b1 b2)
     f0) f: forall a : A,
B a / (fun b1 b2 : B a => RelUnit B a b1 b2)
merely (forall x : A, B x) specialize (qch B _ (RelUnit B) _ _ _ _ g).
H: Funext
A: Type
B: A -> Type
f: forall x : A, merely (B x)
g:= fun a : A =>
let f := f a in
Trunc_ind
  (fun _ : Trunc (-1) (B a) =>
   B a / (fun b1 b2 : B a => RelUnit B a b1 b2))
  (fun f0 : B a =>
   class_of (fun b1 b2 : B a => RelUnit B a b1 b2)
     f0) f: forall a : A,
B a / (fun b1 b2 : B a => RelUnit B a b1 b2)
qch: hexists
(fun g0 : forall x : A, B x =>
forall x : A,
class_of
((fun (a : A) (b1 b2 : B a) => trunctype_type (RelUnit B a b1 b2)) x)
(g0 x) = g x)
sB: forall x : A,
ReflectiveSubuniverse.In (Tr 0) (B x)
merely (forall x : A, B x)
      strip_truncations.
H: Funext
A: Type
B: A -> Type
f: forall x : A, merely (B x)
g:= fun a : A =>
let f := f a in
Trunc_ind
  (fun _ : Trunc (-1) (B a) =>
   B a / (fun b1 b2 : B a => RelUnit B a b1 b2))
  (fun f0 : B a =>
   class_of (fun b1 b2 : B a => RelUnit B a b1 b2)
     f0) f: forall a : A,
B a / (fun b1 b2 : B a => RelUnit B a b1 b2)
sB: forall x : A,
ReflectiveSubuniverse.In (Tr 0) (B x)
qch: {g0 : forall x : A, B x &
forall x : A, class_of (fun b1 b2 : B x => RelUnit B x b1 b2) (g0 x) = g x}
merely (forall x : A, B x)
      apply tr.
H: Funext
A: Type
B: A -> Type
f: forall x : A, merely (B x)
g:= fun a : A =>
let f := f a in
Trunc_ind
  (fun _ : Trunc (-1) (B a) =>
   B a / (fun b1 b2 : B a => RelUnit B a b1 b2))
  (fun f0 : B a =>
   class_of (fun b1 b2 : B a => RelUnit B a b1 b2)
     f0) f: forall a : A,
B a / (fun b1 b2 : B a => RelUnit B a b1 b2)
sB: forall x : A,
ReflectiveSubuniverse.In (Tr 0) (B x)
qch: {g0 : forall x : A, B x &
forall x : A, class_of (fun b1 b2 : B x => RelUnit B x b1 b2) (g0 x) = g x}
forall x : A, B x
      apply qch.
  Qed.

End has_tr0_choice_quotientchoice.

Lemma has_quotient_choice_tr0choice (A : Type)
  : HasTrChoice 0 A -> HasQuotientChoice A.
A: Type
HasTrChoice 0 A -> HasQuotientChoice A
Proof.
A: Type
HasTrChoice 0 A -> HasQuotientChoice A
  intros ch B sB R pR rR sR tR f.
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
hexists
  (fun g : forall x : A, B x =>
   forall x : A, class_of (R x) (g x) = f x)
  set (P := fun a b => class_of (R a) b = f a).
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
hexists
  (fun g : forall x : A, B x =>
   forall x : A, class_of (R x) (g x) = f x)
  assert (forall a, merely ((fun x => {b | P x b}) a)) as g.
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
forall a : A, merely {b : B a & P a b}
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
g: forall a : A,
merely ((fun x : A => {b : B x & P x b}) a)
hexists
  (fun g : forall x : A, B x =>
   forall x : A, class_of (R x) (g x) = f x)
  -
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
forall a : A, merely {b : B a & P a b} intro a.
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
a: A
merely {b : B a & P a b}
    refine (Quotient_ind_hprop _
              (fun c => merely {b | class_of (R a) b = c}) _ (f a)).
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
a: A
forall a0 : B a,
merely
  {b : B a & class_of (R a) b = class_of (R a) a0}
    intro b.
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
a: A
b: B a
merely
  {b0 : B a & class_of (R a) b0 = class_of (R a) b}
    apply tr.
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
a: A
b: B a
{b0 : B a & class_of (R a) b0 = class_of (R a) b}
    by exists b.
  -
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
g: forall a : A,
merely ((fun x : A => {b : B x & P x b}) a)
hexists
  (fun g : forall x : A, B x =>
   forall x : A, class_of (R x) (g x) = f x) pose proof (ch (fun a => {b | P a b}) _ g) as h.
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
g: forall a : A,
merely ((fun x : A => {b : B x & P x b}) a)
h: merely
  (forall x : A,
   (fun a : A => {b : B a & P a b}) x)
hexists
  (fun g : forall x : A, B x =>
   forall x : A, class_of (R x) (g x) = f x)
    strip_truncations.
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
g: forall a : A,
merely ((fun x : A => {b : B x & P x b}) a)
h: forall x : A, {b : B x & P x b}
hexists
  (fun g : forall x : A, B x =>
   forall x : A, class_of (R x) (g x) = f x)
    apply tr.
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
g: forall a : A,
merely ((fun x : A => {b : B x & P x b}) a)
h: forall x : A, {b : B x & P x b}
{g : forall x : A, B x &
forall x : A, class_of (R x) (g x) = f x}
    exists (fun x => (h x).1).
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
g: forall a : A,
merely ((fun x : A => {b : B x & P x b}) a)
h: forall x : A, {b : B x & P x b}
forall x : A, class_of (R x) (h x).1 = f x
    intro a.
A: Type
ch: HasTrChoice 0 A
B: A -> Type
sB: forall x : A, IsHSet (B x)
R: forall x : A, Relation (B x)
pR: forall (x : A) (x0 y : B x), IsHProp (R x x0 y)
rR: forall x : A, Reflexive (R x)
sR: forall x : A, Symmetric (R x)
tR: forall x : A, Transitive (R x)
f: forall x : A, B x / R x
P:= fun (a : A) (b : B a) => class_of (R a) b = f a: forall a : A, B a -> Type
g: forall a : A,
merely ((fun x : A => {b : B x & P x b}) a)
h: forall x : A, {b : B x & P x b}
a: A
class_of (R a) (h a).1 = f a
    apply h.
Qed.

Instance isequiv_has_tr0_choice_to_has_quotient_choice
  `{Funext} (A : Type)
  : IsEquiv (has_quotient_choice_tr0choice A).
H: Funext
A: Type
IsEquiv (has_quotient_choice_tr0choice A)
Proof.
H: Funext
A: Type
IsEquiv (has_quotient_choice_tr0choice A)
  srapply isequiv_iff_hprop.
H: Funext
A: Type
IsHProp (HasTrChoice 0 A)
H: Funext
A: Type
HasQuotientChoice A -> HasTrChoice 0 A
  -
H: Funext
A: Type
IsHProp (HasTrChoice 0 A) exact istrunc_forall.
  -
H: Funext
A: Type
HasQuotientChoice A -> HasTrChoice 0 A apply has_tr0_choice_quotientchoice.
Qed.

Definition equiv_has_tr0_choice_has_quotient_choice
  `{Funext} (A : Type)
  : HasTrChoice 0 A <~> HasQuotientChoice A
  := Build_Equiv _ _ (has_quotient_choice_tr0choice A) _.

(** The next section uses [has_quotient_choice_tr0choice] to generalize [quotient_rec2], see [choose_quotient_ind] below. *)

Section choose_quotient_ind.
  Context `{Univalence}
    {I : Type} `{!HasTrChoice 0 I}
    {A : I -> Type} `{!forall i, IsHSet (A i)}
    (R : forall i, Relation (A i))
    `{!forall i, is_mere_relation (A i) (R i)}
    {rR : forall i, Reflexive (R i)}
    {sR : forall i, Symmetric (R i)}
    {tR : forall i, Transitive (R i)}.

(** First generalize the [qglue] constructor. *)

  Lemma qglue_forall
    (f g : forall i, A i) (r : forall i, R i (f i) (g i))
    : (fun i => class_of (R i) (f i)) = (fun i => class_of (R i) (g i)).
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
f, g: forall i : I, A i
r: forall i : I, R i (f i) (g i)
(fun i : I => class_of (R i) (f i)) =
(fun i : I => class_of (R i) (g i))
  Proof.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
f, g: forall i : I, A i
r: forall i : I, R i (f i) (g i)
(fun i : I => class_of (R i) (f i)) =
(fun i : I => class_of (R i) (g i))
    funext s.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
f, g: forall i : I, A i
r: forall i : I, R i (f i) (g i)
s: I
class_of (R s) (f s) = class_of (R s) (g s)
    by apply qglue.
  Defined.

(** Given suitable preconditions, we will show that [ChooseProp P a g] is inhabited, rather than directly giving an inhabitant of [P g]. This turns out to be beneficial because [ChooseProp P a g] is a proposition. *)

  Local Definition ChooseProp
    (P : (forall i, A i / R i) -> Type) `{!forall g, IsHSet (P g)}
    (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i)))
    (g : forall i, A i / R i)
    : Type
    := {b : P g
       | merely (exists (f : forall i, A i)
                        (q : g = fun i => class_of (R i) (f i)),
                 forall (f' : forall i, A i)
                        (r : forall i, R i (f i) (f' i)),
                 qglue_forall f f' r # q # b = a f')}.

  Local Instance ishprop_choose_quotient_ind_chooseprop
    (P : (forall i, A i / R i) -> Type) `{!forall g, IsHSet (P g)}
    (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i)))
    (g : forall i, A i / R i)
    : IsHProp (ChooseProp P a g).
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
IsHProp (ChooseProp P a g)
  Proof.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
IsHProp (ChooseProp P a g)
    apply ishprop_sigma_disjoint.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
forall x y : P g,
merely
  {f : forall i : I, A i &
  {q : g = (fun i : I => class_of (R i) (f i)) &
  forall (f' : forall i : I, A i)
  (r : forall i : I, R i (f i) (f' i)),
  transport P (qglue_forall f f' r) (transport P q x) =
  a f'}} ->
merely
  {f : forall i : I, A i &
  {q : g = (fun i : I => class_of (R i) (f i)) &
  forall (f' : forall i : I, A i)
  (r : forall i : I, R i (f i) (f' i)),
  transport P (qglue_forall f f' r) (transport P q y) =
  a f'}} -> x = y
    intros x y h1 h2.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
h1: merely
  {f : forall i : I, A i &
  {q : g = (fun i : I => class_of (R i) (f i)) &
  forall (f' : forall i : I, A i)
  (r : forall i : I, R i (f i) (f' i)),
  transport P (qglue_forall f f' r)
    (transport P q x) = 
  a f'}}
h2: merely
  {f : forall i : I, A i &
  {q : g = (fun i : I => class_of (R i) (f i)) &
  forall (f' : forall i : I, A i)
  (r : forall i : I, R i (f i) (f' i)),
  transport P (qglue_forall f f' r)
    (transport P q y) = 
  a f'}}
x = y
    strip_truncations.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
h2: {f : forall i : I, A i &
{q : g = (fun i : I => class_of (R i) (f i)) &
forall (f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r)
  (transport P q y) = 
a f'}}
h1: {f : forall i : I, A i &
{q : g = (fun i : I => class_of (R i) (f i)) &
forall (f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r)
  (transport P q x) = 
a f'}}
x = y
    destruct h1 as [f1 [q1 p1]].
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
h2: {f : forall i : I, A i &
{q : g = (fun i : I => class_of (R i) (f i)) &
forall (f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r)
  (transport P q y) = 
a f'}}
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
p1: forall (f' : forall i : I, A i)
(r : forall i : I, R i (f1 i) (f' i)),
transport P (qglue_forall f1 f' r)
  (transport P q1 x) = 
a f'
x = y
    destruct h2 as [f2 [q2 p2]].
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
p2: forall (f' : forall i : I, A i)
(r : forall i : I, R i (f2 i) (f' i)),
transport P (qglue_forall f2 f' r)
  (transport P q2 y) = 
a f'
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
p1: forall (f' : forall i : I, A i)
(r : forall i : I, R i (f1 i) (f' i)),
transport P (qglue_forall f1 f' r)
  (transport P q1 x) = 
a f'
x = y
    specialize (p1 f1 (fun i => rR i (f1 i))).
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
p2: forall (f' : forall i : I, A i)
(r : forall i : I, R i (f2 i) (f' i)),
transport P (qglue_forall f2 f' r)
  (transport P q2 y) = 
a f'
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
p1: transport P
  (qglue_forall f1 f1 (fun i : I => rR i (f1 i)))
  (transport P q1 x) = 
a f1
x = y
    set (pR := fun i =>
                related_quotient_paths (R i) _ _ (ap (fun h => h i) q2^
                @ ap (fun h => h i) q1)).
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
p2: forall (f' : forall i : I, A i)
(r : forall i : I, R i (f2 i) (f' i)),
transport P (qglue_forall f2 f' r)
  (transport P q2 y) = 
a f'
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
p1: transport P
  (qglue_forall f1 f1 (fun i : I => rR i (f1 i)))
  (transport P q1 x) = 
a f1
pR:= fun i : I =>
related_quotient_paths 
  (R i) (f2 i) (f1 i)
  (ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q2^ @
   ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q1): forall i : I, R i (f2 i) (f1 i)
x = y
    specialize (p2 f1 pR).
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
pR:= fun i : I =>
related_quotient_paths 
  (R i) (f2 i) (f1 i)
  (ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q2^ @
   ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q1): forall i : I, R i (f2 i) (f1 i)
p2: transport P (qglue_forall f2 f1 pR)
  (transport P q2 y) = 
a f1
p1: transport P
  (qglue_forall f1 f1 (fun i : I => rR i (f1 i)))
  (transport P q1 x) = 
a f1
x = y
    do 2 apply moveL_transport_V in p1.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
pR:= fun i : I =>
related_quotient_paths 
  (R i) (f2 i) (f1 i)
  (ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q2^ @
   ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q1): forall i : I, R i (f2 i) (f1 i)
p2: transport P (qglue_forall f2 f1 pR)
  (transport P q2 y) = 
a f1
p1: x =
transport P q1^
  (transport P
     (qglue_forall f1 f1
        (fun i : I => rR i (f1 i)))^ 
     (a f1))
x = y
    do 2 apply moveL_transport_V in p2.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
pR:= fun i : I =>
related_quotient_paths 
  (R i) (f2 i) (f1 i)
  (ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q2^ @
   ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q1): forall i : I, R i (f2 i) (f1 i)
p2: y =
transport P q2^
  (transport P (qglue_forall f2 f1 pR)^ (a f1))
p1: x =
transport P q1^
  (transport P
     (qglue_forall f1 f1
        (fun i : I => rR i (f1 i)))^ 
     (a f1))
x = y
    refine (p1 @ _ @ p2^).
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
pR:= fun i : I =>
related_quotient_paths 
  (R i) (f2 i) (f1 i)
  (ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q2^ @
   ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q1): forall i : I, R i (f2 i) (f1 i)
p2: y =
transport P q2^
  (transport P (qglue_forall f2 f1 pR)^ (a f1))
p1: x =
transport P q1^
  (transport P
     (qglue_forall f1 f1
        (fun i : I => rR i (f1 i)))^ 
     (a f1))
transport P q1^
  (transport P
     (qglue_forall f1 f1 (fun i : I => rR i (f1 i)))^
     (a f1)) =
transport P q2^
  (transport P (qglue_forall f2 f1 pR)^ (a f1))
    apply moveR_transport_p.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
pR:= fun i : I =>
related_quotient_paths 
  (R i) (f2 i) (f1 i)
  (ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q2^ @
   ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q1): forall i : I, R i (f2 i) (f1 i)
p2: y =
transport P q2^
  (transport P (qglue_forall f2 f1 pR)^ (a f1))
p1: x =
transport P q1^
  (transport P
     (qglue_forall f1 f1
        (fun i : I => rR i (f1 i)))^ 
     (a f1))
transport P
  (qglue_forall f1 f1 (fun i : I => rR i (f1 i)))^
  (a f1) =
transport P (q1^)^
  (transport P q2^
     (transport P (qglue_forall f2 f1 pR)^ (a f1)))
    rewrite inv_V.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
pR:= fun i : I =>
related_quotient_paths 
  (R i) (f2 i) (f1 i)
  (ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q2^ @
   ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q1): forall i : I, R i (f2 i) (f1 i)
p2: y =
transport P q2^
  (transport P (qglue_forall f2 f1 pR)^ (a f1))
p1: x =
transport P q1^
  (transport P
     (qglue_forall f1 f1
        (fun i : I => rR i (f1 i)))^ 
     (a f1))
transport P
  (qglue_forall f1 f1 (fun i : I => rR i (f1 i)))^
  (a f1) =
transport P q1
  (transport P q2^
     (transport P (qglue_forall f2 f1 pR)^ (a f1)))
    rewrite <- transport_pp.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
pR:= fun i : I =>
related_quotient_paths 
  (R i) (f2 i) (f1 i)
  (ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q2^ @
   ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q1): forall i : I, R i (f2 i) (f1 i)
p2: y =
transport P q2^
  (transport P (qglue_forall f2 f1 pR)^ (a f1))
p1: x =
transport P q1^
  (transport P
     (qglue_forall f1 f1
        (fun i : I => rR i (f1 i)))^ 
     (a f1))
transport P
  (qglue_forall f1 f1 (fun i : I => rR i (f1 i)))^
  (a f1) =
transport P (q2^ @ q1)
  (transport P (qglue_forall f2 f1 pR)^ (a f1))
    apply moveR_transport_p.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
pR:= fun i : I =>
related_quotient_paths 
  (R i) (f2 i) (f1 i)
  (ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q2^ @
   ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q1): forall i : I, R i (f2 i) (f1 i)
p2: y =
transport P q2^
  (transport P (qglue_forall f2 f1 pR)^ (a f1))
p1: x =
transport P q1^
  (transport P
     (qglue_forall f1 f1
        (fun i : I => rR i (f1 i)))^ 
     (a f1))
a f1 =
transport P
  ((qglue_forall f1 f1 (fun i : I => rR i (f1 i)))^)^
  (transport P (q2^ @ q1)
     (transport P (qglue_forall f2 f1 pR)^ (a f1)))
    rewrite inv_V.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
pR:= fun i : I =>
related_quotient_paths 
  (R i) (f2 i) (f1 i)
  (ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q2^ @
   ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q1): forall i : I, R i (f2 i) (f1 i)
p2: y =
transport P q2^
  (transport P (qglue_forall f2 f1 pR)^ (a f1))
p1: x =
transport P q1^
  (transport P
     (qglue_forall f1 f1
        (fun i : I => rR i (f1 i)))^ 
     (a f1))
a f1 =
transport P
  (qglue_forall f1 f1 (fun i : I => rR i (f1 i)))
  (transport P (q2^ @ q1)
     (transport P (qglue_forall f2 f1 pR)^ (a f1)))
    do 2 rewrite <- transport_pp.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
pR:= fun i : I =>
related_quotient_paths 
  (R i) (f2 i) (f1 i)
  (ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q2^ @
   ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q1): forall i : I, R i (f2 i) (f1 i)
p2: y =
transport P q2^
  (transport P (qglue_forall f2 f1 pR)^ (a f1))
p1: x =
transport P q1^
  (transport P
     (qglue_forall f1 f1
        (fun i : I => rR i (f1 i)))^ 
     (a f1))
a f1 =
transport P
  ((qglue_forall f2 f1 pR)^ @
   ((q2^ @ q1) @
    qglue_forall f1 f1 (fun i : I => rR i (f1 i))))
  (a f1)
    set (pa := (qglue_forall f2 f1 pR)^
               @ (q2^ @ q1 @ qglue_forall f1 f1 _)).
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
x, y: P g
f2: forall i : I, A i
q2: g = (fun i : I => class_of (R i) (f2 i))
f1: forall i : I, A i
q1: g = (fun i : I => class_of (R i) (f1 i))
pR:= fun i : I =>
related_quotient_paths 
  (R i) (f2 i) (f1 i)
  (ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q2^ @
   ap (fun h : forall x0 : I, A x0 / R x0 => h i)
     q1): forall i : I, R i (f2 i) (f1 i)
p2: y =
transport P q2^
  (transport P (qglue_forall f2 f1 pR)^ (a f1))
p1: x =
transport P q1^
  (transport P
     (qglue_forall f1 f1
        (fun i : I => rR i (f1 i)))^ 
     (a f1))
pa:= (qglue_forall f2 f1 pR)^ @
((q2^ @ q1) @
 qglue_forall f1 f1 (fun i : I => rR i (f1 i))): (fun i : I => class_of (R i) (f1 i)) =
(fun i : I => class_of (R i) (f1 i))
a f1 = transport P pa (a f1)
    by induction (hset_path2 idpath pa).
  Qed.

(* Since [ChooseProp P a g] is a proposition, we can apply [has_quotient_choice_tr0choice] and strip its truncation in order to derive [ChooseProp P a g]. *)

  Lemma chooseprop_quotient_ind
    (P : (forall i, A i / R i) -> Type) `{!forall g, IsHSet (P g)}
    (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i)))
    (E : forall (f f' : forall i, A i) (r : forall i, R i (f i) (f' i)),
         qglue_forall f f' r # a f = a f')
    (g : forall i, A i / R i)
    : ChooseProp P a g.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
ChooseProp P a g
  Proof.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
ChooseProp P a g
    pose proof
      (has_quotient_choice_tr0choice I _ A _ R _ _ _ _ g) as h.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
h: hexists
  (fun g0 : forall x : I, A x =>
   forall x : I, class_of (R x) (g0 x) = g x)
ChooseProp P a g
    strip_truncations.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
h: {g0 : forall x : I, A x &
forall x : I, class_of (R x) (g0 x) = g x}
ChooseProp P a g
    destruct h as [h p].
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
h: forall x : I, A x
p: forall x : I, class_of (R x) (h x) = g x
ChooseProp P a g
    apply path_forall in p.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
h: forall x : I, A x
p: (fun x : I => class_of (R x) (h x)) = g
ChooseProp P a g
    refine (transport _ p _).
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
h: forall x : I, A x
p: (fun x : I => class_of (R x) (h x)) = g
ChooseProp P a (fun x : I => class_of (R x) (h x))
    exists (a h).
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
h: forall x : I, A x
p: (fun x : I => class_of (R x) (h x)) = g
merely
  {f : forall i : I, A i &
  {q
  : (fun x : I => class_of (R x) (h x)) =
    (fun i : I => class_of (R i) (f i)) &
  forall (f' : forall i : I, A i)
  (r : forall i : I, R i (f i) (f' i)),
  transport P (qglue_forall f f' r)
    (transport P q (a h)) = a f'}}
    apply tr.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
h: forall x : I, A x
p: (fun x : I => class_of (R x) (h x)) = g
{f : forall i : I, A i &
{q
: (fun x : I => class_of (R x) (h x)) =
  (fun i : I => class_of (R i) (f i)) &
forall (f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r)
  (transport P q (a h)) = a f'}}
    exists h.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
h: forall x : I, A x
p: (fun x : I => class_of (R x) (h x)) = g
{q
: (fun x : I => class_of (R x) (h x)) =
  (fun i : I => class_of (R i) (h i)) &
forall (f' : forall i : I, A i)
(r : forall i : I, R i (h i) (f' i)),
transport P (qglue_forall h f' r)
  (transport P q (a h)) = a f'}
    exists 1.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
h: forall x : I, A x
p: (fun x : I => class_of (R x) (h x)) = g
forall (f' : forall i : I, A i)
(r : forall i : I, R i (h i) (f' i)),
transport P (qglue_forall h f' r)
  (transport P 1 (a h)) = a f'
    apply E.
  Defined.

(** By projecting out of [chooseprop_quotient_ind] we obtain a generalization of [quotient_rec2]. *)

  Lemma choose_quotient_ind
    (P : (forall i, A i / R i) -> Type) `{!forall g, IsHSet (P g)}
    (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i)))
    (E : forall (f f' : forall i, A i) (r : forall i, R i (f i) (f' i)),
         qglue_forall f f' r # a f = a f')
    (g : forall i, A i / R i)
    : P g.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
P g
  Proof.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
g: forall i : I, A i / R i
P g
    exact (chooseprop_quotient_ind P a E g).1.
  Defined.

(** A specialization of [choose_quotient_ind] to the case where [P g] is a proposition. *)

  Lemma choose_quotient_ind_prop
    (P : (forall i, A i / R i) -> Type) `{!forall g, IsHProp (P g)}
    (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i)))
    (g : forall i, A i / R i)
    : P g.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHProp (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
P g
  Proof.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHProp (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
P g
    refine (choose_quotient_ind P a _ g).
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHProp (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f' intros.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHProp (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
g: forall i : I, A i / R i
f, f': forall i : I, A i
r: forall i : I, R i (f i) (f' i)
transport P (qglue_forall f f' r) (a f) = a f' apply path_ishprop.
  Defined.

(** The recursion principle derived from [choose_quotient_ind]. *)

  Definition choose_quotient_rec
    {B : Type} `{!IsHSet B} (a : (forall i, A i) -> B)
    (E : forall (f f' : forall i, A i),
         (forall i, R i (f i) (f' i)) -> a f = a f')
    (g : forall i, A i / R i)
    : B
    := choose_quotient_ind (fun _ => B) a
        (fun f f' r => transport_const _ _ @ E f f' r) g.

(** The "beta-rule" of [choose_quotient_ind]. *)

  Lemma choose_quotient_ind_compute
    (P : (forall i, A i / R i) -> Type) `{!forall g, IsHSet (P g)}
    (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i)))
    (E : forall (f f' : forall i, A i) (r : forall i, R i (f i) (f' i)),
         qglue_forall f f' r # a f = a f')
    (f : forall i, A i)
    : choose_quotient_ind P a E (fun i => class_of (R i) (f i)) = a f.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f: forall i : I, A i
choose_quotient_ind P a E
  (fun i : I => class_of (R i) (f i)) = a f
  Proof.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f: forall i : I, A i
choose_quotient_ind P a E
  (fun i : I => class_of (R i) (f i)) = a f
    refine (Trunc_ind (fun a => (_ a).1 = _) _ _).
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f: forall i : I, A i
forall
a0 : {g : forall x : I, A x &
     forall x : I,
     class_of (R x) (g x) = class_of (R x) (f x)},
(Trunc_ind
   (fun
      _ : Trunc (-1)
            {g : forall x : I, A x &
            forall x : I,
            class_of (R x) (g x) =
            class_of (R x) (f x)} =>
    ChooseProp P a (fun i : I => class_of (R i) (f i)))
   (fun
      h : {g : forall x : I, A x &
          forall x : I,
          class_of (R x) (g x) = class_of (R x) (f x)}
    =>
    transport (ChooseProp P a)
      (path_forall
         (fun x : I => class_of (R x) (h.1 x))
         (fun i : I => class_of (R i) (f i)) h.2)
      (a h.1; tr (h.1; 1; E h.1))) (tr a0)).1 = a f cbn.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f: forall i : I, A i
forall
a0 : {g : forall x : I, A x &
     forall x : I,
     class_of (R x) (g x) = class_of (R x) (f x)},
(transport (ChooseProp P a)
   (path_forall (fun x : I => class_of (R x) (a0.1 x))
      (fun i : I => class_of (R i) (f i)) a0.2)
   (a a0.1; tr (a0.1; 1; E a0.1))).1 = a f
    intros [f' p].
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f, f': forall x : I, A x
p: forall x : I,
class_of (R x) (f' x) = class_of (R x) (f x)
(transport (ChooseProp P a)
   (path_forall (fun x : I => class_of (R x) (f' x))
      (fun i : I => class_of (R i) (f i)) p)
   (a f'; tr (f'; 1; E f'))).1 = a f
    rewrite transport_sigma.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f, f': forall x : I, A x
p: forall x : I,
class_of (R x) (f' x) = class_of (R x) (f x)
(transport P
   (path_forall (fun x : I => class_of (R x) (f' x))
      (fun i : I => class_of (R i) (f i)) p)
   (a f'; tr (f'; 1; E f')).1;
transportD P
  (fun (x : forall x : I, A x / R x) (y : P x) =>
   merely
     {f : forall i : I, A i &
     {q : x = (fun i : I => class_of (R i) (f i)) &
     forall (f' : forall i : I, A i)
     (r : forall i : I, R i (f i) (f' i)),
     transport P (qglue_forall f f' r)
       (transport P q y) = a f'}})
  (path_forall (fun x : I => class_of (R x) (f' x))
     (fun i : I => class_of (R i) (f i)) p)
  (a f'; tr (f'; 1; E f')).1
  (a f'; tr (f'; 1; E f')).2).1 = a f
    set (p' := fun x => related_quotient_paths (R x) _ _ (p x)).
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f, f': forall x : I, A x
p: forall x : I,
class_of (R x) (f' x) = class_of (R x) (f x)
p':= fun x : I =>
related_quotient_paths (R x) (f' x) (f x) (p x): forall x : I, R x (f' x) (f x)
(transport P
   (path_forall (fun x : I => class_of (R x) (f' x))
      (fun i : I => class_of (R i) (f i)) p)
   (a f'; tr (f'; 1; E f')).1;
transportD P
  (fun (x : forall x : I, A x / R x) (y : P x) =>
   merely
     {f : forall i : I, A i &
     {q : x = (fun i : I => class_of (R i) (f i)) &
     forall (f' : forall i : I, A i)
     (r : forall i : I, R i (f i) (f' i)),
     transport P (qglue_forall f f' r)
       (transport P q y) = a f'}})
  (path_forall (fun x : I => class_of (R x) (f' x))
     (fun i : I => class_of (R i) (f i)) p)
  (a f'; tr (f'; 1; E f')).1
  (a f'; tr (f'; 1; E f')).2).1 = a f
    assert (p = (fun i => qglue (p' i))) as pE.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f, f': forall x : I, A x
p: forall x : I,
class_of (R x) (f' x) = class_of (R x) (f x)
p':= fun x : I =>
related_quotient_paths (R x) (f' x) (f x) (p x): forall x : I, R x (f' x) (f x)
p = (fun i : I => qglue (p' i))
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f, f': forall x : I, A x
p: forall x : I,
class_of (R x) (f' x) = class_of (R x) (f x)
p':= fun x : I =>
related_quotient_paths (R x) (f' x) (f x) (p x): forall x : I, R x (f' x) (f x)
pE: p = (fun i : I => qglue (p' i))
(transport P
   (path_forall (fun x : I => class_of (R x) (f' x))
      (fun i : I => class_of (R i) (f i)) p)
   (a f'; tr (f'; 1; E f')).1;
transportD P
  (fun (x : forall x : I, A x / R x) (y : P x) =>
   merely
     {f : forall i : I, A i &
     {q : x = (fun i : I => class_of (R i) (f i)) &
     forall (f' : forall i : I, A i)
     (r : forall i : I, R i (f i) (f' i)),
     transport P (qglue_forall f f' r)
       (transport P q y) = 
     a f'}})
  (path_forall (fun x : I => class_of (R x) (f' x))
     (fun i : I => class_of (R i) (f i)) p)
  (a f'; tr (f'; 1; E f')).1
  (a f'; tr (f'; 1; E f')).2).1 = 
a f
    -
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f, f': forall x : I, A x
p: forall x : I,
class_of (R x) (f' x) = class_of (R x) (f x)
p':= fun x : I =>
related_quotient_paths (R x) (f' x) (f x) (p x): forall x : I, R x (f' x) (f x)
p = (fun i : I => qglue (p' i)) funext x.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f, f': forall x : I, A x
p: forall x : I,
class_of (R x) (f' x) = class_of (R x) (f x)
p':= fun x : I =>
related_quotient_paths (R x) (f' x) (f x) (p x): forall x : I, R x (f' x) (f x)
x: I
p x = qglue (p' x) apply hset_path2.
    -
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f, f': forall x : I, A x
p: forall x : I,
class_of (R x) (f' x) = class_of (R x) (f x)
p':= fun x : I =>
related_quotient_paths (R x) (f' x) (f x) (p x): forall x : I, R x (f' x) (f x)
pE: p = (fun i : I => qglue (p' i))
(transport P
   (path_forall (fun x : I => class_of (R x) (f' x))
      (fun i : I => class_of (R i) (f i)) p)
   (a f'; tr (f'; 1; E f')).1;
transportD P
  (fun (x : forall x : I, A x / R x) (y : P x) =>
   merely
     {f : forall i : I, A i &
     {q : x = (fun i : I => class_of (R i) (f i)) &
     forall (f' : forall i : I, A i)
     (r : forall i : I, R i (f i) (f' i)),
     transport P (qglue_forall f f' r)
       (transport P q y) = a f'}})
  (path_forall (fun x : I => class_of (R x) (f' x))
     (fun i : I => class_of (R i) (f i)) p)
  (a f'; tr (f'; 1; E f')).1
  (a f'; tr (f'; 1; E f')).2).1 = a f rewrite pE.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
P: (forall i : I, A i / R i) -> Type
H2: forall g : forall i : I, A i / R i, IsHSet (P g)
a: forall f : forall i : I, A i,
P (fun i : I => class_of (R i) (f i))
E: forall (f f' : forall i : I, A i)
(r : forall i : I, R i (f i) (f' i)),
transport P (qglue_forall f f' r) (a f) = a f'
f, f': forall x : I, A x
p: forall x : I,
class_of (R x) (f' x) = class_of (R x) (f x)
p':= fun x : I =>
related_quotient_paths (R x) (f' x) (f x) (p x): forall x : I, R x (f' x) (f x)
pE: p = (fun i : I => qglue (p' i))
(transport P
   (path_forall (fun x : I => class_of (R x) (f' x))
      (fun i : I => class_of (R i) (f i))
      (fun i : I => qglue (p' i)))
   (a f'; tr (f'; 1; E f')).1;
transportD P
  (fun (x : forall x : I, A x / R x) (y : P x) =>
   merely
     {f : forall i : I, A i &
     {q : x = (fun i : I => class_of (R i) (f i)) &
     forall (f' : forall i : I, A i)
     (r : forall i : I, R i (f i) (f' i)),
     transport P (qglue_forall f f' r)
       (transport P q y) = a f'}})
  (path_forall (fun x : I => class_of (R x) (f' x))
     (fun i : I => class_of (R i) (f i))
     (fun i : I => qglue (p' i)))
  (a f'; tr (f'; 1; E f')).1
  (a f'; tr (f'; 1; E f')).2).1 = a f apply E.
  Qed.

(** The "beta-rule" of [choose_quotient_rec]. *)

  Lemma choose_quotient_rec_compute
    {B : Type} `{!IsHSet B} (a : (forall i, A i) -> B)
    (E : forall (f f' : forall i, A i),
         (forall i, R i (f i) (f' i)) -> a f = a f')
    (f : forall i, A i)
    : choose_quotient_rec a E (fun i => class_of (R i) (f i)) = a f.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
B: Type
IsHSet0: IsHSet B
a: (forall i : I, A i) -> B
E: forall f f' : forall i : I, A i,
(forall i : I, R i (f i) (f' i)) -> a f = a f'
f: forall i : I, A i
choose_quotient_rec a E
  (fun i : I => class_of (R i) (f i)) = a f
  Proof.
H: Univalence
I: Type
HasTrChoice0: HasTrChoice 0 I
A: I -> Type
H0: forall i : I, IsHSet (A i)
R: forall i : I, Relation (A i)
H1: forall (i : I) (x y : A i), IsHProp (R i x y)
rR: forall i : I, Reflexive (R i)
sR: forall i : I, Symmetric (R i)
tR: forall i : I, Transitive (R i)
B: Type
IsHSet0: IsHSet B
a: (forall i : I, A i) -> B
E: forall f f' : forall i : I, A i,
(forall i : I, R i (f i) (f' i)) -> a f = a f'
f: forall i : I, A i
choose_quotient_rec a E
  (fun i : I => class_of (R i) (f i)) = a f
    apply (choose_quotient_ind_compute (fun _ => B)).
  Qed.
End choose_quotient_ind.