feat(hit/two_quotient): give dependent eliminator for two_quotients
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
8632b7ae27
commit
ae92e8c94d
9 changed files with 336 additions and 67 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
* [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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
34
hott/cubical/square2.hlean
Normal file
34
hott/cubical/square2.hlean
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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₂)⁻¹ :=
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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' :=
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
Loading…
Reference in a new issue