fix(hott): make f explicit in is_equiv.mk and a bit of renaming in init

2015-04-24 18:51:16 -04:00 · 2015-04-24 18:51:16 -04:00 · 86012d841b
commit 86012d841b
parent e769fdd9dc
8 changed files with 31 additions and 33 deletions
--- a/hott/arity.hlean
+++ b/hott/arity.hlean
@ -112,8 +112,8 @@ namespace eq
    : eq_of_homotopy2 (λa b, idpath (f a b)) = idpath f :=
  begin
    apply concat,
-      {apply (ap (λx, eq_of_homotopy x)), apply eq_of_homotopy, intro a, apply eq_of_homotopy_id},
-    apply eq_of_homotopy_id
+      {apply (ap (λx, eq_of_homotopy x)), apply eq_of_homotopy, intro a, apply eq_of_homotopy_idp},
+    apply eq_of_homotopy_idp
  end

  definition eq_of_homotopy3_id (f : Πa b c, D a b c)
@ -121,7 +121,7 @@ namespace eq
  begin
    apply concat,
      {apply (ap (λx, eq_of_homotopy x)), apply eq_of_homotopy, intro a, apply eq_of_homotopy2_id},
-    apply eq_of_homotopy_id
+    apply eq_of_homotopy_idp
  end

 end eq
--- a/hott/init/axioms/funext_of_ua.hlean
+++ b/hott/init/axioms/funext_of_ua.hlean
@ -151,7 +151,7 @@ definition eq_of_homotopy [reducible] : f ∼ g → f = g :=
 (@apd10 A P f g)⁻¹

 --TODO: rename to eq_of_homotopy_idp
-definition eq_of_homotopy_id (f : Π x, P x) : eq_of_homotopy (λx : A, idpath (f x)) = idpath f :=
+definition eq_of_homotopy_idp (f : Π x, P x) : eq_of_homotopy (λx : A, idpath (f x)) = idpath f :=
 is_equiv.sect apd10 idp

 definition naive_funext_of_ua : naive_funext :=
--- a/hott/init/axioms/funext_varieties.hlean
+++ b/hott/init/axioms/funext_varieties.hlean
@ -25,7 +25,6 @@ definition funext.{l k} :=
  Π ⦃A : Type.{l}⦄ {P : A → Type.{k}} (f g : Π x, P x), is_equiv (@apd10 A P f g)

 -- Naive funext is the simple assertion that pointwise equal functions are equal.
-- TODO think about universe levels
 definition naive_funext :=
  Π ⦃A : Type⦄ {P : A → Type} (f g : Πx, P x), (f ∼ g) → f = g

@ -67,7 +66,7 @@ section
          have t2 : is_contr (Πx, Σ y, f x = y),
            from !wf,
          have t3 : (λ x, @sigma.mk _ (λ y, f x = y) (f x) idp) = s g h,
-            from @center_eq (Π x, Σ y, f x = y) t2 _ _,
+            from @eq_of_is_contr (Π x, Σ y, f x = y) t2 _ _,
          have t4 : r (λ x, sigma.mk (f x) idp) = r (s g h),
            from ap r t3,
          have endt : sigma.mk f (homotopy.refl f) = sigma.mk g h,
@ -80,12 +79,12 @@ section

  definition homotopy_ind (g : Πx, B x) (h : f ∼ g) : Q g h :=
    @transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f (homotopy.refl f)) (sigma.mk g h)
-      (@center_eq _ is_contr_sigma_homotopy _ _) d
+      (@eq_of_is_contr _ is_contr_sigma_homotopy _ _) d

  local attribute weak_funext [reducible]
  local attribute homotopy_ind [reducible]
  definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d :=
-    (@hprop_eq_of_is_contr _ _ _ _ !center_eq idp)⁻¹ ▹ idp
+    (@hprop_eq_of_is_contr _ _ _ _ !eq_of_is_contr idp)⁻¹ ▹ idp
 end

 -- Now the proof is fairly easy; we can just use the same induction principle on both sides.
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@ -17,6 +17,7 @@ open eq function
 -- This is our definition of equivalence. In the HoTT-book it's called
 -- ihae (half-adjoint equivalence).
 structure is_equiv [class] {A B : Type} (f : A → B) :=
