Library HoTT.Colimits.Quotient.Choice

Require Import
  HoTT.Basics
  HoTT.Types
  HoTT.Universes.HSet
  HoTT.Truncations.Core
  HoTT.Colimits.Quotient
  HoTT.Projective.

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

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

Section choose_has_quotient_choice.
  Context `{Univalence}
    {A : Type} {B : A → Type} `{!∀ x, IsHSet (B x)}
    (P : ∀ x, B x → Type) `{!∀ 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
    : ∀ x, Reflexive (RelClassEquiv x).
  Proof.
    intros a b. apply equiv_idmap.
  Qed.

  Local Instance symmetric_relclass
    : ∀ x, Symmetric (RelClassEquiv x).
  Proof.
    intros a b1 b2 p. apply (equiv_inverse p).
  Qed.

  Local Instance transitive_relclass
    : ∀ x, Transitive (RelClassEquiv x).
  Proof.
    intros a b1 b2 b3 p q. apply (equiv_compose q p).
  Qed.

  Local Instance hprop_choose_cod (a : A)
    : IsHProp {c : B a / RelClassEquiv a
                 | ∀ b, in_class (RelClassEquiv a) c b <~> P a b}.
  Proof.
    apply ishprop_sigma_disjoint.
    refine (Quotient_ind_hprop _ _ _).
    intro b1.
    refine (Quotient_ind_hprop _ _ _).
    intros b2 f g.
    apply qglue.
    apply (f b2)^-1.
    apply g.
    apply reflexive_relclass.
  Qed.

  Local Definition prechoose (i : ∀ x, hexists (P x)) (a : A)
    : {c : B a / RelClassEquiv a
         | ∀ b : B a, in_class (RelClassEquiv a) c b <~> P a b}.
  Proof.
    specialize (i a).
    strip_truncations.
    destruct i as [b1 h].
    ∃ (class_of _ b1).
    intro b2.
    apply equiv_iff_hprop.
    - intro f. exact (f h).
    - intro p. by apply equiv_iff_hprop.
  Defined.

  Local Definition choose (i : ∀ 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).
  Proof.
    done.
  Qed.

  Local Instance symmetric_relunit (B : A → Type) (a : A)
    : Symmetric (RelUnit B a).
  Proof.
    done.
  Qed.

  Local Instance transitive_relunit (B : A → Type) (a : A)
    : Transitive (RelUnit B a).
  Proof.
    done.
  Qed.

  Local Instance ishprop_quotient_relunit (B : A → Type) (a : A)
    : IsHProp (B a / RelUnit B a).
  Proof.
    apply hprop_allpath.
    refine (Quotient_ind_hprop _ _ _).
    intro r.
    refine (Quotient_ind_hprop _ _ _).
    intro s.
    by apply qglue.
  Qed.

  Lemma has_tr0_choice_quotientchoice : HasTrChoice 0 A.
  Proof.
    intros B sB f.
    transparent assert (g : (∀ a, B a / RelUnit B a)).
    - intro a.
      specialize (f a).
      strip_truncations.
      exact (class_of _ f).
    - specialize (qch B _ (RelUnit B) _ _ _ _ g).
      strip_truncations.
      apply tr.
      apply qch.
  Qed.

End has_tr0_choice_quotientchoice.

Lemma has_quotient_choice_tr0choice (A : Type)
  : HasTrChoice 0 A → HasQuotientChoice A.
Proof.
  intros ch B sB R pR rR sR tR f.
  set (P := fun a b ⇒ class_of (R a) b = f a).
  assert (∀ a, merely ((fun x ⇒ {b | P x b}) a)) as g.
  - intro a.
    refine (Quotient_ind_hprop _
              (fun c ⇒ merely {b | class_of (R a) b = c}) _ (f a)).
    intro b.
    apply tr.
    by ∃ b.
  - pose proof (ch (fun a ⇒ {b | P a b}) _ g) as h.
    strip_truncations.
    apply tr.
    ∃ (fun x ⇒ (h x).1).
    intro a.
    apply h.
Qed.

Global Instance isequiv_has_tr0_choice_to_has_quotient_choice
  `{Funext} (A : Type)
  : IsEquiv (has_quotient_choice_tr0choice A).
Proof.
  srapply isequiv_iff_hprop.
  - apply istrunc_forall.
  - 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} `{!∀ i, IsHSet (A i)}
    (R : ∀ i, Relation (A i))
    `{!∀ i, is_mere_relation (A i) (R i)}
    {rR : ∀ i, Reflexive (R i)}
    {sR : ∀ i, Symmetric (R i)}
    {tR : ∀ i, Transitive (R i)}.

