feat(types.trunc): prove the principle of unique choice

hott/book.md

@@ -17,7 +17,7 @@ The rows indicate the chapters, the columns the sections.
 |-------|---|---|---|---|---|---|---|---|---|----|----|----|----|----|----|
 | Ch 1  | . | . | . | . | + | + | + | + | + | .  | +  | +  |    |    |    |
 | Ch 2  | + | + | + | + | . | + | + | + | + | +  | +  | +  | +  | +  | +  |
-| Ch 3  | + | + | + | + | ½ | + | + | - | ½ | .  | +  |    |    |    |    |
+| Ch 3  | + | + | + | + | ½ | + | + | - | + | .  | +  |    |    |    |    |
 | Ch 4  | - | + | - | + | . | + | - | - | + |    |    |    |    |    |    |
 | Ch 5  | - | . | - | - | - | . | . | ½ |   |    |    |    |    |    |    |
 | Ch 6  | . | + | + | + | + | ½ | ½ | ¼ | ¼ | ¼  | ¾  | -  | .  |    |    |
@@ -77,7 +77,7 @@ Chapter 3: Sets and logic
 - 3.6 (The logic of mere propositions): in the corresponding file in the [types](types/types.md) folder. (is_trunc_prod is defined in [types.sigma](types/sigma.hlean))
 - 3.7 (Propositional truncation): [init.hit](init/hit.hlean) and [hit.trunc](hit/trunc.hlean)
 - 3.8 (The axiom of choice): not formalized
-- 3.9 (The principle of unique choice): Lemma 9.3.1 is equiv_trunc in [hit.trunc](hit/trunc.hlean), Lemma 9.3.2 is not formalized
+- 3.9 (The principle of unique choice): Lemma 9.3.1 in [hit.trunc](hit/trunc.hlean), Lemma 9.3.2 in [types.trunc](types/trunc.hlean)
 - 3.10 (When are propositions truncated?): no formalizable content
 - 3.11 (Contractibility): [init.trunc](init/trunc.hlean) (mostly), [types.pi](types/pi.hlean) (Lemma 3.11.6), [types.trunc](types/trunc.hlean) (Lemma 3.11.7), [types.sigma](types/sigma.hlean) (Lemma 3.11.9) 
 

hott/hit/circle.hlean

@@ -144,7 +144,7 @@ namespace circle
 
   theorem elim_type_loop_inv (Pbase : Type) (Ploop : Pbase ≃ Pbase) :
     transport (circle.elim_type Pbase Ploop) loop⁻¹ = to_inv Ploop :=
-  by rewrite [tr_inv_fn,↑to_inv]; apply inv_eq_inv; apply elim_type_loop
+  by rewrite [tr_inv_fn]; apply inv_eq_inv; apply elim_type_loop
 end circle
 
 attribute circle.base1 circle.base2 circle.base [constructor]
@@ -245,7 +245,7 @@ namespace circle
   --the carrier of π₁(S¹) is the set-truncation of base = base.
   open core algebra trunc equiv.ops
   definition fg_carrier_equiv_int : π₁(S¹) ≃ ℤ :=
-  trunc_equiv_trunc 0 base_eq_base_equiv ⬝e !equiv_trunc⁻¹ᵉ
+  trunc_equiv_trunc 0 base_eq_base_equiv ⬝e !trunc_equiv
 
   definition con_comm_base (p q : base = base) : p ⬝ q = q ⬝ p :=
   eq_of_fn_eq_fn base_eq_base_equiv (by esimp;rewrite [+encode_con,add.comm])

hott/hit/trunc.hlean

@@ -41,8 +41,8 @@ namespace trunc
              (λaa, trunc.rec_on aa (λa, idp))
              (λa, idp)
 
-  definition equiv_trunc [H : is_trunc n A] : A ≃ trunc n A :=
+  definition trunc_equiv [H : is_trunc n A] : trunc n A ≃ A :=
-  equiv.mk tr _
+  (equiv.mk tr _)⁻¹ᵉ
 
   definition is_trunc_of_is_equiv_tr [H : is_equiv (@tr n A)] : is_trunc n A :=
   is_trunc_is_equiv_closed n (@tr n _)⁻¹
