From 40e1f45cfa0a62771de8ab9102793e9b34f0cf83 Mon Sep 17 00:00:00 2001
From: Niels <nnmvdw@gmail.com>
Date: Fri, 1 Sep 2017 16:29:48 +0200
Subject: [PATCH] Shortened T.v

---
 FiniteSets/representations/T.v          | 354 +++---------------------
 FiniteSets/representations/definition.v |  74 -----
 FiniteSets/variations/projective.v      |  43 +--
 3 files changed, 71 insertions(+), 400 deletions(-)

diff --git a/FiniteSets/representations/T.v b/FiniteSets/representations/T.v
index 2e435e6..dd9c764 100644
--- a/FiniteSets/representations/T.v
+++ b/FiniteSets/representations/T.v
@@ -1,330 +1,68 @@
 (* Type which proves that all types have merely decidable equality implies LEM *)
 Require Import HoTT HitTactics Sub.
 
-Module Export T.
-  Section HIT.
-    Variable A : Type.
-
-    Private Inductive T (B : Type) : Type :=
-    | b : T B
-    | c : T B.
-
-    Axiom p : A -> b A = c A.
-    Axiom setT : IsHSet (T A).
-
-  End HIT.
-
-  Arguments p {_} _.
-
-  Section T_induction.
-    Variable A : Type.
-    Variable (P : (T A) -> Type).
-    Variable (H : forall x, IsHSet (P x)).
-    Variable (bP : P (b A)).
-    Variable (cP : P (c A)).
-    Variable (pP : forall a : A, (p a) # bP = cP).
-
-    (* Induction principle *)
-    Fixpoint T_ind
-             (x : T A)
-             {struct x}
-      : P x
-      := (match x return _ -> _ -> P x with
-          | b => fun _ _ => bP
-          | c => fun _ _ => cP
-          end) pP H.
-
-    Axiom T_ind_beta_p : forall (a : A),
-        apD T_ind (p a) = pP a.
-  End T_induction.
-
-  Section T_recursion.
-
-    Variable A : Type.
-    Variable P : Type.
-    Variable H : IsHSet P.
-    Variable bP : P.
-    Variable cP : P.
-    Variable pP : A -> bP = cP.
-
-    Definition T_rec : T A -> P.
-    Proof.
-      simple refine (T_ind A _ _ _ _ _) ; cbn.
-      - apply bP.
-      - apply cP.
-      - intro a.
-        simple refine ((transport_const _ _) @  (pP a)).
-    Defined.
-
-    Definition T_rec_beta_p : forall (a : A),
-        ap T_rec (p a) = pP a.
-    Proof.
-      intros.
-      unfold T_rec.
-      eapply (cancelL (transport_const (p a) _)).
-      simple refine ((apD_const _ _)^ @ _).
-      apply T_ind_beta_p.
-    Defined.
-  End T_recursion.
-
-  Instance T_recursion A : HitRecursion (T A)
-    := {indTy := _; recTy := _;
-        H_inductor := T_ind A; H_recursor := T_rec A }.
-
-End T.
-
-Section merely_dec_lem.
-  Variable A : hProp.
+Section TR.
   Context `{Univalence}.
+  Variable A : hProp.
 
-  Definition code_b : T A -> hProp.
+  Definition T := Unit + Unit.
+
+  Definition R (x y : T) : hProp :=
+    match x, y with
+    | inl tt, inl tt => Unit_hp
+    | inl tt, inr tt => A
+    | inr tt, inl tt => A
+    | inr tt, inr tt => Unit_hp
+    end.
+
+  Global Instance R_mere : is_mere_relation _ R.
   Proof.
-    hrecursion.
-    - apply Unit_hp.
-    - apply A.
-    - intro a.
-      apply path_iff_hprop.
-      * apply (fun _ => a).
-      * apply (fun _ => tt).
+    intros x y ; destruct x ; destruct y ; apply _.
   Defined.
 
-  Definition code_c : T A -> hProp.
+  Global Instance R_refl : Reflexive R.
   Proof.
-    hrecursion.
-    - apply A.
-    - apply Unit_hp.
-    - intro a.
-      apply path_iff_hprop.
-      * apply (fun _ => tt).
-      * apply (fun _ => a).
+    intro x ; destruct x as [[ ] | [ ]] ; apply tt.
+  Defined.
+  
+  Global Instance R_sym : Symmetric R.
+  Proof.
+    repeat (let x := fresh in intro x ; destruct x as [[ ] | [ ]])
+    ; auto ; apply tt.
+  Defined.
+  
+  Global Instance R_trans : Transitive R.
+  Proof.
+    repeat (let x := fresh in intro x ; destruct x as [[ ] | [ ]]) ; intros
+    ; auto ; apply tt.
   Defined.
 
-  Definition code : T A -> T A -> hProp.
-  Proof.
-    simple refine (T_rec _ _ _ _ _ _).
-    - exact code_b.
-    - exact code_c.
-    - intro a.
-      apply path_forall.
-      intro z.
-      hinduction z.
-      * apply path_iff_hprop.
-        ** apply (fun _ => a).
-        ** apply (fun _ => tt).
-      * apply path_iff_hprop.
-        ** apply (fun _ => tt).
-        ** apply (fun _ => a).
-      * intros. apply set_path2.
-  Defined.
+  Definition TR : Type := quotient R.
+  Definition TR_zero : TR := class_of R (inl tt).
+  Definition TR_one : TR := class_of R (inr tt).
 
-  Local Ltac f_prop := apply path_forall ; intro ; apply path_ishprop.
+  Definition equiv_pathspace_T : (TR_zero = TR_one) = (R (inl tt) (inr tt))
+    := path_universe (sets_exact R (inl tt) (inr tt)).
 
-  Lemma transport_code_b_x (a : A) :
-    transport code_b (p a) = fun _ => a.
-  Proof.
-    f_prop.
-  Defined.
-
-  Lemma transport_code_c_x (a : A) :
-    transport code_c (p a) = fun _ => tt.
-  Proof.
-    f_prop.
-  Defined.
-
-  Lemma transport_code_c_x_V (a : A) :
-    transport code_c (p a)^ = fun _ => a.
-  Proof.
-    f_prop.
-  Defined.
-
-  Lemma transport_code_x_b (a : A) :
-    transport (fun x => code x (b A)) (p a) = fun _ => a.
-  Proof.
-    f_prop.
-  Defined.
-
-  Lemma transport_code_x_c (a : A) :
-    transport (fun x => code x (c A)) (p a) = fun _ => tt.
-  Proof.
-    f_prop.
-  Defined.
-
-  Lemma transport_code_x_c_V (a : A) :
-    transport (fun x => code x (c A)) (p a)^ = fun _ => a.
-  Proof.
-    f_prop.
-  Defined.
-
-  Lemma ap_diag {B : Type} {x y : B} (p : x = y) :
-    ap (fun x : B => (x, x)) p = path_prod' p p.
-  Proof.
-      by path_induction.
-  Defined.
-
-  Lemma transport_code_diag (a : A) z :
-    (transport (fun i : (T A) => code i i) (p a)) z = tt.
-  Proof.
-    apply path_ishprop.
-  Defined.
-
-  Definition r : forall (x : T A), code x x.
-  Proof.
-    simple refine (T_ind _ _ _ _ _ _); simpl.
-    - exact tt.
-    - exact tt.
-    - intro a.
-      apply transport_code_diag.
-  Defined.
-
-  Definition encode_pre : forall (x y : T A), x = y -> code x y
-    := fun x y p => transport (fun z => code x z) p (r x).
-
-  Definition encode : forall x y, x = y -> code x y.
-  Proof.
-    intros x y.
-    intro p.
-    refine (transport (fun z => code x z) p _). clear p.
-    revert x. simple refine (T_ind _ _ _ _ _ _); simpl.
-    - exact tt.
-    - exact tt.
-    - intro a.
-      apply path_ishprop.
-  Defined.
-
-  Definition decode_b : forall (y : T A), code_b y -> (b A) = y.
-  Proof.
-    simple refine (T_ind _ _ _ _ _ _) ; simpl.
-    - exact (fun _ => idpath).
-    - exact (fun a => p a).
-    - intro a.
-      apply path_forall.
-      intro t.
-      refine (transport_arrow _ _ _ @ _).
-      refine (transport_paths_FlFr _ _ @ _).
-      hott_simpl.
-      f_ap.
-      apply path_ishprop.
-  Defined.
-
-  Definition decode_c : forall (y : T A), code_c y -> (c A) = y.
-  Proof.
-    simple refine (T_ind _ _ _ _ _ _); simpl.
-    - exact (fun a => (p a)^).
-    - exact (fun _ => idpath).
-    - intro a.
-      apply path_forall.
-      intro t.
-      refine (transport_arrow _ _ _ @ _).
-      refine (transport_paths_FlFr _ _ @ _).
-      rewrite transport_code_c_x_V.
-      hott_simpl.
-  Defined.
-
-  Lemma transport_paths_FlFr_trunc :
-    forall {X Y : Type} (f g : X -> Y) {x1 x2 : X} (q : x1 = x2)
-           (r : f x1 = g x1),
-      transport (fun x : X => Trunc 0 (f x = g x)) q (tr r) = tr (((ap f q)^ @ r) @ ap g q).
-  Proof.
-    destruct q; simpl. intro r.
-    refine (ap tr _).
-    exact ((concat_1p r)^ @ (concat_p1 (1 @ r))^).
-  Defined.
-
-  Definition decode : forall (x y : T A), code x y -> x = y.
-  Proof.
-    simple refine (T_ind _ _ _ _ _ _); simpl.
-    - intro y. exact (decode_b y).
-    - intro y. exact (decode_c y).
-    - intro a.
-      apply path_forall. intro z.
-      rewrite transport_forall_constant.
-      apply path_forall. intros c.
-      rewrite transport_arrow.
-      hott_simpl.
-      rewrite (transport_paths_FlFr _ _).
-      revert z c. simple refine (T_ind _ _ _ _ _ _) ; simpl.
-      + intro.
-        hott_simpl.
-        f_ap.
-        refine (ap (fun x => (p x)) _).
-        apply path_ishprop.
-      + intro.
-        rewrite transport_code_x_c_V.
-        hott_simpl.
-      + intro b.
-        apply path_forall.
-        intro z.
-        rewrite transport_forall.
-        apply set_path2.
-  Defined.
-
-  Lemma decode_encode (u v : T A) : forall (p : u = v),
-      decode u v (encode u v p) = p.
-  Proof.
-    intros p. induction p.
-    simpl. revert u. simple refine (T_ind _ _ _ _ _ _).
-    + simpl. reflexivity.
-    + simpl. reflexivity.
-    + intro a.
-      apply set_path2.
-  Defined.
-
-  Lemma encode_decode : forall (u v : T A) (c : code u v),
-      encode u v (decode u v c) = c.
-  Proof.
-    simple refine (T_ind _ _ _ _ _ _).
-    - simple refine (T_ind _ _ _ _ _ _).
-      + simpl. apply path_ishprop.
-      + simpl. intro a. apply path_ishprop.
-      + intro a. apply path_forall; intros ?. apply set_path2.
-    - simple refine (T_ind _ _ _ _ _ _).
-      + simpl. intro a. apply path_ishprop.
-      + simpl. apply path_ishprop.
-      + intro a. apply path_forall; intros ?. apply set_path2.
-    - intro a. repeat (apply path_forall; intros ?). apply set_path2.
-  Defined.
-
-
-  Instance T_hprop (a : A) : IsHProp (b A = c A).
-  Proof.
-    apply hprop_allpath.
-    intros x y.
-    pose (encode (b A) _ x) as t1.
-    pose (encode (b A) _ y) as t2.
-    assert (t1 = t2).
+  Global Instance quotientB_recursion : HitRecursion TR :=
     {
-      unfold t1, t2.
-      apply path_ishprop.
-    }
-    pose (decode _ _ t1) as t3.
-    pose (decode _ _ t2) as t4.
-    assert (t3 = t4) as H1.
-    {
-      unfold t3, t4.
-      f_ap.
-    }
-    unfold t3, t4, t1, t2 in H1.
-    rewrite ?decode_encode in H1.
-    apply H1.
-  Defined.
+      indTy := _;
+      recTy :=
+        forall (P : Type) (HP: IsHSet P) (u : T -> P),
+          (forall x y : T, R x y -> u x = u y) -> TR -> P;
+      H_inductor := quotient_ind R ;
+      H_recursor := @quotient_rec _ R _
+    }.
 
-  Lemma equiv_pathspace_T : (b A = c A) = A.
-  Proof.
-    apply path_iff_ishprop.
-    - intro x.
-      apply (encode (b A) (c A) x).
-    - apply p.
-  Defined.
-
-End merely_dec_lem.
+End TR.
 
 Theorem merely_dec `{Univalence} : (forall (A : Type) (a b : A), hor (a = b) (~a = b))
                                    ->
                                    forall (A : hProp), A + (~A).
 Proof.
-  intros.
-  specialize (X (T A) (b A) (c A)).
-  rewrite (equiv_pathspace_T A) in X.
+  intros X A.
+  specialize (X (TR A) (TR_zero A) (TR_one A)).
+  rewrite equiv_pathspace_T in X.
   strip_truncations.
   apply X.
-Defined.
+Defined.
\ No newline at end of file
diff --git a/FiniteSets/representations/definition.v b/FiniteSets/representations/definition.v
index 2bc8fb9..533e9c6 100644
--- a/FiniteSets/representations/definition.v
+++ b/FiniteSets/representations/definition.v
@@ -74,20 +74,6 @@ Module Export FSet.
           | U y z => fun _ _ _ _ _ _ => uP y z (FSet_ind y) (FSet_ind z)
           end) H assocP commP nlP nrP idemP.
 
