feat(hit): add hits with 2-path constructors
In hit.two_quotient we define a general construction to define hits with 2-dimensional path constructors, similar to quotients. We can add 2-paths between any two 'words', where a word consists of 1-path constructors, concatenation and inverses. We use this to define the torus, reflexive quotients and the reduced suspension. There is still one 'sorry' in the construction
This commit is contained in:
Floris van Doorn
parent
df3ce2b00b
commit
24762fe843
4 changed files with 590 additions and 0 deletions
87
hott/hit/red_susp.hlean
Normal file
87
hott/hit/red_susp.hlean
Normal file
|
|
@ -0,0 +1,87 @@
|
|||
/-
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Floris van Doorn
|
||||
|
||||
Declaration of the reduced suspension
|
||||
-/
|
||||
|
||||
import .two_quotient types.pointed algebra.e_closure
|
||||
|
||||
open simple_two_quotient eq unit pointed e_closure
|
||||
|
||||
namespace red_susp
|
||||
section
|
||||
|
||||
parameter {A : Pointed}
|
||||
|
||||
inductive red_susp_R : unit → unit → Type :=
|
||||
| Rmk : Π(a : A), red_susp_R star star
|
||||
open red_susp_R
|
||||
inductive red_susp_Q : Π⦃x : unit⦄, e_closure red_susp_R x x → Type :=
|
||||
| Qmk : red_susp_Q [Rmk pt]
|
||||
open red_susp_Q
|
||||
local abbreviation R := red_susp_R
|
||||
local abbreviation Q := red_susp_Q
|
||||
|
||||
definition red_susp : Type := simple_two_quotient R Q -- TODO: define this in root namespace
|
||||
|
||||
definition base : red_susp :=
|
||||
incl0 R Q star
|
||||
|
||||
definition merid (a : A) : base = base :=
|
||||
incl1 R Q (Rmk a)
|
||||
|
||||
definition merid_pt : merid pt = idp :=
|
||||
incl2 R Q Qmk
|
||||
|
||||
-- protected definition rec {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
|
||||
-- (Pe : Pm pt =[merid_pt] idpo) (x : red_susp) : P x :=
|
||||
-- begin
|
||||
-- induction x,
|
||||
-- end
|
||||
|
||||
-- protected definition rec_on [reducible] {P : red_susp → Type} (x : red_susp) (Pb : P base)
|
||||
-- (Pm : Π(a : A), Pb =[merid a] Pb) (Pe : Pm pt =[merid_pt] idpo) : P x :=
|
||||
-- rec Pb Pm Pe x
|
||||
|
||||
-- definition rec_merid {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
|
||||
-- (Pe : Pm pt =[merid_pt] idpo) (a : A)
|
||||
-- : apdo (rec Pb Pm Pe) (merid a) = Pm a :=
|
||||
-- !rec_incl1
|
||||
|
||||
-- theorem elim_merid_pt {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
|
||||
-- (Pe : Pm pt =[merid_pt] idpo)
|
||||
-- : square (ap02 (rec Pb Pm Pe) merid_pt) Pe (rec_merid Pe pt) idp :=
|
||||
-- !rec_incl2
|
||||
|
||||
protected definition elim {P : Type} (Pb : P) (Pm : Π(a : A), Pb = Pb)
|
||||
(Pe : Pm pt = idp) (x : red_susp) : P :=
|
||||
begin
|
||||
induction x,
|
||||
exact Pb,
|
||||
induction s, exact Pm a,
|
||||
induction q, exact Pe
|
||||
end
|
||||
|
||||
protected definition elim_on [reducible] {P : Type} (x : red_susp) (Pb : P)
|
||||
(Pm : Π(a : A), Pb = Pb) (Pe : Pm pt = idp) : P :=
|
||||
elim Pb Pm Pe x
|
||||
|
||||
definition elim_merid {P : Type} {Pb : P} {Pm : Π(a : A), Pb = Pb}
|
||||
(Pe : Pm pt = idp) (a : A)
|
||||
: ap (elim Pb Pm Pe) (merid a) = Pm a :=
|
||||
!elim_incl1
|
||||
|
||||
theorem elim_merid_pt {P : Type} (Pb : P) (Pm : Π(a : A), Pb = Pb)
|
||||
(Pe : Pm pt = idp) : square (ap02 (elim Pb Pm Pe) merid_pt) Pe (elim_merid Pe pt) idp :=
|
||||
!elim_incl2
|
||||
|
||||
end
|
||||
end red_susp
|
||||
|
||||
attribute red_susp.base [constructor]
|
||||
attribute /-red_susp.rec-/ red_susp.elim [unfold-c 6] [recursor 6]
|
||||
--attribute red_susp.elim_type [unfold-c 9]
|
||||
attribute /-red_susp.rec_on-/ red_susp.elim_on [unfold-c 3]
|
||||
--attribute red_susp.elim_type_on [unfold-c 6]
|
||||
90
hott/hit/refl_quotient.hlean
Normal file
90
hott/hit/refl_quotient.hlean
Normal file
|
|
@ -0,0 +1,90 @@
|
|||
/-
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Authors: Floris van Doorn
|
||||
|
||||
Quotient of a reflexive relation
|
||||
-/
|
||||
|
||||
import hit.circle types.cubical.squareover .two_quotient
|
||||
|
||||
open eq simple_two_quotient e_closure
|
||||
|
||||
namespace refl_quotient
|
||||
section
|
||||
|
||||
parameters {A : Type} (R : A → A → Type) (ρ : Πa, R a a)
|
||||
inductive refl_quotient_Q : Π⦃a : A⦄, e_closure R a a → Type :=
|
||||
| Qmk {} : Π(a : A), refl_quotient_Q [ρ a]
|
||||
open refl_quotient_Q
|
||||
local abbreviation Q := refl_quotient_Q
|
||||
|
||||
definition refl_quotient : Type := simple_two_quotient R Q -- TODO: define this in root namespace
|
||||
|
||||
definition rclass_of (a : A) : refl_quotient := incl0 R Q a
|
||||
definition req_of_rel ⦃a a' : A⦄ (r : R a a') : rclass_of a = rclass_of a' :=
|
||||
incl1 R Q r
|
||||
|
||||
definition pρ (a : A) : req_of_rel (ρ a) = idp :=
|
||||
incl2 R Q (Qmk a)
|
||||
|
||||
-- protected definition rec {P : refl_quotient → Type}
|
||||
-- (Pc : Π(a : A), P (rclass_of a))
|
||||
-- (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
|
||||
-- (Pr : Π(a : A), Pp (ρ a) =[pρ a] idpo)
|
||||
-- (x : refl_quotient) : P x :=
|
||||
-- sorry
|
||||
|
||||
-- protected definition rec_on [reducible] {P : refl_quotient → Type}
|
||||
-- (Pc : Π(a : A), P (rclass_of a))
|
||||
-- (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
|
||||
-- (Pr : Π(a : A), Pp (ρ a) =[pρ a] idpo) : P y :=
|
||||
-- rec Pinl Pinr Pglue y
|
||||
|
||||
-- definition rec_req_of_rel {P : Type} {P : refl_quotient → Type}
|
||||
-- (Pc : Π(a : A), P (rclass_of a))
|
||||
-- (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
|
||||
-- (Pr : Π(a : A), Pp (ρ a) =[pρ a] idpo)
|
||||
-- ⦃a a' : A⦄ (r : R a a') : apdo (rec Pc Pp Pr) (req_of_rel r) = Pp r :=
|
||||
-- !rec_incl1
|
||||
|
||||
-- theorem rec_pρ {P : Type} {P : refl_quotient → Type}
|
||||
-- (Pc : Π(a : A), P (rclass_of a))
|
||||
-- (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
|
||||
-- (Pr : Π(a : A), Pp (ρ a) =[pρ a] idpo) (a : A)
|
||||
-- : square (ap02 (rec Pc Pp Pr) (pρ a)) (Pr a) (elim_req_of_rel Pr (ρ a)) idp :=
|
||||
-- !rec_incl2
|
||||
|
||||
protected definition elim {P : Type} (Pc : Π(a : A), P)
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (Pr : Π(a : A), Pp (ρ a) = idp)
|
||||
(x : refl_quotient) : P :=
|
||||
begin
|
||||
induction x,
|
||||
exact Pc a,
|
||||
exact Pp s,
|
||||
induction q, apply Pr
|
||||
end
|
||||
|
||||
protected definition elim_on [reducible] {P : Type} (x : refl_quotient) (Pc : Π(a : A), P)
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (Pr : Π(a : A), Pp (ρ a) = idp) : P :=
|
||||
elim Pc Pp Pr x
|
||||
|
||||
definition elim_req_of_rel {P : Type} {Pc : Π(a : A), P}
|
||||
{Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a'} (Pr : Π(a : A), Pp (ρ a) = idp)
|
||||
⦃a a' : A⦄ (r : R a a') : ap (elim Pc Pp Pr) (req_of_rel r) = Pp r :=
|
||||
!elim_incl1
|
||||
|
||||
theorem elim_pρ {P : Type} (Pc : Π(a : A), P)
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (Pr : Π(a : A), Pp (ρ a) = idp) (a : A)
|
||||
: square (ap02 (elim Pc Pp Pr) (pρ a)) (Pr a) (elim_req_of_rel Pr (ρ a)) idp :=
|
||||
!elim_incl2
|
||||
|
||||
end
|
||||
end refl_quotient
|
||||
|
||||
attribute refl_quotient.rclass_of [constructor]
|
||||
attribute /-refl_quotient.rec-/ refl_quotient.elim [unfold-c 8] [recursor 8]
|
||||
--attribute refl_quotient.elim_type [unfold-c 9]
|
||||
attribute /-refl_quotient.rec_on-/ refl_quotient.elim_on [unfold-c 5]
|
||||
--attribute refl_quotient.elim_type_on [unfold-c 6]
|
||||
93
hott/hit/torus.hlean
Normal file
93
hott/hit/torus.hlean
Normal file
|
|
@ -0,0 +1,93 @@
|
|||
/-
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Authors: Floris van Doorn
|
||||
|
||||
Declaration of the torus
|
||||
-/
|
||||
|
||||
import .two_quotient
|
||||
|
||||
open two_quotient eq bool unit relation
|
||||
|
||||
namespace torus
|
||||
|
||||
definition torus_R (x y : unit) := bool
|
||||
local infix `⬝r`:75 := @e_closure.trans unit torus_R star star star
|
||||
local postfix `⁻¹ʳ`:(max+10) := @e_closure.symm unit torus_R star star
|
||||
local notation `[`:max a `]`:0 := @e_closure.of_rel unit torus_R star star a
|
||||
|
||||
inductive torus_Q : Π⦃x y : unit⦄, e_closure torus_R x y → e_closure torus_R x y → Type :=
|
||||
| Qmk : torus_Q ([ff] ⬝r [tt]) ([tt] ⬝r [ff])
|
||||
|
||||
definition torus := two_quotient torus_R torus_Q
|
||||
definition base : torus := incl0 _ _ star
|
||||
definition loop1 : base = base := incl1 _ _ ff
|
||||
definition loop2 : base = base := incl1 _ _ tt
|
||||
definition surf : loop1 ⬝ loop2 = loop2 ⬝ loop1 :=
|
||||
incl2 _ _ torus_Q.Qmk
|
||||
|
||||
-- protected definition rec {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
|
||||
-- (Pl2 : Pb =[loop2] Pb) (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2)
|
||||
-- (x : torus) : P x :=
|
||||
-- sorry
|
||||
|
||||
-- example {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb) (Pl2 : Pb =[loop2] Pb)
|
||||
-- (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2) : torus.rec Pb Pl1 Pl2 Pf base = Pb := idp
|
||||
|
||||
-- definition rec_loop1 {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
|
||||
-- (Pl2 : Pb =[loop2] Pb) (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2)
|
||||
-- : apdo (torus.rec Pb Pl1 Pl2 Pf) loop1 = Pl1 :=
|
||||
-- sorry
|
||||
|
||||
-- definition rec_loop2 {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
|
||||
-- (Pl2 : Pb =[loop2] Pb) (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2)
|
||||
-- : apdo (torus.rec Pb Pl1 Pl2 Pf) loop2 = Pl2 :=
|
||||
-- sorry
|
||||
|
||||
-- definition rec_surf {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
|
||||
-- (Pl2 : Pb =[loop2] Pb) (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2)
|
||||
-- : cubeover P rfl1 (apds (torus.rec Pb Pl1 Pl2 Pf) fill) Pf
|
||||
-- (vdeg_squareover !rec_loop2) (vdeg_squareover !rec_loop2)
|
||||
-- (vdeg_squareover !rec_loop1) (vdeg_squareover !rec_loop1) :=
|
||||
-- sorry
|
||||
|
||||
protected definition elim {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
|
||||
(Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) (x : torus) : P :=
|
||||
begin
|
||||
induction x,
|
||||
{ exact Pb},
|
||||
{ induction s,
|
||||
{ exact Pl1},
|
||||
{ exact Pl2}},
|
||||
{ induction q, exact Ps},
|
||||
end
|
||||
|
||||
protected definition elim_on [reducible] {P : Type} (x : torus) (Pb : P)
|
||||
(Pl1 : Pb = Pb) (Pl2 : Pb = Pb) (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : P :=
|
||||
torus.elim Pb Pl1 Pl2 Ps x
|
||||
|
||||
definition elim_loop1 {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
|
||||
(Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : ap (torus.elim Pb Pl1 Pl2 Ps) loop1 = Pl1 :=
|
||||
!elim_incl1
|
||||
|
||||
definition elim_loop2 {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
|
||||
(Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : ap (torus.elim Pb Pl1 Pl2 Ps) loop2 = Pl2 :=
|
||||
!elim_incl1
|
||||
|
||||
definition elim_surf {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
|
||||
(Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1)
|
||||
: square (ap02 (torus.elim Pb Pl1 Pl2 Ps) surf)
|
||||
Ps
|
||||
(!ap_con ⬝ (!elim_loop1 ◾ !elim_loop2))
|
||||
(!ap_con ⬝ (!elim_loop2 ◾ !elim_loop1)) :=
|
||||
!elim_incl2
|
||||
|
||||
end torus
|
||||
|
||||
attribute torus.base [constructor]
|
||||
attribute /-torus.rec-/ torus.elim [unfold-c 6] [recursor 6]
|
||||
--attribute torus.elim_type [unfold-c 9]
|
||||
attribute /-torus.rec_on-/ torus.elim_on [unfold-c 2]
|
||||
--attribute torus.elim_type_on [unfold-c 6]
|
||||
320
hott/hit/two_quotient.hlean
Normal file
320
hott/hit/two_quotient.hlean
Normal file
|
|
@ -0,0 +1,320 @@
|
|||
/-
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Authors: Floris van Doorn
|
||||
-/
|
||||
|
||||
import hit.circle types.eq2 algebra.e_closure
|
||||
|
||||
open quotient eq circle sum sigma equiv function relation
|
||||
|
||||
namespace simple_two_quotient
|
||||
|
||||
section
|
||||
parameters {A : Type}
|
||||
(R : A → A → Type)
|
||||
local abbreviation T := e_closure R -- the (type-valued) equivalence closure of R
|
||||
parameter (Q : Π⦃a⦄, T a a → Type)
|
||||
variables ⦃a a' : A⦄ {s : R a a'} {r : T a a}
|
||||
|
||||
|
||||
local abbreviation B := A ⊎ Σ(a : A) (r : T a a), Q r
|
||||
|
||||
inductive pre_simple_two_quotient_rel : B → B → Type :=
|
||||
| pre_Rmk {} : Π⦃a a'⦄ (r : R a a'), pre_simple_two_quotient_rel (inl a) (inl a')
|
||||
--BUG: if {} not provided, the alias for pre_Rmk is wrong
|
||||
|
||||
definition pre_simple_two_quotient := quotient pre_simple_two_quotient_rel
|
||||
|
||||
open pre_simple_two_quotient_rel
|
||||
local abbreviation C := quotient pre_simple_two_quotient_rel
|
||||
protected definition j [constructor] (a : A) : C := class_of pre_simple_two_quotient_rel (inl a)
|
||||
protected definition pre_aux [constructor] (q : Q r) : C :=
|
||||
class_of pre_simple_two_quotient_rel (inr ⟨a, r, q⟩)
|
||||
protected definition e (s : R a a') : j a = j a' := eq_of_rel _ (pre_Rmk s)
|
||||
protected definition et (t : T a a') : j a = j a' := e_closure.elim e t
|
||||
protected definition f [unfold-c 7] (q : Q r) : S¹ → C :=
|
||||
circle.elim (j a) (et r)
|
||||
|
||||
protected definition pre_rec [unfold-c 8] {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') (x : C) : P x :=
|
||||
begin
|
||||
induction x with p,
|
||||
{ induction p,
|
||||
{ apply Pj},
|
||||
{ induction a with a1 a2, induction a2, apply Pa}},
|
||||
{ induction H, esimp, apply Pe},
|
||||
end
|
||||
|
||||
protected definition pre_elim [unfold-c 8] {P : Type} (Pj : A → P)
|
||||
(Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P) (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a = Pj a') (x : C)
|
||||
: P :=
|
||||
pre_rec Pj Pa (λa a' s, pathover_of_eq (Pe s)) x
|
||||
|
||||
protected theorem rec_e {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⦄ (s : R a a')
|
||||
: apdo (pre_rec Pj Pa Pe) (e s) = Pe s :=
|
||||
!rec_eq_of_rel
|
||||
|
||||
protected theorem elim_e {P : Type} (Pj : A → P) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P)
|
||||
(Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a = Pj a') ⦃a a' : A⦄ (s : R a a')
|
||||
: ap (pre_elim Pj Pa Pe) (e s) = Pe s :=
|
||||
begin
|
||||
apply eq_of_fn_eq_fn_inv !(pathover_constant (e s)),
|
||||
rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑pre_elim,rec_e],
|
||||
end
|
||||
|
||||
protected definition elim_et {P : Type} (Pj : A → P) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P)
|
||||
(Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a = Pj a') ⦃a a' : A⦄ (t : T a a')
|
||||
: 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
|
||||
|
||||
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)
|
||||
|
||||
open simple_two_quotient_rel
|
||||
definition simple_two_quotient := quotient simple_two_quotient_rel
|
||||
local abbreviation D := simple_two_quotient
|
||||
local abbreviation i := class_of simple_two_quotient_rel
|
||||
definition incl0 (a : A) : D := i (j a)
|
||||
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 inclt is easier to work with
|
||||
protected definition incltw (t : T a a') : incl0 a = incl0 a' := ap i (et t)
|
||||
|
||||
protected definition inclt_eq_incltw (t : T a a') : inclt t = incltw t :=
|
||||
(ap_e_closure_elim i e t)⁻¹
|
||||
|
||||
definition incl2' (q : Q r) (x : S¹) : i (f q x) = aux q :=
|
||||
eq_of_rel simple_two_quotient_rel (Rmk q x)
|
||||
|
||||
protected definition incl2w (q : Q r) : incltw r = idp :=
|
||||
(ap02 i (elim_loop (j a) (et r))⁻¹) ⬝
|
||||
(ap_compose i (f q) loop)⁻¹ ⬝
|
||||
ap_weakly_constant (incl2' q) loop ⬝
|
||||
!con.right_inv
|
||||
|
||||
definition incl2 (q : Q r) : inclt r = idp :=
|
||||
inclt_eq_incltw r ⬝ incl2w q
|
||||
|
||||
local attribute simple_two_quotient f i incl0 aux incl1 incl2' inclt [reducible]
|
||||
local attribute i aux incl0 [constructor]
|
||||
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)
|
||||
(x : D) : P :=
|
||||
begin
|
||||
induction x,
|
||||
{ refine (pre_elim _ _ _ a),
|
||||
{ exact P0},
|
||||
{ intro a r q, exact P0 a},
|
||||
{ exact P1}},
|
||||
{ exact abstract begin induction H, induction x,
|
||||
{ exact idpath (P0 a)},
|
||||
{ unfold f, apply pathover_eq, apply hdeg_square,
|
||||
exact abstract ap_compose (pre_elim P0 _ P1) (f q) loop ⬝
|
||||
ap _ !elim_loop ⬝
|
||||
!elim_et ⬝
|
||||
P2 q ⬝
|
||||
!ap_constant⁻¹ end
|
||||
} end end},
|
||||
end
|
||||
local attribute elim [unfold-c 8]
|
||||
|
||||
protected definition elim_on {P : Type} (x : D) (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)
|
||||
: P :=
|
||||
elim P0 P1 P2 x
|
||||
|
||||
definition elim_incl1 {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)
|
||||
⦃a a' : A⦄ (s : R a a') : ap (elim P0 P1 P2) (incl1 s) = P1 s :=
|
||||
(ap_compose (elim P0 P1 P2) i (e s))⁻¹ ⬝ !elim_e
|
||||
|
||||
definition elim_inclt {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)
|
||||
⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (inclt t) = e_closure.elim P1 t :=
|
||||
ap_e_closure_elim_h incl1 (elim_incl1 P2) t
|
||||
|
||||
protected definition elim_incltw {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)
|
||||
⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (incltw t) = e_closure.elim P1 t :=
|
||||
(ap_compose (elim P0 P1 P2) i (et t))⁻¹ ⬝ !elim_et
|
||||
|
||||
protected theorem elim_inclt_eq_elim_incltw {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)
|
||||
⦃a a' : A⦄ (t : T a a')
|
||||
: elim_inclt P2 t = ap (ap (elim P0 P1 P2)) (inclt_eq_incltw t) ⬝ elim_incltw P2 t :=
|
||||
begin
|
||||
unfold [elim_inclt,elim_incltw,inclt_eq_incltw,et],
|
||||
refine !ap_e_closure_elim_h_eq ⬝ _,
|
||||
rewrite [ap_inv,-con.assoc],
|
||||
xrewrite [eq_of_square (ap_ap_e_closure_elim i (elim P0 P1 P2) e t)⁻¹ʰ],
|
||||
rewrite [↓incl1,con.assoc], apply whisker_left,
|
||||
rewrite [↑[elim_et,elim_incl1],+ap_e_closure_elim_h_eq,con_inv,↑[i,function.compose]],
|
||||
rewrite [-con.assoc (_ ⬝ _),con.assoc _⁻¹,con.left_inv,▸*,-ap_inv,-ap_con],
|
||||
apply ap (ap _),
|
||||
krewrite [-eq_of_homotopy3_inv,-eq_of_homotopy3_con]
|
||||
end
|
||||
|
||||
definition elim_incl2'_incl0 {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)
|
||||
⦃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)
|
||||
⦃a : A⦄ ⦃r : T a a⦄ (q : Q r)
|
||||
: square (ap02 (elim P0 P1 P2) (incl2w q)) (P2 q) (elim_incltw P2 r) idp :=
|
||||
begin
|
||||
esimp [incl2w,ap02],
|
||||
rewrite [+ap_con (ap _),▸*],
|
||||
xrewrite [-ap_compose (ap _) (ap i)],
|
||||
rewrite [+ap_inv],
|
||||
xrewrite [eq_top_of_square
|
||||
((ap_compose_natural (elim P0 P1 P2) i (elim_loop (j a) (et r)))⁻¹ʰ⁻¹ᵛ ⬝h
|
||||
(ap_ap_compose (elim P0 P1 P2) i (f q) loop)⁻¹ʰ⁻¹ᵛ ⬝h
|
||||
ap_ap_weakly_constant (elim P0 P1 P2) (incl2' q) loop ⬝h
|
||||
ap_con_right_inv_sq (elim P0 P1 P2) (incl2' q base)),
|
||||
↑[elim_incltw]],
|
||||
apply whisker_tl,
|
||||
rewrite [ap_weakly_constant_eq],
|
||||
xrewrite [naturality_apdo_eq (λx, !elim_eq_of_rel) loop],
|
||||
rewrite [↑elim_2,rec_loop,square_of_pathover_concato_eq,square_of_pathover_eq_concato,
|
||||
eq_of_square_vconcat_eq,eq_of_square_eq_vconcat],
|
||||
apply eq_vconcat,
|
||||
{ apply ap (λx, _ ⬝ eq_con_inv_of_con_eq ((_ ⬝ x ⬝ _)⁻¹ ⬝ _) ⬝ _),
|
||||
transitivity _, apply ap eq_of_square,
|
||||
apply to_right_inv !pathover_eq_equiv_square (hdeg_square (elim_1 P A R Q P0 P1 a r q P2)),
|
||||
transitivity _, apply eq_of_square_hdeg_square,
|
||||
unfold elim_1, reflexivity},
|
||||
rewrite [+con_inv,whisker_left_inv,+inv_inv,-whisker_right_inv,
|
||||
con.assoc (whisker_left _ _),con.assoc _ (whisker_right _ _),▸*,
|
||||
whisker_right_con_whisker_left _ !ap_constant],
|
||||
xrewrite [-con.assoc _ _ (whisker_right _ _)],
|
||||
rewrite [con.assoc _ _ (whisker_left _ _),idp_con_whisker_left,▸*,
|
||||
con.assoc _ !ap_constant⁻¹,con.left_inv],
|
||||
xrewrite [eq_con_inv_of_con_eq_whisker_left,▸*],
|
||||
rewrite [+con.assoc _ _ !con.right_inv,
|
||||
right_inv_eq_idp (
|
||||
(λ(x : ap (elim P0 P1 P2) (incl2' q base) = idpath
|
||||
(elim P0 P1 P2 (class_of simple_two_quotient_rel (f q base)))), x)
|
||||
(elim_incl2'_incl0 P2 q)),
|
||||
↑[whisker_left]],
|
||||
xrewrite [con2_con_con2],
|
||||
rewrite [idp_con,↑elim_incl2'_incl0,con.left_inv,whisker_right_inv,↑whisker_right],
|
||||
xrewrite [con.assoc _ _ (_ ◾ _)],
|
||||
rewrite [con.left_inv,▸*,-+con.assoc,con.assoc _⁻¹,↑[elim,function.compose],con.left_inv,
|
||||
▸*,↑j,con.left_inv,idp_con],
|
||||
apply square_of_eq, reflexivity
|
||||
end
|
||||
|
||||
theorem elim_incl2 {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)
|
||||
⦃a : A⦄ ⦃r : T a a⦄ (q : Q r)
|
||||
: square (ap02 (elim P0 P1 P2) (incl2 q)) (P2 q) (elim_inclt P2 r) idp :=
|
||||
begin
|
||||
rewrite [↑incl2,↑ap02,ap_con,elim_inclt_eq_elim_incltw],
|
||||
apply whisker_tl,
|
||||
apply elim_incl2w
|
||||
end
|
||||
|
||||
end
|
||||
end simple_two_quotient
|
||||
|
||||
--attribute simple_two_quotient.j [constructor] --TODO
|
||||
attribute /-simple_two_quotient.rec-/ simple_two_quotient.elim [unfold-c 8] [recursor 8]
|
||||
--attribute simple_two_quotient.elim_type [unfold-c 9]
|
||||
attribute /-simple_two_quotient.rec_on-/ simple_two_quotient.elim_on [unfold-c 5]
|
||||
--attribute simple_two_quotient.elim_type_on [unfold-c 6]
|
||||
|
||||
namespace two_quotient
|
||||
open e_closure simple_two_quotient
|
||||
section
|
||||
parameters {A : Type}
|
||||
(R : A → A → Type)
|
||||
local abbreviation T := e_closure R -- the (type-valued) equivalence closure of R
|
||||
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
|
||||
local abbreviation Q2 := two_quotient_Q
|
||||
|
||||
definition two_quotient := simple_two_quotient R Q2
|
||||
definition incl0 (a : A) : two_quotient := incl0 _ _ a
|
||||
definition incl1 (s : R a a') : incl0 a = incl0 a' := incl1 _ _ s
|
||||
definition inclt (t : T a a') : incl0 a = incl0 a' := e_closure.elim incl1 t
|
||||
definition incl2 (q : Q t t') : inclt t = inclt t' :=
|
||||
eq_of_con_inv_eq_idp (incl2 _ _ (Qmk R q))
|
||||
|
||||
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')
|
||||
(x : two_quotient) : P :=
|
||||
begin
|
||||
induction x,
|
||||
{ exact P0 a},
|
||||
{ exact P1 s},
|
||||
{ exact abstract [unfold-c 10] begin induction q with a a' t t' q,
|
||||
rewrite [↑e_closure.elim,↓e_closure.elim P1 t,↓e_closure.elim P1 t'],
|
||||
apply con_inv_eq_idp, exact P2 q end end},
|
||||
end
|
||||
local attribute elim [unfold-c 8]
|
||||
|
||||
protected definition elim_on {P : Type} (x : two_quotient) (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')
|
||||
: P :=
|
||||
elim P0 P1 P2 x
|
||||
|
||||
definition elim_incl1 {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')
|
||||
⦃a a' : A⦄ (s : R a a') : ap (elim P0 P1 P2) (incl1 s) = P1 s :=
|
||||
!elim_incl1
|
||||
|
||||
definition elim_inclt {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')
|
||||
⦃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
|
||||
|
||||
--print elim
|
||||
theorem elim_incl2 {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')
|
||||
⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t')
|
||||
: square (ap02 (elim P0 P1 P2) (incl2 q)) (P2 q) (elim_inclt P2 t) (elim_inclt P2 t') :=
|
||||
begin
|
||||
-- let H := elim_incl2 R Q2 P0 P1 (two_quotient_Q.rec (λ (a a' : A) (t t' : T a a') (q : Q t t'), con_inv_eq_idp (P2 q))) (Qmk R q),
|
||||
-- esimp at H,
|
||||
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)),▸*],
|
||||
exact sorry
|
||||
end
|
||||
|
||||
end
|
||||
end two_quotient
|
||||
|
||||
--attribute two_quotient.j [constructor] --TODO
|
||||
attribute /-two_quotient.rec-/ two_quotient.elim [unfold-c 8] [recursor 8]
|
||||
--attribute two_quotient.elim_type [unfold-c 9]
|
||||
attribute /-two_quotient.rec_on-/ two_quotient.elim_on [unfold-c 5]
|
||||
--attribute two_quotient.elim_type_on [unfold-c 6]
|
||||
Loading…
Reference in a new issue