First generalize the qglue constructor.

  Lemma qglue_forall
    (f g : ∀ i, A i) (r : ∀ i, R i (f i) (g i))
    : (fun i ⇒ class_of (R i) (f i)) = (fun i ⇒ class_of (R i) (g i)).
  Proof.
    funext 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 : (∀ i, A i / R i) → Type) `{!∀ g, IsHSet (P g)}
    (a : ∀ (f : ∀ i, A i), P (fun i ⇒ class_of (R i) (f i)))
    (g : ∀ i, A i / R i)
    : Type
    := {b : P g
       | merely (∃ (f : ∀ i, A i)
                        (q : g = fun i ⇒ class_of (R i) (f i)),
                 ∀ (f' : ∀ i, A i)
                        (r : ∀ i, R i (f i) (f' i)),
                 qglue_forall f f' r # q # b = a f')}.

  Local Instance ishprop_choose_quotient_ind_chooseprop
    (P : (∀ i, A i / R i) → Type) `{!∀ g, IsHSet (P g)}
    (a : ∀ (f : ∀ i, A i), P (fun i ⇒ class_of (R i) (f i)))
    (g : ∀ i, A i / R i)
    : IsHProp (ChooseProp P a g).
  Proof.
    apply ishprop_sigma_disjoint.
    intros x y h1 h2.
    strip_truncations.
    destruct h1 as [f1 [q1 p1]].
    destruct h2 as [f2 [q2 p2]].
    specialize (p1 f1 (fun i ⇒ rR i (f1 i))).
    set (pR := fun i ⇒
                related_quotient_paths (R i) _ _ (ap (fun h ⇒ h i) q2^
                @ ap (fun h ⇒ h i) q1)).
    specialize (p2 f1 pR).
    do 2 apply moveL_transport_V in p1.
    do 2 apply moveL_transport_V in p2.
    refine (p1 @ _ @ p2^).
    apply moveR_transport_p.
    rewrite inv_V.
    rewrite <- transport_pp.
    apply moveR_transport_p.
    rewrite inv_V.
    do 2 rewrite <- transport_pp.
    set (pa := (qglue_forall f2 f1 pR)^
               @ (q2^ @ q1 @ qglue_forall f1 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 : (∀ i, A i / R i) → Type) `{!∀ g, IsHSet (P g)}
    (a : ∀ (f : ∀ i, A i), P (fun i ⇒ class_of (R i) (f i)))
    (E : ∀ (f f' : ∀ i, A i) (r : ∀ i, R i (f i) (f' i)),
         qglue_forall f f' r # a f = a f')
    (g : ∀ i, A i / R i)
    : ChooseProp P a g.
  Proof.
    pose proof
      (has_quotient_choice_tr0choice I _ A _ R _ _ _ _ g) as h.
    strip_truncations.
    destruct h as [h p].
    apply path_forall in p.
    refine (transport _ p _).
    ∃ (a h).
    apply tr.
    ∃ h.
    ∃ 1.
    apply E.
  Defined.

By projecting out of chooseprop_quotient_ind we obtain a generalization of quotient_rec2.

  Lemma choose_quotient_ind
    (P : (∀ i, A i / R i) → Type) `{!∀ g, IsHSet (P g)}
    (a : ∀ (f : ∀ i, A i), P (fun i ⇒ class_of (R i) (f i)))
    (E : ∀ (f f' : ∀ i, A i) (r : ∀ i, R i (f i) (f' i)),
         qglue_forall f f' r # a f = a f')
    (g : ∀ i, A i / R i)
    : P g.
  Proof.
    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 : (∀ i, A i / R i) → Type) `{!∀ g, IsHProp (P g)}
    (a : ∀ (f : ∀ i, A i), P (fun i ⇒ class_of (R i) (f i)))
    (g : ∀ i, A i / R i)
    : P g.
  Proof.
    refine (choose_quotient_ind P a _ g). intros. apply path_ishprop.
  Defined.

The recursion principle derived from choose_quotient_ind.

  Definition choose_quotient_rec
    {B : Type} `{!IsHSet B} (a : (∀ i, A i) → B)
    (E : ∀ (f f' : ∀ i, A i),
         (∀ i, R i (f i) (f' i)) → a f = a f')
    (g : ∀ 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 : (∀ i, A i / R i) → Type) `{!∀ g, IsHSet (P g)}
    (a : ∀ (f : ∀ i, A i), P (fun i ⇒ class_of (R i) (f i)))
    (E : ∀ (f f' : ∀ i, A i) (r : ∀ i, R i (f i) (f' i)),
         qglue_forall f f' r # a f = a f')
    (f : ∀ i, A i)
    : choose_quotient_ind P a E (fun i ⇒ class_of (R i) (f i)) = a f.
  Proof.
    refine (Trunc_ind (fun a ⇒ (_ a).1 = _) _ _). cbn.
    intros [f' p].
    rewrite transport_sigma.
    set (p' := fun x ⇒ related_quotient_paths (R x) _ _ (p x)).
    assert (p = (fun i ⇒ qglue (p' i))) as pE.
    - funext x. apply hset_path2.
    - rewrite pE. apply E.
  Qed.

The "beta-rule" of choose_quotient_rec.

  Lemma choose_quotient_rec_compute
    {B : Type} `{!IsHSet B} (a : (∀ i, A i) → B)
    (E : ∀ (f f' : ∀ i, A i),
         (∀ i, R i (f i) (f' i)) → a f = a f')
    (f : ∀ i, A i)
    : choose_quotient_rec a E (fun i ⇒ class_of (R i) (f i)) = a f.
  Proof.
    apply (choose_quotient_ind_compute (fun _ ⇒ B)).
  Qed.
End choose_quotient_ind.