From ae92e8c94d614def8ef0b3510005a46b844ab8b6 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 22 Nov 2015 01:37:13 -0500 Subject: [PATCH] feat(hit/two_quotient): give dependent eliminator for two_quotients --- hott/algebra/e_closure.hlean | 80 ++++++++++++------ hott/cubical/cubical.md | 6 +- hott/cubical/pathover2.hlean | 97 ++++++++++++++++++++-- hott/cubical/square2.hlean | 34 ++++++++ hott/cubical/squareover.hlean | 15 ++++ hott/eq2.hlean | 10 +-- hott/hit/two_quotient.hlean | 152 +++++++++++++++++++++++++++++----- hott/init/pathover.hlean | 7 +- hott/types/equiv.hlean | 2 +- 9 files changed, 336 insertions(+), 67 deletions(-) create mode 100644 hott/cubical/square2.hlean diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean index 0d5993b64..c1ad224f3 100644 --- a/hott/algebra/e_closure.hlean +++ b/hott/algebra/e_closure.hlean @@ -8,7 +8,7 @@ A more appropriate intuition is the type of words formed from the relation, and inverses, concatenations and reflexivity -/ -import .relation eq2 arity +import algebra.relation eq2 arity cubical.pathover2 open eq equiv @@ -24,7 +24,7 @@ namespace e_closure notation `[`:max a `]`:0 := e_closure.of_rel a abbreviation rfl {A : Type} {R : A → A → Type} {a : A} := of_path R (idpath a) end e_closure - +open e_closure namespace relation section @@ -57,11 +57,37 @@ section exact ap_con g (e_closure.elim e r) (e_closure.elim e r') ⬝ (IH₁ ◾ IH₂) end +/- definition ap_e_closure_elim_h_inv [unfold_full] {B C : Type} {f : A → B} {g : B → C} + (e : Π⦃a a' : A⦄, R a a' → f a = f a') + {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')} + (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a') + : ap_e_closure_elim_h e p t⁻¹ʳ = ap_inv g (e_closure.elim e t) ⬝ (ap_e_closure_elim_h e p t)⁻² := + by reflexivity + + definition ap_e_closure_elim_h_con [unfold_full] {B C : Type} {f : A → B} {g : B → C} + (e : Π⦃a a' : A⦄, R a a' → f a = f a') + {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')} + (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a') (t' : T a' a'') + : ap_e_closure_elim_h e p (t ⬝r t') = ap_con g (e_closure.elim e t) (e_closure.elim e t') ⬝ + (ap_e_closure_elim_h e p t ◾ ap_e_closure_elim_h e p t') := + by reflexivity-/ + definition ap_e_closure_elim [unfold 10] {B C : Type} {f : A → B} (g : B → C) - (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') + (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') : ap g (e_closure.elim e t) = e_closure.elim (λa a' r, ap g (e r)) t := ap_e_closure_elim_h e (λa a' s, idp) t + definition ap_e_closure_elim_inv [unfold_full] {B C : Type} {f : A → B} (g : B → C) + (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') + : ap_e_closure_elim g e t⁻¹ʳ = ap_inv g (e_closure.elim e t) ⬝ (ap_e_closure_elim g e t)⁻² := + by reflexivity + + definition ap_e_closure_elim_con [unfold_full] {B C : Type} {f : A → B} (g : B → C) + (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') (t' : T a' a'') + : ap_e_closure_elim g e (t ⬝r t') = ap_con g (e_closure.elim e t) (e_closure.elim e t') ⬝ + (ap_e_closure_elim g e t ◾ ap_e_closure_elim g e t') := + by reflexivity + definition ap_e_closure_elim_h_eq {B C : Type} {f : A → B} {g : B → C} (e : Π⦃a a' : A⦄, R a a' → f a = f a') {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')} @@ -107,7 +133,6 @@ section (ap_e_closure_elim h (λa a' r, ap g (e r)) t) := !ap_ap_e_closure_elim_h - open e_closure definition is_equivalence_e_closure : is_equivalence T := begin constructor, @@ -131,13 +156,12 @@ section : e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t ⬝ (ap f p) := by induction p; esimp; exact !idp_con⁻¹ - --dependent elimination: + /- dependent elimination -/ variables {P : B → Type} {Q : C → Type} {f : A → B} {g : B → C} {f' : Π(a : A), P (f a)} - protected definition e_closure.elimo [unfold 11] - (p : Π⦃a a' : A⦄, R a a' → f a = f a') - (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a') - (t : T a a') : f' a =[e_closure.elim p t] f' a' := + protected definition e_closure.elimo [unfold 11] (p : Π⦃a a' : A⦄, R a a' → f a = f a') + (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a') (t : T a a') + : f' a =[e_closure.elim p t] f' a' := begin induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂, exact po r, @@ -146,6 +170,16 @@ section exact IH₁ ⬝o IH₂ end + definition elimo_inv [unfold_full] (p : Π⦃a a' : A⦄, R a a' → f a = f a') + (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a') (t : T a a') + : e_closure.elimo p po t⁻¹ʳ = (e_closure.elimo p po t)⁻¹ᵒ := + by reflexivity + + definition elimo_con [unfold_full] (p : Π⦃a a' : A⦄, R a a' → f a = f a') + (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a') (t : T a a') (t' : T a' a'') + : e_closure.elimo p po (t ⬝r t') = e_closure.elimo p po t ⬝o e_closure.elimo p po t' := + by reflexivity + definition ap_e_closure_elimo_h [unfold 12] {g' : Πb, Q (g b)} (p : Π⦃a a' : A⦄, R a a' → f a = f a') (po : Π⦃a a' : A⦄ (s : R a a'), g' (f a) =[p s] g' (f a')) @@ -160,29 +194,21 @@ section exact apdo_con g' (e_closure.elim p r) (e_closure.elim p r') ⬝ (IH₁ ◾o IH₂) end -/- - definition e_closure_elimo_ap {g' : Π(a : A), Q (g (f a))} + theorem e_closure_elimo_ap {g' : Π(a : A), Q (g (f a))} (p : Π⦃a a' : A⦄, R a a' → f a = f a') (po : Π⦃a a' : A⦄ (s : R a a'), g' a =[ap g (p s)] g' a') - (t : T a a') : e_closure.elimo (λa a' r, ap g (p r)) po t = - change_path (ap_e_closure_elim g p t) - (pathover_ap Q g (e_closure.elimo p (λa a' s, pathover_of_pathover_ap Q g (po s)) t)) := + (t : T a a') : e_closure.elimo p (λa a' s, pathover_of_pathover_ap Q g (po s)) t = + pathover_of_pathover_ap Q g (change_path (ap_e_closure_elim g p t)⁻¹ + (e_closure.elimo (λa a' r, ap g (p r)) po t)) := begin induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂, - { esimp, exact (to_right_inv !pathover_compose (po r))⁻¹}, - { induction pp, reflexivity}, - { exact sorry}, - { exact sorry}, + { reflexivity}, + { induction pp; reflexivity}, + { rewrite [+elimo_inv, ap_e_closure_elim_inv, IH, con_inv, change_path_con, ▸*, -inv2_inv, + change_path_invo, pathover_of_pathover_ap_invo]}, + { rewrite [+elimo_con, ap_e_closure_elim_con, IH₁, IH₂, con_inv, change_path_con, ▸*, con2_inv, + change_path_cono, pathover_of_pathover_ap_cono]}, end - definition e_closure_elimo_ap' {g' : Π(a : A), Q (g (f a))} - (p : Π⦃a a' : A⦄, R a a' → f a = f a') - (po : Π⦃a a' : A⦄ (s : R a a'), g' a =[ap g (p s)] g' a') - (t : T a a') : - pathover_of_pathover_ap Q g (change_path (ap_e_closure_elim g p t)⁻¹ (e_closure.elimo (λa a' r, ap g (p r)) po t)) = - e_closure.elimo p (λa a' s, pathover_of_pathover_ap Q g (po s)) t := - sorry --/ - end end relation diff --git a/hott/cubical/cubical.md b/hott/cubical/cubical.md index 4008f1ff0..62fce5fa5 100644 --- a/hott/cubical/cubical.md +++ b/hott/cubical/cubical.md @@ -8,4 +8,8 @@ The files [path](../init/path.hlean) and [pathover](../init/pathover.hlean) are * [square](square.hlean): square in a type * [cube](cube.hlean): cube in a type * [squareover](squareover.hlean): square over a square -* [cubeover](cubeover.hlean): cube over a cube \ No newline at end of file +* [cubeover](cubeover.hlean): cube over a cube + +The following files are higher coherence laws between operators defined in the basic files +* [pathover2](pathover2.hlean) +* [square2](square2.hlean) diff --git a/hott/cubical/pathover2.hlean b/hott/cubical/pathover2.hlean index 71371e311..addbf9ace 100644 --- a/hott/cubical/pathover2.hlean +++ b/hott/cubical/pathover2.hlean @@ -6,12 +6,15 @@ Author: Floris van Doorn Coherence conditions for operations on pathovers -/ -open function +open function equiv namespace eq - variables {A A' A'' : Type} {a a' a₂ : A} (B : A → Type) {p : a = a₂} - {b b' : B a} {b₂ : B a₂} + variables {A A' A'' : Type} {B B' : A → Type} {B'' : A' → Type} {C : Π⦃a⦄, B a → Type} + {a a₂ a₃ a₄ : A} {p p' p'' : a = a₂} {p₂ p₂' : a₂ = a₃} {p₃ : a₃ = a₄} {p₁₃ : a = a₃} + {a' : A'} + {b b' : B a} {b₂ b₂' : B a₂} {b₃ : B a₃} {b₄ : B a₄} + {c : C b} {c₂ : C b₂} definition pathover_ap_id (q : b =[p] b₂) : pathover_ap B id q = change_path (ap_id p)⁻¹ q := by induction q; reflexivity @@ -27,10 +30,6 @@ namespace eq = change_path (ap_compose g f p) (pathover_ap B (g ∘ f) q) := by induction q; reflexivity - definition apdo_eq_apdo_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a') - : apdo (λx, g (f x)) p = pathover_of_pathover_ap B f (apdo g (ap f p)) := - by induction p; reflexivity - definition pathover_of_tr_eq_idp (r : b = b') : pathover_of_tr_eq r = pathover_idp_of_eq r := idp @@ -42,4 +41,88 @@ namespace eq : apo011 f p q = eq_of_pathover (apo11 (apdo f p) q) := by induction q; reflexivity + definition change_path_con (q : p = p') (q' : p' = p'') (r : b =[p] b₂) : + change_path (q ⬝ q') r = change_path q' (change_path q r) := + by induction q; induction q'; reflexivity + + definition change_path_invo (q : p = p') (r : b =[p] b₂) : + change_path (inverse2 q) r⁻¹ᵒ = (change_path q r)⁻¹ᵒ := + by induction q; reflexivity + + definition change_path_cono (q : p = p') (q₂ : p₂ = p₂') (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃): + change_path (q ◾ q₂) (r ⬝o r₂) = change_path q r ⬝o change_path q₂ r₂ := + by induction q; induction q₂; reflexivity + + definition pathover_of_pathover_ap_invo (B' : A' → Type) (f : A → A') + {b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[ap f p] b₂) : + pathover_of_pathover_ap B' f (change_path (ap_inv f p)⁻¹ q⁻¹ᵒ) = + (pathover_of_pathover_ap B' f q)⁻¹ᵒ:= + by induction p; eapply idp_rec_on q; reflexivity + + definition pathover_of_pathover_ap_cono (B' : A' → Type) (f : A → A') + {b : B' (f a)} {b₂ : B' (f a₂)} {b₃ : B' (f a₃)} (q : b =[ap f p] b₂) (q₂ : b₂ =[ap f p₂] b₃) : + pathover_of_pathover_ap B' f (change_path (ap_con f p p₂)⁻¹ (q ⬝o q₂)) = + pathover_of_pathover_ap B' f q ⬝o pathover_of_pathover_ap B' f q₂ := + by induction p; induction p₂; eapply idp_rec_on q; eapply idp_rec_on q₂; reflexivity + + definition pathover_ap_pathover_of_pathover_ap (P : A'' → Type) (g : A' → A'') (f : A → A') + {p : a = a₂} {b : P (g (f a))} {b₂ : P (g (f a₂))} (q : b =[ap f p] b₂) : + pathover_ap P (g ∘ f) (pathover_of_pathover_ap (P ∘ g) f q) = + change_path (ap_compose g f p)⁻¹ (pathover_ap P g q) := + by induction p; eapply (idp_rec_on q); reflexivity + + definition change_path_pathover_of_pathover_ap (B' : A' → Type) (f : A → A') {p p' : a = a₂} + (r : p = p') {b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[ap f p] b₂) : + change_path r (pathover_of_pathover_ap B' f q) = + pathover_of_pathover_ap B' f (change_path (ap02 f r) q) := + by induction r; reflexivity + + definition pathover_ap_change_path (B' : A' → Type) (f : A → A') {p p' : a = a₂} + (r : p = p') {b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[p] b₂) : + pathover_ap B' f (change_path r q) = change_path (ap02 f r) (pathover_ap B' f q) := + by induction r; reflexivity + + definition change_path_equiv [constructor] (b : B a) (b₂ : B a₂) (q : p = p') + : (b =[p] b₂) ≃ (b =[p'] b₂) := + begin + fapply equiv.MK, + { exact change_path q}, + { exact change_path q⁻¹}, + { intro r, induction q, reflexivity}, + { intro r, induction q, reflexivity}, + end + + definition apdo_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a₂) + : apdo g (ap f p) = pathover_ap B f (apdo (λx, g (f x)) p) := + by induction p; reflexivity + + definition apdo_eq_apdo_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a₂) + : apdo (λx, g (f x)) p = pathover_of_pathover_ap B f (apdo g (ap f p)) := + by induction p; reflexivity + + definition ap_compose_ap02_constant {A B C : Type} {a a' : A} (p : a = a') (b : B) (c : C) : + ap_compose (λc, b) (λa, c) p ⬝ ap02 (λc, b) (ap_constant p c) = ap_constant p b := + by induction p; reflexivity + + theorem apdo_constant (b : B'' a') (p : a = a) : + pathover_ap B'' (λa, a') (apdo (λa, b) p) = change_path (ap_constant p a')⁻¹ idpo := + begin + rewrite [apdo_eq_apdo_ap _ _ p], + let y := !change_path_of_pathover (apdo (apdo id) (ap_constant p b))⁻¹ᵒ, + rewrite -y, esimp, clear y, + refine !pathover_ap_pathover_of_pathover_ap ⬝ _, + rewrite pathover_ap_change_path, + rewrite -change_path_con, apply ap (λx, change_path x idpo), + unfold ap02, rewrite [ap_inv,-con_inv], apply inverse2, + apply ap_compose_ap02_constant + end + + definition apdo_change_path {B : A → Type} {a a₂ : A} (f : Πa, B a) {p p' : a = a₂} (s : p = p') + : apdo f p' = change_path s (apdo f p) := + by induction s; reflexivity + + definition cono_invo_eq_idpo {q q' : b =[p] b₂} (r : q = q') + : change_path (con.right_inv p) (q ⬝o q'⁻¹ᵒ) = idpo := + by induction r; induction q; reflexivity + end eq diff --git a/hott/cubical/square2.hlean b/hott/cubical/square2.hlean new file mode 100644 index 000000000..40a0c41b6 --- /dev/null +++ b/hott/cubical/square2.hlean @@ -0,0 +1,34 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Floris van Doorn + +Coherence conditions for operations on squares +-/ + +import .square + +namespace eq + + variables {A B C : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A} + {b : B} {c : C} + /-a₀₀-/ {p₁₀ p₁₀' : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/ + {p₀₁ p₀₁' : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ p₂₁' : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂} + /-a₀₂-/ {p₁₂ p₁₂' : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/ + {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄} + /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/ + + theorem whisker_bl_whisker_tl_eq (p : a = a') + : whisker_bl p (whisker_tl p ids) = con.right_inv p ⬝ph vrfl := + by induction p; reflexivity + + theorem ap_is_constant_natural_square {g : B → C} {f : A → B} (H : Πa, g (f a) = c) (p : a = a') : + (ap_is_constant H p)⁻¹ ⬝ph natural_square_tr H p ⬝hp ap_constant p c = + whisker_bl (H a') (whisker_tl (H a) ids) := + begin induction p, esimp, rewrite inv_inv, rewrite whisker_bl_whisker_tl_eq end + + definition inv_ph_eq_of_eq_ph {p : a₀₀ = a₀₂} {r : p₀₁ = p} {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} + {s₁₁' : square p₁₀ p₁₂ p p₂₁} (t : s₁₁ = r ⬝ph s₁₁') : r⁻¹ ⬝ph s₁₁ = s₁₁' := + by induction r; exact t + +end eq diff --git a/hott/cubical/squareover.hlean b/hott/cubical/squareover.hlean index 83215b4dd..b37c5065c 100644 --- a/hott/cubical/squareover.hlean +++ b/hott/cubical/squareover.hlean @@ -262,4 +262,19 @@ namespace eq induction p, esimp at s, apply pathover_idp_of_eq, apply eq_of_vdeg_squareover, exact s end + definition squareover_change_path_left {p₀₁' : a₀₀ = a₀₂} (r : p₀₁' = p₀₁) + {q₀₁ : b₀₀ =[p₀₁'] b₀₂} (t : squareover B (r ⬝ph s₁₁) q₁₀ q₁₂ q₀₁ q₂₁) + : squareover B s₁₁ q₁₀ q₁₂ (change_path r q₀₁) q₂₁ := + by induction r; exact t + + definition squareover_change_path_right {p₂₁' : a₂₀ = a₂₂} (r : p₂₁' = p₂₁) + {q₂₁ : b₂₀ =[p₂₁'] b₂₂} (t : squareover B (s₁₁ ⬝hp r⁻¹) q₁₀ q₁₂ q₀₁ q₂₁) + : squareover B s₁₁ q₁₀ q₁₂ q₀₁ (change_path r q₂₁) := + by induction r; exact t + + definition squareover_change_path_right' {p₂₁' : a₂₀ = a₂₂} (r : p₂₁ = p₂₁') + {q₂₁ : b₂₀ =[p₂₁'] b₂₂} (t : squareover B (s₁₁ ⬝hp r) q₁₀ q₁₂ q₀₁ q₂₁) + : squareover B s₁₁ q₁₀ q₁₂ q₀₁ (change_path r⁻¹ q₂₁) := + by induction r; exact t + end eq diff --git a/hott/eq2.hlean b/hott/eq2.hlean index 1942e40cc..493ab7d79 100644 --- a/hott/eq2.hlean +++ b/hott/eq2.hlean @@ -90,6 +90,10 @@ namespace eq (ap_compose g f q) := natural_square (ap_compose g f) r + theorem whisker_right_eq_of_con_inv_eq_idp {p q : a₁ = a₂} (r : p ⬝ q⁻¹ = idp) : + whisker_right (eq_of_con_inv_eq_idp r) q⁻¹ ⬝ con.right_inv q = r := + by induction q; esimp at r; cases r; reflexivity + theorem ap_eq_of_con_inv_eq_idp (f : A → B) {p q : a₁ = a₂} (r : p ⬝ q⁻¹ = idp) : ap02 f (eq_of_con_inv_eq_idp r) = eq_of_con_inv_eq_idp (whisker_left _ !ap_inv⁻¹ ⬝ !ap_con⁻¹ ⬝ ap02 f r) @@ -101,12 +105,6 @@ namespace eq : eq_of_con_inv_eq_idp (r ◾ inverse2 s ⬝ t) = r ⬝ eq_of_con_inv_eq_idp t ⬝ s⁻¹ := by induction s;induction r;induction q;reflexivity --- definition naturality_apdo {A : Type} {B : A → Type} {a a₂ : A} {f g : Πa, B a} --- (H : f ~ g) (p : a = a₂) --- : squareover B vrfl (apdo f p) (apdo g p) --- (pathover_idp_of_eq (H a)) (pathover_idp_of_eq (H a₂)) := --- by induction p;esimp;exact hrflo - definition naturality_apdo_eq {A : Type} {B : A → Type} {a a₂ : A} {f g : Πa, B a} (H : f ~ g) (p : a = a₂) : apdo f p = concato_eq (eq_concato (H a) (apdo g p)) (H a₂)⁻¹ := diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean index 7463a5f70..d8fa7d12e 100644 --- a/hott/hit/two_quotient.hlean +++ b/hott/hit/two_quotient.hlean @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -/ -import homotopy.circle eq2 algebra.e_closure cubical.cube +import homotopy.circle eq2 algebra.e_closure cubical.squareover cubical.cube cubical.square2 -open quotient eq circle sum sigma equiv function relation +open quotient eq circle sum sigma equiv function relation e_closure /- This files defines a general class of nonrecursive HITs using just quotients. @@ -21,7 +21,7 @@ open quotient eq circle sum sigma equiv function relation where p, p' are of the form - refl (f a), for some a : A; - e r, for some r : R a a'; - - ap f q, where q : a = a'; + - ap f q, where q : a = a' :> A; - inverses of such paths; - concatenations of such paths. @@ -92,9 +92,15 @@ namespace simple_two_quotient : ap (pre_elim Pj Pa Pe) (et t) = e_closure.elim Pe t := ap_e_closure_elim_h e (elim_e Pj Pa Pe) t + protected definition rec_et {P : C → Type} + (Pj : Πa, P (j a)) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), P (pre_aux q)) + (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a =[e s] Pj a') ⦃a a' : A⦄ (t : T a a') + : apdo (pre_rec Pj Pa Pe) (et t) = e_closure.elimo e Pe t := + ap_e_closure_elimo_h e Pe (rec_e Pj Pa Pe) t + inductive simple_two_quotient_rel : C → C → Type := | Rmk {} : Π{a : A} {r : T a a} (q : Q r) (x : circle), - simple_two_quotient_rel (f q x) (pre_aux q) + simple_two_quotient_rel (f q x) (pre_aux q) open simple_two_quotient_rel definition simple_two_quotient := quotient simple_two_quotient_rel @@ -104,6 +110,7 @@ namespace simple_two_quotient protected definition aux (q : Q r) : D := i (pre_aux q) definition incl1 (s : R a a') : incl0 a = incl0 a' := ap i (e s) definition inclt (t : T a a') : incl0 a = incl0 a' := e_closure.elim incl1 t + -- "wrong" version inclt, which is ap i (p ⬝ q) instead of ap i p ⬝ ap i q -- it is used in the proof, because incltw is easier to work with protected definition incltw (t : T a a') : incl0 a = incl0 a' := ap i (et t) @@ -125,6 +132,75 @@ namespace simple_two_quotient local attribute simple_two_quotient f i D incl0 aux incl1 incl2' inclt [reducible] local attribute i aux incl0 [constructor] + + protected definition rec {P : D → Type} (P0 : Π(a : A), P (incl0 a)) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') + (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), + change_path (incl2 q) (e_closure.elimo incl1 P1 r) = idpo) (x : D) : P x := + begin + induction x, + { refine (pre_rec _ _ _ a), + { exact P0}, + { intro a r q, exact incl2' q base ▸ P0 a}, + { intro a a' s, exact pathover_of_pathover_ap P i (P1 s)}}, + { exact abstract [irreducible] begin induction H, induction x, + { esimp, exact pathover_tr (incl2' q base) (P0 a)}, + { apply pathover_pathover, + esimp, fold [i, incl2' q], + refine eq_hconcato _ _, apply _, + { transitivity _, + { apply ap (pathover_ap _ _), + transitivity _, apply apdo_compose2 (pre_rec P0 _ _) (f q) loop, + apply ap (pathover_of_pathover_ap _ _), + transitivity _, apply apdo_change_path, exact !elim_loop⁻¹, + transitivity _, + apply ap (change_path _), + transitivity _, apply rec_et, + transitivity (pathover_of_pathover_ap P i (change_path (inclt_eq_incltw r) + (e_closure.elimo incl1 (λ (a a' : A) (s : R a a'), P1 s) r))), + apply e_closure_elimo_ap, + exact idp, + apply change_path_pathover_of_pathover_ap}, + esimp, transitivity _, apply pathover_ap_pathover_of_pathover_ap P i (f q), + transitivity _, apply ap (change_path _), apply to_right_inv !pathover_compose, + do 2 (transitivity _; exact !change_path_con⁻¹), + transitivity _, apply ap (change_path _), + exact (to_left_inv (change_path_equiv _ _ (incl2 q)) _)⁻¹, esimp, + rewrite P2, transitivity _; exact !change_path_con⁻¹, apply ap (λx, change_path x _), + rewrite [↑incl2, con_inv], transitivity _, exact !con.assoc⁻¹, + rewrite [inv_con_cancel_right, ↑incl2w, ↑ap02, +con_inv, +ap_inv, +inv_inv, -+con.assoc, + +con_inv_cancel_right], reflexivity}, + rewrite [change_path_con, apdo_constant], + apply squareover_change_path_left, apply squareover_change_path_right', + apply squareover_change_path_left, + refine change_square _ vrflo, + symmetry, apply inv_ph_eq_of_eq_ph, rewrite [ap_is_constant_natural_square], + apply whisker_bl_whisker_tl_eq} end end}, + end + + protected definition rec_on [reducible] {P : D → Type} (x : D) (P0 : Π(a : A), P (incl0 a)) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') + (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), + change_path (incl2 q) (e_closure.elimo incl1 P1 r) = idpo) : P x := + rec P0 P1 P2 x + + theorem rec_incl1 {P : D → Type} (P0 : Π(a : A), P (incl0 a)) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') + (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), + change_path (incl2 q) (e_closure.elimo incl1 P1 r) = idpo) ⦃a a' : A⦄ (s : R a a') + : apdo (rec P0 P1 P2) (incl1 s) = P1 s := + begin + unfold [rec, incl1], refine !apdo_ap ⬝ _, esimp, rewrite rec_e, + apply to_right_inv !pathover_compose + end + + theorem rec_inclt {P : D → Type} (P0 : Π(a : A), P (incl0 a)) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') + (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), + change_path (incl2 q) (e_closure.elimo incl1 P1 r) = idpo) ⦃a a' : A⦄ (t : T a a') + : apdo (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t := + ap_e_closure_elimo_h incl1 P1 (rec_incl1 P0 P1 P2) t + protected definition elim {P : Type} (P0 : A → P) (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp) @@ -142,8 +218,7 @@ namespace simple_two_quotient ap _ !elim_loop ⬝ !elim_et ⬝ P2 q ⬝ - !ap_constant⁻¹ end -} end end}, + !ap_constant⁻¹ end} end end}, end local attribute elim [unfold 8] @@ -194,7 +269,6 @@ namespace simple_two_quotient ⦃a : A⦄ ⦃r : T a a⦄ (q : Q r) : ap (elim P0 P1 P2) (incl2' q base) = idpath (P0 a) := !elim_eq_of_rel - -- set_option pp.implicit true protected theorem elim_incl2w {P : Type} (P0 : A → P) (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp) @@ -257,14 +331,14 @@ namespace simple_two_quotient end end simple_two_quotient ---attribute simple_two_quotient.j [constructor] --TODO -attribute /-simple_two_quotient.rec-/ simple_two_quotient.elim [unfold 8] [recursor 8] ---attribute simple_two_quotient.elim_type [unfold 9] -attribute /-simple_two_quotient.rec_on-/ simple_two_quotient.elim_on [unfold 5] ---attribute simple_two_quotient.elim_type_on [unfold 6] +attribute simple_two_quotient.j [constructor] +attribute simple_two_quotient.rec simple_two_quotient.elim [unfold 8] [recursor 8] +--attribute simple_two_quotient.elim_type [unfold 9] -- TODO +attribute simple_two_quotient.rec_on simple_two_quotient.elim_on [unfold 5] +--attribute simple_two_quotient.elim_type_on [unfold 6] -- TODO namespace two_quotient - open e_closure simple_two_quotient + open simple_two_quotient section parameters {A : Type} (R : A → A → Type) @@ -272,7 +346,6 @@ namespace two_quotient parameter (Q : Π⦃a a'⦄, T a a' → T a a' → Type) variables ⦃a a' : A⦄ {s : R a a'} {t t' : T a a'} - inductive two_quotient_Q : Π⦃a : A⦄, e_closure R a a → Type := | Qmk : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄, Q t t' → two_quotient_Q (t ⬝r t'⁻¹ʳ) open two_quotient_Q @@ -285,6 +358,46 @@ namespace two_quotient definition incl2 (q : Q t t') : inclt t = inclt t' := eq_of_con_inv_eq_idp (incl2 _ _ (Qmk R q)) + protected definition rec {P : two_quotient → Type} (P0 : Π(a : A), P (incl0 a)) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), + change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t') + (x : two_quotient) : P x := + begin + induction x, + { exact P0 a}, + { exact P1 s}, + { induction q with a a' t t' q, + rewrite [elimo_con (simple_two_quotient.incl1 R Q2) P1, + elimo_inv (simple_two_quotient.incl1 R Q2) P1, + -whisker_right_eq_of_con_inv_eq_idp (simple_two_quotient.incl2 R Q2 (Qmk R q)), + change_path_con], + xrewrite [change_path_cono], + refine ap (λx, change_path _ (_ ⬝o x)) !change_path_invo ⬝ _, esimp, + apply cono_invo_eq_idpo, apply P2} + end + + protected definition rec_on [reducible] {P : two_quotient → Type} (x : two_quotient) + (P0 : Π(a : A), P (incl0 a)) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), + change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t') : P x := + rec P0 P1 P2 x + + theorem rec_incl1 {P : two_quotient → Type} (P0 : Π(a : A), P (incl0 a)) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), + change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t') + ⦃a a' : A⦄ (s : R a a') : apdo (rec P0 P1 P2) (incl1 s) = P1 s := + rec_incl1 _ _ _ _ _ s + + theorem rec_inclt {P : two_quotient → Type} (P0 : Π(a : A), P (incl0 a)) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), + change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t') + ⦃a a' : A⦄ (t : T a a') : apdo (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t := + rec_inclt _ _ _ _ _ t + protected definition elim {P : Type} (P0 : A → P) (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t') @@ -294,7 +407,7 @@ namespace two_quotient { exact P0 a}, { exact P1 s}, { exact abstract [unfold 10] begin induction q with a a' t t' q, - rewrite [↑e_closure.elim], + esimp [e_closure.elim], apply con_inv_eq_idp, exact P2 q end end}, end local attribute elim [unfold 8] @@ -315,7 +428,7 @@ namespace two_quotient {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'} (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t') ⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (inclt t) = e_closure.elim P1 t := - !elim_inclt --ap_e_closure_elim_h incl1 (elim_incl1 P2) t + !elim_inclt theorem elim_incl2 {P : Type} (P0 : A → P) (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') @@ -325,7 +438,6 @@ namespace two_quotient begin rewrite [↑[incl2,elim],ap_eq_of_con_inv_eq_idp], xrewrite [eq_top_of_square (elim_incl2 R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2) (Qmk R q))], --- esimp, --doesn't fold elim_inclt back. The following tactic is just a "custom esimp" xrewrite [{simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2) (t ⬝r t'⁻¹ʳ)} idpath (ap_con (simple_two_quotient.elim R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2)) @@ -344,8 +456,8 @@ namespace two_quotient end end two_quotient ---attribute two_quotient.j [constructor] --TODO -attribute /-two_quotient.rec-/ two_quotient.elim [unfold 8] [recursor 8] +attribute two_quotient.incl0 [constructor] +attribute two_quotient.rec two_quotient.elim [unfold 8] [recursor 8] --attribute two_quotient.elim_type [unfold 9] -attribute /-two_quotient.rec_on-/ two_quotient.elim_on [unfold 5] +attribute two_quotient.rec_on two_quotient.elim_on [unfold 5] --attribute two_quotient.elim_type_on [unfold 6] diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index 4a554ae34..fc24d191b 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -293,11 +293,8 @@ namespace eq : eq_concato q⁻¹ (pathover_idp_of_eq q) = (idpo : b' =[refl a] b') := by induction q;constructor - definition change_path_equiv (f : Π{a}, B a ≃ B' a) (r : b =[p] b₂) : f b =[p] f b₂ := - by induction r;constructor - - definition change_path_equiv' (f : Π{a}, B a ≃ B' a) (r : f b =[p] f b₂) : b =[p] b₂ := - (left_inv f b)⁻¹ ⬝po change_path_equiv (λa, f⁻¹ᵉ) r ⬝op left_inv f b₂ + definition pathover_of_fn_pathover_fn (f : Π{a}, B a ≃ B' a) (r : f b =[p] f b₂) : b =[p] b₂ := + (left_inv f b)⁻¹ ⬝po apo (λa, f⁻¹ᵉ) r ⬝op left_inv f b₂ definition change_path_of_pathover (s : p = p') (r : b =[p] b₂) (r' : b =[p'] b₂) (q : r =[s] r') : change_path s r = r' := diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 03b3bb383..c9ca55f39 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -175,7 +175,7 @@ namespace equiv {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a') (r : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[p] g b') : f =[p] g := begin - fapply change_path_equiv', + fapply pathover_of_fn_pathover_fn, { intro a, apply equiv.sigma_char}, { fapply sigma_pathover, esimp, apply arrow_pathover, exact r,