+mk' ::
  (inv : B → A)
  (retr : (f ∘ inv) ∼ id)
  (sect : (inv ∘ f) ∼ id)
@ -33,19 +34,22 @@ structure equiv (A B : Type) :=
 namespace is_equiv
  /- Some instances and closure properties of equivalences -/
  postfix `⁻¹` := inv
-  --a second notation for the inverse, which is not overloaded
+  /- a second notation for the inverse, which is not overloaded -/
  postfix [parsing-only] `⁻¹ᵉ`:std.prec.max_plus := inv

  section
  variables {A B C : Type} (f : A → B) (g : B → C) {f' : A → B}

+  -- The variant of mk' where f is explicit.
+  protected abbreviation mk := @is_equiv.mk' A B f
+
  -- The identity function is an equivalence.
-  -- TODO: make A explicit
-  definition is_equiv_id : (@is_equiv A A id) := is_equiv.mk id (λa, idp) (λa, idp) (λa, idp)
+  definition is_equiv_id (A : Type) : (@is_equiv A A id) :=
+  is_equiv.mk id id (λa, idp) (λa, idp) (λa, idp)

  -- The composition of two equivalences is, again, an equivalence.
  definition is_equiv_compose [Hf : is_equiv f] [Hg : is_equiv g] : is_equiv (g ∘ f) :=
-    is_equiv.mk ((inv f) ∘ (inv g))
+    is_equiv.mk (g ∘ f) (f⁻¹ ∘ g⁻¹)
               (λc, ap g (retr f (g⁻¹ c)) ⬝ retr g c)
               (λa, ap (inv f) (sect g (f a)) ⬝ sect f a)
               (λa, (whisker_left _ (adj g (f a))) ⬝
@ -92,7 +96,7 @@ namespace is_equiv
          ... = (ap f' (ap invf ff'a)⁻¹) ⬝ ap f' secta : by rewrite ap_inv
          ... = ap f' ((ap invf ff'a)⁻¹ ⬝ secta)       : by rewrite ap_con,
    eq3) in
-  is_equiv.mk (inv f) sect' retr' adj'
+  is_equiv.mk f' (inv f) sect' retr' adj'
  end

  section
@ -133,8 +137,7 @@ namespace is_equiv
        from eq_of_idp_eq_inv_con eq3,
      eq4)

-  definition adjointify : is_equiv f :=
-    is_equiv.mk g ret adjointify_sect' adjointify_adj'
+  definition adjointify : is_equiv f := is_equiv.mk f g ret adjointify_sect' adjointify_adj'

  end

@ -213,7 +216,7 @@ namespace is_equiv

  --Transporting is an equivalence
  definition is_equiv_tr [instance] {A : Type} (P : A → Type) {x y : A} (p : x = y) : (is_equiv (transport P p)) :=
-    is_equiv.mk (transport P p⁻¹) (tr_inv_tr P p) (inv_tr_tr P p) (tr_inv_tr_lemma P p)
+    is_equiv.mk _ (transport P p⁻¹) (tr_inv_tr P p) (inv_tr_tr P p) (tr_inv_tr_lemma P p)


 end is_equiv
--- a/hott/init/function.hlean
+++ b/hott/init/function.hlean
@ -13,7 +13,7 @@ import init.reserved_notation

 namespace function

-variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
+variables {A B C D E : Type}

 definition compose [reducible] (f : B → C) (g : A → B) : A → C :=
 λx, f (g x)
@ -44,8 +44,6 @@ precedence `∘'`:60
 precedence `on`:1
 precedence `$`:1

-variables {f g : A → B}
-

 infixr  ∘                  := compose
 infixr  ∘'                 := dcompose
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@ -101,16 +101,15 @@ namespace is_trunc
  definition contr [H : is_contr A] (a : A) : !center = a :=
  @contr_internal.contr A !is_trunc.to_internal a

-  --TODO: rename
-  definition center_eq [H : is_contr A] (x y : A) : x = y :=
+  definition eq_of_is_contr [H : is_contr A] (x y : A) : x = y :=
  (contr x)⁻¹ ⬝ (contr y)

  definition hprop_eq_of_is_contr {A : Type} [H : is_contr A] {x y : A} (p q : x = y) : p = q :=
