fix(choice): make some style changes

hott/choice.hlean

@@ -1,91 +1,88 @@
-import .types.trunc 
+import types.trunc types.bool
 open eq bool equiv sigma sigma.ops trunc is_trunc pi
 
-section
+namespace choice
 
   universe variable u
 
   -- 3.8.1. The axiom of choice.
-  definition AC := Π (X : Type.{u}) (A : X -> Type.{u}) (P : Π x, A x -> Type.{u}),
+  definition AC [reducible] := Π (X : Type.{u}) (A : X -> Type.{u}) (P : Π x, A x -> Type.{u}),
   is_hset X -> (Π x, is_hset (A x)) -> (Π x a, is_hprop (P x a)) ->
   (Π x, ∥ Σ a, P x a ∥) -> ∥ Σ f, Π x, P x (f x) ∥
 
-  -- 3.8.3. Corresponds to the assertion that "the cartesian product of a family of nonempty sets is nonempty".
-  definition AC_cart := Π (X : Type.{u}) (A : X -> Type.{u}), 
-  is_hset X -> (Π x, is_hset (A x)) -> (Π x, ∥ A x ∥) -> ∥ Π x, A x ∥  
+  -- 3.8.3. Corresponds to the assertion that
+  -- "the cartesian product of a family of nonempty sets is nonempty".
+  definition AC_cart [reducible] := Π (X : Type.{u}) (A : X -> Type.{u}),
+  is_hset X -> (Π x, is_hset (A x)) -> (Π x, ∥ A x ∥) -> ∥ Π x, A x ∥
 
   -- A slight variant of AC with a modified (equivalent) codomain.
-  definition AC' := Π (X : Type.{u}) (A : X -> Type.{u}) (P : Π x, A x -> Type.{u}),
+  definition AC' [reducible] := Π (X : Type.{u}) (A : X -> Type.{u}) (P : Π x, A x -> Type.{u}),
   is_hset X -> (Π x, is_hset (A x)) ->  (Π x a, is_hprop (P x a))
   -> (Π x, ∥ Σ a, P x a ∥) -> ∥ Π x, Σ a : A x, P x a ∥
 
   -- The equivalence of AC and AC' follows from the equivalence of their codomains.
   definition AC_equiv_AC' : AC.{u} ≃ AC'.{u} :=
-  @equiv_of_is_hprop _ _ !is_trunc_pi !is_trunc_pi
-  (λ H X A P HX HA HP HI, trunc_functor _
-  (to_fun !sigma_pi_equiv_pi_sigma) (H X A P HX HA HP HI))
-  (λ H X A P HX HA HP HI, trunc_functor _
-  (to_inv !sigma_pi_equiv_pi_sigma) (H X A P HX HA HP HI))
+  equiv_of_is_hprop
+    (λ H X A P HX HA HP HI, trunc_functor _ (to_fun !sigma_pi_equiv_pi_sigma) (H X A P HX HA HP HI))
+    (λ H X A P HX HA HP HI, trunc_functor _ (to_inv !sigma_pi_equiv_pi_sigma) (H X A P HX HA HP HI))
 
   -- AC_cart can be derived from AC' by setting P := λ _ _ , unit.
   definition AC_cart_of_AC' : AC'.{u} -> AC_cart.{u} :=
-  λ H X A HX HA HI, trunc_functor _ (λ H0 x, (H0 x).1) 
-  (H X A (λ x a, lift.{0 u} unit) HX HA (λ x a, !is_trunc_lift) 
-  (λ x, trunc_functor _ (λ a, ⟨a, lift.up.{0 u} unit.star⟩) (HI x))) 
+  λ H X A HX HA HI, trunc_functor _ (λ H0 x, (H0 x).1)
+    (H X A (λ x a, lift.{0 u} unit) HX HA (λ x a, !is_trunc_lift)
+      (λ x, trunc_functor _ (λ a, ⟨a, lift.up.{0 u} unit.star⟩) (HI x)))
 
   -- And the converse, by setting A := λ x, Σ a, P x a.
   definition AC'_of_AC_cart : AC_cart.{u} -> AC'.{u} :=
   by intro H X A P HX HA HP HI;
   apply H X (λ x, Σ a, P x a) HX (λ x, !is_trunc_sigma) HI
-  
-  -- Which is enough to show AC' ≃ AC_cart, since both are hprops. 
-  definition AC'_equiv_AC_cart : AC'.{u} ≃ AC_cart.{u} :=
-  @equiv_of_is_hprop _ _ !is_trunc_pi !is_trunc_pi AC'_to_AC_cart.{u} AC_cart_to_AC'.{u}
 