-    Axiom FSet_ind_beta_assoc : forall (x y z : FSet A),
-        apD FSet_ind (assoc x y z) =
-        (assocP x y z (FSet_ind x)  (FSet_ind y) (FSet_ind z)).
-
-    Axiom FSet_ind_beta_comm : forall (x y : FSet A),
-        apD FSet_ind (comm x y) = (commP x y (FSet_ind x) (FSet_ind y)).
-
-    Axiom FSet_ind_beta_nl : forall (x : FSet A),
-        apD FSet_ind (nl x) = (nlP x (FSet_ind x)).
-
-    Axiom FSet_ind_beta_nr : forall (x : FSet A),
-        apD FSet_ind (nr x) = (nrP x (FSet_ind x)).
-
-    Axiom FSet_ind_beta_idem : forall (x : A), apD FSet_ind (idem x) = idemP x.
   End FSet_induction.
 
   Section FSet_recursion.
@@ -118,66 +104,6 @@ Module Export FSet.
       - apply idemP.
     Defined.
 
-    Definition FSet_rec_beta_assoc : forall (x y z : FSet A),
-        ap FSet_rec (assoc x y z)
-        =
-        assocP (FSet_rec x) (FSet_rec y) (FSet_rec z).
-    Proof.
-      intros.
-      unfold FSet_rec.
-      eapply (cancelL (transport_const (assoc x y z) _)).
-      simple refine ((apD_const _ _)^ @ _).
-      apply FSet_ind_beta_assoc.
-    Defined.
-
-    Definition FSet_rec_beta_comm : forall (x y : FSet A),
-        ap FSet_rec (comm x y)
-        =
-        commP (FSet_rec x) (FSet_rec y).
-    Proof.
-      intros.
-      unfold FSet_rec.
-      eapply (cancelL (transport_const (comm x y) _)).
-      simple refine ((apD_const _ _)^ @ _).
-      apply FSet_ind_beta_comm.
-    Defined.
-
-    Definition FSet_rec_beta_nl : forall (x : FSet A),
-        ap FSet_rec (nl x)
-        =
-        nlP (FSet_rec x).
-    Proof.
-      intros.
-      unfold FSet_rec.
-      eapply (cancelL (transport_const (nl x) _)).
-      simple refine ((apD_const _ _)^ @ _).
-      apply FSet_ind_beta_nl.
-    Defined.
-
-    Definition FSet_rec_beta_nr : forall (x : FSet A),
-        ap FSet_rec (nr x)
-        =
-        nrP (FSet_rec x).
-    Proof.
-      intros.
-      unfold FSet_rec.
-      eapply (cancelL (transport_const (nr x) _)).
-      simple refine ((apD_const _ _)^ @ _).
-      apply FSet_ind_beta_nr.
-    Defined.
-
-    Definition FSet_rec_beta_idem : forall (a : A),
-        ap FSet_rec (idem a)
-        =
-        idemP a.
-    Proof.
-      intros.
-      unfold FSet_rec.
-      eapply (cancelL (transport_const (idem a) _)).
-      simple refine ((apD_const _ _)^ @ _).
-      apply FSet_ind_beta_idem.
-    Defined.
-
   End FSet_recursion.
 
   Instance FSet_recursion A : HitRecursion (FSet A) :=