-  have K : ∀ (r : x = y), center_eq x y = r, from (λ r, eq.rec_on r !con.left_inv),
+  have K : ∀ (r : x = y), eq_of_is_contr x y = r, from (λ r, eq.rec_on r !con.left_inv),
  (K p)⁻¹ ⬝ K q

  definition is_contr_eq {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) :=
-  is_contr.mk !center_eq (λ p, !hprop_eq_of_is_contr)
+  is_contr.mk !eq_of_is_contr (λ p, !hprop_eq_of_is_contr)
  local attribute is_contr_eq [instance]

  /- truncation is upward close -/
@ -236,7 +235,7 @@ namespace is_trunc

  definition is_equiv_of_is_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A)
    : is_equiv f :=
-  is_equiv.mk g (λb, !is_hprop.elim) (λa, !is_hprop.elim) (λa, !is_hset.elim)
+  is_equiv.mk f g (λb, !is_hprop.elim) (λa, !is_hprop.elim) (λa, !is_hset.elim)

  definition equiv_of_is_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A)
    : A ≃ B :=
@ -252,11 +251,10 @@ namespace is_trunc
  open equiv
  -- A contractible type is equivalent to [Unit]. *)
  definition equiv_unit_of_is_contr [H : is_contr A] : A ≃ unit :=
-    equiv.mk (λ (x : A), ⋆)
-      (is_equiv.mk (λ (u : unit), center A)
-        (λ (u : unit), unit.rec_on u idp)
-        (λ (x : A), contr x)
-        (λ (x : A), !ap_constant⁻¹))
+  equiv.MK (λ (x : A), ⋆)
+           (λ (u : unit), center A)
+           (λ (u : unit), unit.rec_on u idp)
+           (λ (x : A), contr x)

  -- TODO: port "Truncated morphisms"

--- a/hott/types/eq.hlean
+++ b/hott/types/eq.hlean
@ -137,7 +137,7 @@ namespace eq
  /- Path operations are equivalences -/

  definition is_equiv_eq_inverse (a1 a2 : A) : is_equiv (@inverse A a1 a2) :=
-  is_equiv.mk inverse inv_inv inv_inv (λp, eq.rec_on p idp)
+  is_equiv.mk inverse inverse inv_inv inv_inv (λp, eq.rec_on p idp)
  local attribute is_equiv_eq_inverse [instance]

  definition eq_equiv_eq_symm (a1 a2 : A) : (a1 = a2) ≃ (a2 = a1) :=
@ -145,7 +145,7 @@ namespace eq

  definition is_equiv_concat_left [instance] (p : a1 = a2) (a3 : A)
    : is_equiv (@concat _ a1 a2 a3 p) :=
-  is_equiv.mk (concat p⁻¹)
+  is_equiv.mk (concat p) (concat p⁻¹)
              (con_inv_cancel_left p)
              (inv_con_cancel_left p)
              (eq.rec_on p (λq, eq.rec_on q idp))
@ -156,7 +156,7 @@ namespace eq

  definition is_equiv_concat_right [instance] (p : a2 = a3) (a1 : A)
    : is_equiv (λq : a1 = a2, q ⬝ p) :=
-  is_equiv.mk (λq, q ⬝ p⁻¹)
+  is_equiv.mk (λq, q ⬝ p) (λq, q ⬝ p⁻¹)
              (λq, inv_con_cancel_right q p)
              (λq, con_inv_cancel_right q p)
              (eq.rec_on p (λq, eq.rec_on q idp))
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@ -60,7 +60,7 @@ namespace is_equiv
  protected definition sigma_char : (is_equiv f) ≃
  (Σ(g : B → A) (ε : f ∘ g ∼ id) (η : g ∘ f ∼ id), Π(a : A), ε (f a) = ap f (η a)) :=
  equiv.MK (λH, ⟨inv f, retr f, sect f, adj f⟩)
-           (λp, is_equiv.mk p.1 p.2.1 p.2.2.1 p.2.2.2)
+           (λp, is_equiv.mk f p.1 p.2.1 p.2.2.1 p.2.2.2)
           (λp, begin
                  cases p with [p1, p2],
                  cases p2 with [p21, p22],