feat(hit): prove path computation rules for all hits except the circle
This commit is contained in:
parent
70a2f6534c
commit
6c061991cc
8 changed files with 14 additions and 9 deletions
|
@ -42,7 +42,7 @@ namespace circle
|
|||
theorem rec2_seg1 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
|
||||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1)
|
||||
: apd (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
|
||||
sorry
|
||||
!rec_merid
|
||||
|
||||
theorem rec2_seg2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
|
||||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1)
|
||||
|
|
|
@ -47,7 +47,7 @@ parameters {A B : Type.{u}} (f g : A → B)
|
|||
theorem rec_cp {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x))
|
||||
(Pcp : Π(x : A), cp x ▹ P_i (f x) = P_i (g x))
|
||||
(x : A) : apd (rec P_i Pcp) (cp x) = Pcp x :=
|
||||
sorry
|
||||
!rec_eq_of_rel
|
||||
|
||||
protected definition elim {P : Type} (P_i : B → P)
|
||||
(Pcp : Π(x : A), P_i (f x) = P_i (g x)) (y : coeq) : P :=
|
||||
|
|
|
@ -53,7 +53,7 @@ section
|
|||
(Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
|
||||
(Pglue : Π(j : J) (x : A (dom j)), cglue j x ▹ Pincl (f j x) = Pincl x)
|
||||
{j : J} (x : A (dom j)) : apd (rec Pincl Pglue) (cglue j x) = Pglue j x :=
|
||||
sorry
|
||||
!rec_eq_of_rel
|
||||
|
||||
protected definition elim {P : Type} (Pincl : Π⦃i : I⦄ (x : A i), P)
|
||||
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) (y : colimit) : P :=
|
||||
|
@ -93,6 +93,10 @@ end colimit
|
|||
/- definition of a sequential colimit -/
|
||||
namespace seq_colim
|
||||
section
|
||||
/-
|
||||
we define it directly in terms of type quotients. An alternative definition could be
|
||||
definition seq_colim := colimit.colimit A function.id succ f
|
||||
-/
|
||||
parameters {A : ℕ → Type} (f : Π⦃n⦄, A n → A (succ n))
|
||||
variables {n : ℕ} (a : A n)
|
||||
|
||||
|
@ -132,7 +136,7 @@ section
|
|||
theorem rec_glue {P : seq_colim → Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
|
||||
(Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▹ Pincl (f a) = Pincl a) {n : ℕ} (a : A n)
|
||||
: apd (rec Pincl Pglue) (glue a) = Pglue a :=
|
||||
sorry
|
||||
!rec_eq_of_rel
|
||||
|
||||
protected definition elim {P : Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
|
||||
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : seq_colim → P :=
|
||||
|
|
|
@ -55,7 +55,7 @@ parameters {A B : Type.{u}} (f : A → B)
|
|||
(Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a))
|
||||
(Pseg : Π(a : A), seg a ▹ Pbase (f a) = Ptop a)
|
||||
(a : A) : apd (rec Pbase Ptop Pseg) (seg a) = Pseg a :=
|
||||
sorry
|
||||
!rec_eq_of_rel
|
||||
|
||||
protected definition elim {P : Type} (Pbase : B → P) (Ptop : A → P)
|
||||
(Pseg : Π(a : A), Pbase (f a) = Ptop a) (x : cylinder) : P :=
|
||||
|
|
|
@ -53,7 +53,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
|
|||
theorem rec_glue {P : pushout → Type} (Pinl : Π(x : BL), P (inl x))
|
||||
(Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x))
|
||||
(x : TL) : apd (rec Pinl Pinr Pglue) (glue x) = Pglue x :=
|
||||
sorry
|
||||
!rec_eq_of_rel
|
||||
|
||||
protected definition elim {P : Type} (Pinl : BL → P) (Pinr : TR → P)
|
||||
(Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (y : pushout) : P :=
|
||||
|
|
|
@ -47,7 +47,7 @@ parameters {A : Type} (R : A → A → hprop)
|
|||
theorem rec_eq_of_rel {P : quotient → Type} [Pt : Πaa, is_hset (P aa)]
|
||||
(Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')
|
||||
{a a' : A} (H : R a a') : apd (rec Pc Pp) (eq_of_rel H) = Pp H :=
|
||||
sorry
|
||||
!is_hset.elim
|
||||
|
||||
protected definition elim {P : Type} [Pt : is_hset P] (Pc : A → P)
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : quotient) : P :=
|
||||
|
|
|
@ -42,7 +42,7 @@ namespace suspension
|
|||
theorem rec_merid {P : suspension A → Type} (PN : P !north) (PS : P !south)
|
||||
(Pm : Π(a : A), merid a ▹ PN = PS) (a : A)
|
||||
: apd (rec PN PS Pm) (merid a) = Pm a :=
|
||||
sorry
|
||||
!rec_glue
|
||||
|
||||
protected definition elim {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS)
|
||||
(x : suspension A) : P :=
|
||||
|
|
|
@ -19,7 +19,7 @@ namespace type_quotient
|
|||
protected definition elim {P : Type} (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a')
|
||||
(x : type_quotient R) : P :=
|
||||
type_quotient.rec Pc (λa a' H, !tr_constant ⬝ Pp H) x
|
||||
attribute elim [unfold-c 6]
|
||||
|
||||
protected definition elim_on [reducible] {P : Type} (x : type_quotient R)
|
||||
(Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P :=
|
||||
elim Pc Pp x
|
||||
|
@ -49,4 +49,5 @@ namespace type_quotient
|
|||
: type_quotient R → Type :=
|
||||
elim_type H.1 H.2
|
||||
|
||||
|
||||
end type_quotient
|
||||
|
|
Loading…
Add table
Reference in a new issue