diff --git a/FiniteSets/variations/projective.v b/FiniteSets/variations/projective.v
index 0c2b651..100acbe 100644
--- a/FiniteSets/variations/projective.v
+++ b/FiniteSets/variations/projective.v
@@ -87,35 +87,41 @@ End k_fin_lem_projective.
 Section k_fin_projective_lem.
   Context `{Univalence}.
   Variable (P : Type).
-  Context `{Hprop : IsHProp P}.
+  Context `{IsHProp P}.
 
-  Definition X : Type := T P.
+  Definition X : Type := TR (BuildhProp P).
   Instance X_set : IsHSet X.
-  Proof. apply _. Defined.
+  Proof.
+    apply _.
+  Defined.
 
   Definition X_fin : Kf X.
   Proof.
     apply Kf_unfold.
-    exists ({|b P|} ∪ {|c P|}).
+    exists ({|TR_zero _|} ∪ {|TR_one _|}).
     hinduction.
-    - apply (tr (inl (tr idpath))).
-    - apply (tr (inr (tr idpath))).
-    - intros. apply path_ishprop.
+    - destruct x as [ [ ] | [ ] ].
+      * apply (tr (inl (tr idpath))).
+      * apply (tr (inr (tr idpath))).
+    - intros.
+      apply path_ishprop.
   Defined.
 
   Definition p (a : Unit + Unit) : X :=
     match a with
-    | inl _ => b P
-    | inr _ => c P
+    | inl _ => TR_zero _
+    | inr _ => TR_one _
     end.
 
   Instance p_surj : IsSurjection p.
   Proof.
     apply BuildIsSurjection.
     hinduction.
-    - apply tr. exists (inl tt). reflexivity.
-    - apply tr. exists (inr tt). reflexivity.
-    - intros. apply path_ishprop.
+    - destruct x as [[ ] | [ ]].
+      * apply tr. exists (inl tt). reflexivity.
+      * apply tr. exists (inr tt). reflexivity.
+    - intros.
+      apply path_ishprop.
   Defined.
 
   Lemma LEM `{IsProjective X} : P + ~P.
@@ -123,16 +129,17 @@ Section k_fin_projective_lem.
     pose (k := projective p idmap _).
     unfold hexists in k.
     simple refine (Trunc_rec _ k); clear k; intros [g Hg].
-    destruct (dec (g (b P) = g (c P))) as [Hℵ | Hℵ].
+    destruct (dec (g (TR_zero _) = g (TR_one _))) as [Hℵ | Hℵ].
     - left.
-      assert (b P = c P) as Hbc.
+      assert (TR_zero (BuildhProp P) = TR_one _) as Hbc.
       { pose (ap p Hℵ) as Hα.
-        rewrite (ap (fun h => h (b P)) Hg) in Hα.
-        rewrite (ap (fun h => h (c P)) Hg) in Hα.
+        rewrite (ap (fun h => h (TR_zero _)) Hg) in Hα.
+        rewrite (ap (fun h => h (TR_one _)) Hg) in Hα.
         assumption. }
-      apply (encode _ (b P) (c P) Hbc).
+      refine (classes_eq_related _ _ _ Hbc).
     - right. intros HP.
       apply Hℵ.
-      apply (ap g (T.p HP)).
+      refine (ap g (related_classes_eq _ _)).
+      apply HP.
   Defined.
 End k_fin_projective_lem.