-  -- 3.8.2. AC ≃ AC_cart follows by transitivity. 
-  definition AC_equiv_AC_cart : AC.{u} ≃ AC_cart.{u} := 
+  -- Which is enough to show AC' ≃ AC_cart, since both are hprops.
+  definition AC'_equiv_AC_cart : AC'.{u} ≃ AC_cart.{u} :=
+  equiv_of_is_hprop AC_cart_of_AC'.{u} AC'_of_AC_cart.{u}
+
+  -- 3.8.2. AC ≃ AC_cart follows by transitivity.
+  definition AC_equiv_AC_cart : AC.{u} ≃ AC_cart.{u} :=
   equiv.trans AC_equiv_AC' AC'_equiv_AC_cart
 
-
+  namespace example385
   definition X : Type.{1} := Σ A : Type.{0}, ∥ A = bool ∥
-  
+
   definition x0 : X := ⟨bool, merely.intro _ rfl⟩
 
   definition Y : X -> Type.{1} := λ x, x0 = x
 
-  definition not_is_hprop_bool_eq_bool : ¬ is_hprop (bool = bool) :=
-  λ H, eq_bnot_ne_idp !is_hprop.elim 
-
-  definition not_is_hset_X : ¬ is_hset X := 
+  definition not_is_hset_X : ¬ is_hset X :=
   begin
     intro H, apply not_is_hprop_bool_eq_bool,
     apply @is_trunc_equiv_closed (x0 = x0),
     apply equiv.symm !equiv_subtype
-  end 
-
-  definition is_hset_bool : is_hset bool :=
-  @is_hset_of_decidable_eq _ bool.has_decidable_eq
+  end
 
   definition is_hset_x1 (x : X) : is_hset x.1 :=
-  by cases x; induction a_1; apply a_1⁻¹ ▸ is_hset_bool
+  by cases x; induction a_1; cases a_1; exact _
 
   definition is_hset_Yx (x : X) : is_hset (Y x) :=
   begin
     apply @is_trunc_equiv_closed _ _ _ !equiv_subtype,
-    apply @is_trunc_equiv_closed _ _ _ (equiv.symm !eq_equiv_equiv), 
+    apply @is_trunc_equiv_closed _ _ _ (equiv.symm !eq_equiv_equiv),
     apply is_trunc_equiv; repeat (apply is_hset_x1)
   end
 
-  definition trunc_Yx (x : X) : ∥ Y x ∥ := 
+  definition trunc_Yx (x : X) : ∥ Y x ∥ :=
   begin
     cases x, induction a_1, apply merely.intro,
     apply to_fun !equiv_subtype, rewrite a_1
   end
 
-  -- 3.8.5. There exists a type X and a family Y : X → U such that each Y(x) is a set, but such that (3.8.3) is false.
+  end example385
+  open example385
+
+  -- 3.8.5. There exists a type X and a family Y : X → U such that each Y(x) is a set,
+  -- but such that (3.8.3) is false.
   definition X_must_be_hset : Σ (X : Type.{1}) (Y : X -> Type.{1})
   (HA : Π x : X, is_hset (Y x)), ¬ ((Π x : X, ∥ Y x ∥) -> ∥ Π x : X, Y x ∥) :=
   ⟨X, Y, is_hset_Yx, λ H, trunc.rec_on (H trunc_Yx)
-  (λ H0, not_is_hset_X (@is_trunc_of_is_contr _ _ (is_contr.mk x0 H0)))⟩ 
+    (λ H0, not_is_hset_X (@is_trunc_of_is_contr _ _ (is_contr.mk x0 H0)))⟩
 
-end
+end choice

hott/types/bool.hlean

@@ -155,8 +155,11 @@ namespace bool
   assert H2 : bnot = id, from !cast_ua_fn⁻¹ ⬝ ap cast H,
   absurd (ap10 H2 tt) ff_ne_tt
 
+  theorem is_hset_bool : is_hset bool := _
+  theorem not_is_hprop_bool_eq_bool : ¬ is_hprop (bool = bool) :=
+  λ H, eq_bnot_ne_idp !is_hprop.elim
 
-  definition bool_equiv_option_unit : bool ≃ option unit :=
+  definition bool_equiv_option_unit [constructor] : bool ≃ option unit :=
   begin
     fapply equiv.MK,
     { intro b, cases b, exact none, exact some star},