@@ -128,7 +128,7 @@ namespace trunc
     : trunc n (Σ x, P x) ≃ Σ x, trunc n (P x) :=
   calc
     trunc n (Σ x, P x) ≃ trunc n (Σ x, trunc n (P x)) : trunc_sigma_equiv
-      ... ≃ Σ x, trunc n (P x) : equiv.symm !equiv_trunc
+      ... ≃ Σ x, trunc n (P x) : !trunc_equiv
   end
 
 end trunc

hott/init/trunc.hlean

@@ -300,11 +300,14 @@ namespace is_trunc
   theorem is_hset.elimo (q q' : c =[p] c₂) [H : is_hset (C a)] : q = q' :=
   !is_hprop.elim
 
-  /- truncatedness of lift -/
-  definition is_trunc_lift [instance] (A : Type) (n : trunc_index) [H : is_trunc n A]
-    : is_trunc n (lift A) :=
-  is_trunc_equiv_closed _ !equiv_lift
-
   -- TODO: port "Truncated morphisms"
 
 end is_trunc
+
+/- truncatedness of lift -/
+namespace lift
+  open is_trunc equiv
+  definition is_trunc_lift [instance] [priority 1450] (A : Type) (n : trunc_index)
+    [H : is_trunc n A] : is_trunc n (lift A) :=
+  is_trunc_equiv_closed _ !equiv_lift
+end lift

hott/types/lift.hlean

@@ -138,4 +138,7 @@ namespace lift
       apply ua_refl}
   end
 
+  -- is_trunc_lift is defined in init.trunc
+
+
 end lift

hott/types/sigma.hlean

@@ -341,18 +341,22 @@ namespace sigma
   equiv.mk sigma.coind_unc _
   end
 
-  /- ** Subtypes (sigma types whose second components are hprops) -/
+  /- Subtypes (sigma types whose second components are hprops) -/
+
+  definition subtype [reducible] {A : Type} (P : A → Type) [H : Πa, is_hprop (P a)] :=
+  Σ(a : A), P a
+  notation [parsing-only] `{` binder `|` r:(scoped:1 P, subtype P) `}` := r
 
   /- To prove equality in a subtype, we only need equality of the first component. -/
-  definition subtype_eq [H : Πa, is_hprop (B a)] (u v : Σa, B a) : u.1 = v.1 → u = v :=
+  definition subtype_eq [H : Πa, is_hprop (B a)] (u v : {a | B a}) : u.1 = v.1 → u = v :=
   sigma_eq_unc ∘ inv pr1
 
-  definition is_equiv_subtype_eq [H : Πa, is_hprop (B a)] (u v : Σa, B a)
+  definition is_equiv_subtype_eq [H : Πa, is_hprop (B a)] (u v : {a | B a})
       : is_equiv (subtype_eq u v) :=
   !is_equiv_compose
   local attribute is_equiv_subtype_eq [instance]
 
-  definition equiv_subtype [H : Πa, is_hprop (B a)] (u v : Σa, B a) : (u.1 = v.1) ≃ (u = v) :=
+  definition equiv_subtype [H : Πa, is_hprop (B a)] (u v : {a | B a}) : (u.1 = v.1) ≃ (u = v) :=
   equiv.mk !subtype_eq _
 
   /- truncatedness -/

hott/types/trunc.hlean

@@ -227,7 +227,7 @@ namespace trunc
   begin
     revert A m H, eapply (trunc_index.rec_on n),
     { clear n, intro A m H, apply is_contr_equiv_closed,
-      { apply equiv_trunc, apply (@is_trunc_of_leq _ -2), exact unit.star} },
+      { apply equiv.symm, apply trunc_equiv, apply (@is_trunc_of_leq _ -2), exact unit.star} },
     { clear n, intro n IH A m H, induction m with m,
       { apply (@is_trunc_of_leq _ -2), exact unit.star},
       { apply is_trunc_succ_intro, intro aa aa',
@@ -238,6 +238,12 @@ namespace trunc
         { exact (IH _ _ _)}}}
   end
 
+  open equiv.ops
+  definition unique_choice {P : A → Type} [H : Πa, is_hprop (P a)] (f : Πa, ∥ P a ∥) (a : A)
+    : P a :=
+  !trunc_equiv (f a)
+
+
 end trunc open trunc
 
 namespace function