From ebba33057c77fb5260498f1a699e3b6bf7f904d2 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 13 Mar 2015 12:13:50 -0400 Subject: [PATCH] feat(hott): add arity.hlean, about multivariate functions --- hott/algebra/precategory/functor.hlean | 112 ++++------------- hott/algebra/precategory/iso.hlean | 2 +- hott/algebra/precategory/yoneda.hlean | 1 + hott/arity.hlean | 159 +++++++++++++++++++++++++ hott/init/axioms/funext_of_ua.hlean | 18 +-- hott/init/path.hlean | 49 +------- hott/types/equiv.hlean | 2 +- 7 files changed, 196 insertions(+), 147 deletions(-) create mode 100644 hott/arity.hlean diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean index 15d1dffab..e4d493475 100644 --- a/hott/algebra/precategory/functor.hlean +++ b/hott/algebra/precategory/functor.hlean @@ -11,91 +11,6 @@ import .basic types.pi .iso open function category eq prod equiv is_equiv sigma sigma.ops is_trunc funext iso open pi - - - - section - - variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} - - definition homotopy2 [reducible] (f g : Πa b, C a b) : Type := - Πa b, f a b = g a b - - definition homotopy3 [reducible] (f g : Πa b c, D a b c) : Type := - Πa b c, f a b c = g a b c - notation f `∼2`:50 g := homotopy2 f g - notation f `∼3`:50 g := homotopy3 f g - - -- definition apD100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g := - -- λa b, eq.rec_on p idp - - definition apD100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g := - λa b, apD10 (apD10 p a) b - - definition apD1000 {f g : Πa b c, D a b c} (p : f = g) : f ∼3 g := - λa b c, apD100 (apD10 p a) b c - - definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f ∼2 g) : f = g := - eq_of_homotopy (λa, eq_of_homotopy (H a)) - - definition eq_of_homotopy3 {f g : Πa b c, D a b c} (H : f ∼3 g) : f = g := - eq_of_homotopy (λa, eq_of_homotopy2 (H a)) - - definition eq_of_homotopy2_id (f : Πa b, C a b) - : 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 - end - - definition eq_of_homotopy3_id (f : Πa b c, D a b c) - : eq_of_homotopy3 (λa b c, idpath (f a b c)) = idpath f := - 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 - end - - --TODO: put in namespace funext - definition is_equiv_apD100 [instance] (f g : Πa b, C a b) : is_equiv (@apD100 A B C f g) := - adjointify _ - eq_of_homotopy2 - begin - intro H, esimp {apD100,eq_of_homotopy2, function.compose}, - apply eq_of_homotopy, intro a, - apply concat, apply (ap (λx, @apD10 _ (λb : B a, _) _ _ (x a))), apply (retr apD10), ---TODO: remove implicit argument after #469 is closed - apply (retr apD10) - end - begin - intro p, cases p, apply eq_of_homotopy2_id - end - - definition is_equiv_apD1000 [instance] (f g : Πa b c, D a b c) : is_equiv (@apD1000 A B C D f g) := - adjointify _ - eq_of_homotopy3 - begin - intro H, apply eq_of_homotopy, intro a, - apply concat, {apply (ap (λx, @apD100 _ _ (λ(b : B a)(c : C a b), _) _ _ (x a))), apply (retr apD10)}, ---TODO: remove implicit argument after #469 is closed - apply (@retr _ _ apD100 !is_equiv_apD100) --is explicit argument needed here? - end - begin - intro p, cases p, apply eq_of_homotopy3_id - end - - protected definition homotopy2.rec_on {f g : Πa b, C a b} {P : (f ∼2 g) → Type} - (p : f ∼2 g) (H : Π(q : f = g), P (apD100 q)) : P p := - retr apD100 p ▹ H (eq_of_homotopy2 p) - - protected definition homotopy3.rec_on {f g : Πa b c, D a b c} {P : (f ∼3 g) → Type} - (p : f ∼3 g) (H : Π(q : f = g), P (apD1000 q)) : P p := - retr apD1000 p ▹ H (eq_of_homotopy3 p) - end - - - structure functor (C D : Precategory) : Type := (to_fun_ob : C → D) (to_fun_hom : Π ⦃a b : C⦄, hom a b → hom (to_fun_ob a) (to_fun_ob b)) @@ -221,20 +136,39 @@ namespace functor apply is_trunc_eq, apply is_trunc_succ, apply !homH}, end + definition functor_eq_eta' {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂} + (p : functor.mk ob₁ hom₁ id₁ comp₁ = functor.mk ob₂ hom₂ id₂ comp₂) + : p = p := --functor_eq_mk' _ _ _ _ (ap010 to_fun_ob p) _ := + sorry --set_option pp.universes true -- set_option pp.notation false -- set_option pp.implicit true - definition functor_eq2' {obF obF' : C → D} {homF homF' idF idF' compF compF'} - (p q : functor.mk obF homF idF compF = functor.mk obF' homF' idF' compF') (r : obF = obF') - : p = q := + -- TODO: REMOVE? + definition functor_eq2'' {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂} + {pob₁ pob₂ : ob₁ = ob₂} (phom₁ : pob₁ ▹ hom₁ = hom₂) (phom₂ : pob₂ ▹ hom₁ = hom₂) + (r : pob₁ = pob₂) : functor_eq_mk'' id₁ id₂ comp₁ comp₂ pob₁ phom₁ + = functor_eq_mk'' id₁ id₂ comp₁ comp₂ pob₂ phom₂ := begin cases r, + apply (ap (functor_eq_mk'' id₁ id₂ @comp₁ @comp₂ pob₂)), + apply is_hprop.elim + end + + definition functor_eq2' {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂} {pob₁ pob₂ : ob₁ ∼ ob₂} +(phom₁ : Π(a b : C) (f : hom a b), hom_of_eq (pob₁ b) ∘ hom₁ a b f ∘ inv_of_eq (pob₁ a) = hom₂ a b f) +(phom₂ : Π(a b : C) (f : hom a b), hom_of_eq (pob₂ b) ∘ hom₁ a b f ∘ inv_of_eq (pob₂ a) = hom₂ a b f) + (r : pob₁ = pob₂) : functor_eq_mk' id₁ id₂ comp₁ comp₂ pob₁ phom₁ + = functor_eq_mk' id₁ id₂ comp₁ comp₂ pob₂ phom₂ := + begin + cases r, + apply (ap (functor_eq_mk' id₁ id₂ @comp₁ @comp₂ pob₂)), + apply is_hprop.elim end definition functor_eq2 {F₁ F₂ : C ⇒ D} (p q : F₁ = F₂) (r : ap010 to_fun_ob p ∼ ap010 to_fun_ob q) : p = q := begin - + apply sorry end -- definition ap010_functor_eq_mk' {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ = to_fun_ob F₂) diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean index cf946838f..1ef412efa 100644 --- a/hott/algebra/precategory/iso.hlean +++ b/hott/algebra/precategory/iso.hlean @@ -6,7 +6,7 @@ Module: algebra.precategory.iso Author: Floris van Doorn, Jakob von Raumer -/ -import algebra.precategory.basic types.sigma +import algebra.precategory.basic types.sigma arity open eq category prod equiv is_equiv sigma sigma.ops is_trunc diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean index 0d7a8f3ce..47b8c0dce 100644 --- a/hott/algebra/precategory/yoneda.hlean +++ b/hott/algebra/precategory/yoneda.hlean @@ -125,6 +125,7 @@ namespace functor functor.mk (functor_uncurry_ob G) (functor_uncurry_hom G) (functor_uncurry_id G) + (functor_uncurry_comp G) theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F := functor_eq_mk (λp, ap (to_fun_ob F) !prod.eta) diff --git a/hott/arity.hlean b/hott/arity.hlean new file mode 100644 index 000000000..4ece88c3a --- /dev/null +++ b/hott/arity.hlean @@ -0,0 +1,159 @@ +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: init.path +Author: Floris van Doorn + +Theorems about functions with multiple arguments +-/ + +variables {A U V W X Y Z : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} + {E : Πa b c, D a b c → Type} +variables {a a' : A} {u u' : U} {v v' : V} {w w' : W} {x x' : X} {y y' : Y} + {b : B a} {b' : B a'} + {c : C a b} {c' : C a' b'} + {d : D a b c} {d' : D a' b' c'} + +namespace eq + /- + Naming convention: + The theorem which states how to construct an path between two function applications is + api₀i₁...iₙ. + Here i₀, ... iₙ are digits, n is the arity of the function(s), + and iⱼ specifies the dimension of the path between the jᵗʰ argument + (i₀ specifies the dimension of the path between the functions). + A value iⱼ ≡ 0 means that the jᵗʰ arguments are definitionally equal + The functions are non-dependent, except when the theorem name contains trailing zeroes + (where the function is dependent only in the arguments where it doesn't result in any + transports in the theorem statement). + For the fully-dependent versions (except that the conclusion doesn't contain a transport) + we write + apDi₀i₁...iₙ. + + For versions where only some arguments depend on some other arguments, + or for versions with transport in the conclusion (like apD), we don't have a + consistent naming scheme (yet). + + We don't prove each theorem systematically, but prove only the ones which we actually need. + -/ + + definition homotopy2 [reducible] (f g : Πa b, C a b) : Type := + Πa b, f a b = g a b + definition homotopy3 [reducible] (f g : Πa b c, D a b c) : Type := + Πa b c, f a b c = g a b c + definition homotopy4 [reducible] (f g : Πa b c d, E a b c d) : Type := + Πa b c d, f a b c d = g a b c d + + notation f `∼2`:50 g := homotopy2 f g + notation f `∼3`:50 g := homotopy3 f g + + definition ap011 (f : U → V → W) (Hu : u = u') (Hv : v = v') : f u v = f u' v' := + eq.rec_on Hu (ap (f u) Hv) + + definition ap0111 (f : U → V → W → X) (Hu : u = u') (Hv : v = v') (Hw : w = w') + : f u v w = f u' v' w' := + eq.rec_on Hu (ap011 (f u) Hv Hw) + + definition ap01111 (f : U → V → W → X → Y) (Hu : u = u') (Hv : v = v') (Hw : w = w') (Hx : x = x') + : f u v w x = f u' v' w' x' := + eq.rec_on Hu (ap0111 (f u) Hv Hw Hx) + + definition ap010 (f : X → Πa, B a) (Hx : x = x') : f x ∼ f x' := + λa, eq.rec_on Hx idp + + definition ap0100 (f : X → Πa b, C a b) (Hx : x = x') : f x ∼2 f x' := + λa b, eq.rec_on Hx idp + + definition ap01000 (f : X → Πa b c, D a b c) (Hx : x = x') : f x ∼3 f x' := + λa b c, eq.rec_on Hx idp + + definition apD011 (f : Πa, B a → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b') + : f a b = f a' b' := + eq.rec_on Hb (eq.rec_on Ha idp) + + definition apD0111 (f : Πa b, C a b → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b') + (Hc : apD011 C Ha Hb ▹ c = c') + : f a b c = f a' b' c' := + eq.rec_on Hc (eq.rec_on Hb (eq.rec_on Ha idp)) + + definition apD01111 (f : Πa b c, D a b c → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b') + (Hc : apD011 C Ha Hb ▹ c = c') (Hd : apD0111 D Ha Hb Hc ▹ d = d') + : f a b c d = f a' b' c' d' := + eq.rec_on Hd (eq.rec_on Hc (eq.rec_on Hb (eq.rec_on Ha idp))) + + definition apD100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g := + λa b, apD10 (apD10 p a) b + + definition apD1000 {f g : Πa b c, D a b c} (p : f = g) : f ∼3 g := + λa b c, apD100 (apD10 p a) b c + + /- the following theorems are function extentionality for functions with multiple arguments -/ + + definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f ∼2 g) : f = g := + eq_of_homotopy (λa, eq_of_homotopy (H a)) + + definition eq_of_homotopy3 {f g : Πa b c, D a b c} (H : f ∼3 g) : f = g := + eq_of_homotopy (λa, eq_of_homotopy2 (H a)) + + definition eq_of_homotopy2_id (f : Πa b, C a b) + : 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 + end + + definition eq_of_homotopy3_id (f : Πa b c, D a b c) + : eq_of_homotopy3 (λa b c, idpath (f a b c)) = idpath f := + 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 + end +end eq + +open is_equiv eq +namespace funext + definition is_equiv_apD100 [instance] (f g : Πa b, C a b) : is_equiv (@apD100 A B C f g) := + adjointify _ + eq_of_homotopy2 + begin + intro H, esimp {apD100,eq_of_homotopy2, function.compose}, + apply eq_of_homotopy, intro a, + apply concat, apply (ap (λx, @apD10 _ (λb : B a, _) _ _ (x a))), apply (retr apD10), +--TODO: remove implicit argument after #469 is closed + apply (retr apD10) + end + begin + intro p, cases p, apply eq_of_homotopy2_id + end + + definition is_equiv_apD1000 [instance] (f g : Πa b c, D a b c) + : is_equiv (@apD1000 A B C D f g) := + adjointify _ + eq_of_homotopy3 + begin + intro H, apply eq_of_homotopy, intro a, + apply concat, + {apply (ap (λx, @apD100 _ _ (λ(b : B a)(c : C a b), _) _ _ (x a))), + apply (retr apD10)}, +--TODO: remove implicit argument after #469 is closed + apply (@retr _ _ apD100 !is_equiv_apD100) --is explicit argument needed here? + end + begin + intro p, cases p, apply eq_of_homotopy3_id + end +end funext + +namespace eq + open funext + local attribute funext.is_equiv_apD100 [instance] + protected definition homotopy2.rec_on {f g : Πa b, C a b} {P : (f ∼2 g) → Type} + (p : f ∼2 g) (H : Π(q : f = g), P (apD100 q)) : P p := + retr apD100 p ▹ H (eq_of_homotopy2 p) + + protected definition homotopy3.rec_on {f g : Πa b c, D a b c} {P : (f ∼3 g) → Type} + (p : f ∼3 g) (H : Π(q : f = g), P (apD1000 q)) : P p := + retr apD1000 p ▹ H (eq_of_homotopy3 p) +end eq diff --git a/hott/init/axioms/funext_of_ua.hlean b/hott/init/axioms/funext_of_ua.hlean index d4095e6d3..ddeeec0ee 100644 --- a/hott/init/axioms/funext_of_ua.hlean +++ b/hott/init/axioms/funext_of_ua.hlean @@ -135,28 +135,28 @@ theorem weak_funext_of_ua : weak_funext := definition funext_of_ua : funext := funext_of_weak_funext (@weak_funext_of_ua) +variables {A : Type} {P : A → Type} {f g : Π x, P x} + namespace funext - definition is_equiv_apD [instance] {A : Type} {P : A → Type} (f g : Π x, P x) - : is_equiv (@apD10 A P f g) := + definition is_equiv_apD [instance] (f g : Π x, P x) : is_equiv (@apD10 A P f g) := funext_of_ua f g end funext open funext -definition eq_equiv_homotopy {A : Type} {P : A → Type} {f g : Π x, P x} : (f = g) ≃ (f ∼ g) := +definition eq_equiv_homotopy : (f = g) ≃ (f ∼ g) := equiv.mk apD10 _ -definition eq_of_homotopy {A : Type} {P : A → Type} {f g : Π x, P x} : f ∼ g → f = g := +definition eq_of_homotopy [reducible] : f ∼ g → f = g := (@apD10 A P f g)⁻¹ ---rename to eq_of_homotopy_idp -definition eq_of_homotopy_id {A : Type} {P : A → Type} (f : Π x, P x) - : eq_of_homotopy (λx : A, idpath (f x)) = idpath f := +--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 := is_equiv.sect apD10 idp definition naive_funext_of_ua : naive_funext := λ A P f g h, eq_of_homotopy h -protected definition homotopy.rec_on {A : Type} {B : A → Type} {f g : Πa, B a} {P : (f ∼ g) → Type} - (p : f ∼ g) (H : Π(q : f = g), P (apD10 q)) : P p := +protected definition homotopy.rec_on {Q : (f ∼ g) → Type} (p : f ∼ g) + (H : Π(q : f = g), Q (apD10 q)) : Q p := retr apD10 p ▹ H (eq_of_homotopy p) diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 9c74d2176..7767d3d9e 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -3,7 +3,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Module: init.path -Author: Jeremy Avigad, Jakob von Raumer, Floris van Doorn +Authors: Jeremy Avigad, Jakob von Raumer, Floris van Doorn Ported from Coq HoTT -/ @@ -186,7 +186,7 @@ namespace eq definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x = y) : f x = f y := eq.rec_on p idp - definition ap01 := ap + definition ap01 [reducible] := ap definition homotopy [reducible] (f g : Πx, P x) : Type := Πx : A, f x = g x @@ -590,8 +590,6 @@ namespace eq (whisker_right a q) ⬝ (whisker_left p' b) = (whisker_left p b) ⬝ (whisker_right a q') := eq.rec_on b (eq.rec_on a (idp_con _)⁻¹) - - -- Structure corresponding to the coherence equations of a bicategory. -- The "pentagonator": the 3-cell witnessing the associativity pentagon. @@ -630,7 +628,6 @@ namespace eq ⬝ (ap02 f r ◾ ap02 f s) ⬝ (ap_con f p' q')⁻¹ := eq.rec_on r (eq.rec_on s (eq.rec_on q (eq.rec_on p idp))) - -- eq.rec_on r (eq.rec_on s (eq.rec_on p (eq.rec_on q idp))) definition apD02 {p q : x = y} (f : Π x, P x) (r : p = q) : apD f p = transport2 P r (f x) ⬝ apD f q := @@ -645,45 +642,3 @@ namespace eq ⬝ (whisker_right (tr2_con P r1 r2 (f x))⁻¹ (apD f p3)) := eq.rec_on r2 (eq.rec_on r1 (eq.rec_on p1 idp)) end eq - -namespace eq - section - variables {A B C D E : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} - - definition ap011 (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' := - eq.rec_on Ha (eq.rec_on Hb idp) - - definition ap0111 (f : A → B → C → D) (Ha : a = a') (Hb : b = b') (Hc : c = c') - : f a b c = f a' b' c' := - eq.rec_on Ha (ap011 (f a) Hb Hc) - - definition ap01111 (f : A → B → C → D → E) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') - : f a b c d = f a' b' c' d' := - eq.rec_on Ha (ap0111 (f a) Hb Hc Hd) - - definition ap010 {C : B → Type} (f : A → Π(b : B), C b) (Ha : a = a') (b : B) : f a b = f a' b := - eq.rec_on Ha idp - end - section - variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} - {E : Πa b c, D a b c → Type} {F : Type} - variables {a a' : A} - {b : B a} {b' : B a'} - {c : C a b} {c' : C a' b'} - {d : D a b c} {d' : D a' b' c'} - - definition apD011 (f : Πa, B a → F) (Ha : a = a') (Hb : (Ha ▹ b) = b') - : f a b = f a' b' := - eq.rec_on Hb (eq.rec_on Ha idp) - - definition apD0111 (f : Πa b, C a b → F) (Ha : a = a') (Hb : (Ha ▹ b) = b') - (Hc : apD011 C Ha Hb ▹ c = c') - : f a b c = f a' b' c' := - eq.rec_on Hc (eq.rec_on Hb (eq.rec_on Ha idp)) - - definition apD01111 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : (Ha ▹ b) = b') - (Hc : apD011 C Ha Hb ▹ c = c') (Hd : apD0111 D Ha Hb Hc ▹ d = d') - : f a b c d = f a' b' c' d' := - eq.rec_on Hd (eq.rec_on Hc (eq.rec_on Hb (eq.rec_on Ha idp))) - end -end eq diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index c43172f79..1dc62f774 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -9,7 +9,7 @@ Ported from Coq HoTT Theorems about the types equiv and is_equiv -/ -import types.fiber types.arrow +import types.fiber types.arrow arity open eq is_trunc sigma sigma.ops arrow pi