feat(hott): add recursor attribute to hits
recursor attribute is added to both the dependent and nondependent elimination, is such a way that the dependent elimination is used by default
This commit is contained in:
parent
8056f326d7
commit
50290fb81c
13 changed files with 32 additions and 29 deletions
|
@ -23,7 +23,7 @@ namespace cubical
|
|||
|
||||
notation b `=[`:50 p:0 `]`:0 b₂:50 := pathover _ b p b₂
|
||||
|
||||
definition idpo [reducible] {b : B a} : b =[refl a] b :=
|
||||
definition idpo [reducible] [constructor] {b : B a} : b =[refl a] b :=
|
||||
pathover.idpatho b
|
||||
|
||||
/- equivalences with equality using transport -/
|
||||
|
@ -121,7 +121,7 @@ namespace cubical
|
|||
definition pathover_idp_of_eq {b' : B a} (q : b = b') : b =[idpath a] b' :=
|
||||
pathover_of_transport_eq q
|
||||
|
||||
definition idp_rec_on {P : Π⦃b₂ : B a⦄, b =[idpath a] b₂ → Type}
|
||||
definition idp_rec_on [recursor] {P : Π⦃b₂ : B a⦄, b =[idpath a] b₂ → Type}
|
||||
{b₂ : B a} (r : b =[idpath a] b₂) (H : P idpo) : P r :=
|
||||
have H2 : P (pathover_idp_of_eq (eq_of_pathover_idp r)),
|
||||
from eq.rec_on (eq_of_pathover_idp r) H,
|
||||
|
|
|
@ -26,13 +26,13 @@ namespace cubical
|
|||
variables {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} {s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁}
|
||||
{s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃} {s₃₃ : square p₃₂ p₃₄ p₂₃ p₄₃}
|
||||
|
||||
definition ids [reducible] := @square.ids
|
||||
definition idsquare [reducible] (a : A) := @square.ids A a
|
||||
definition ids [reducible] [constructor] := @square.ids
|
||||
definition idsquare [reducible] [constructor] (a : A) := @square.ids A a
|
||||
|
||||
definition hrefl (p : a = a') : square idp idp p p :=
|
||||
definition hrefl [unfold-c 4] (p : a = a') : square idp idp p p :=
|
||||
by cases p; exact ids
|
||||
|
||||
definition vrefl (p : a = a') : square p p idp idp :=
|
||||
definition vrefl [unfold-c 4] (p : a = a') : square p p idp idp :=
|
||||
by cases p; exact ids
|
||||
|
||||
definition hconcat (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁)
|
||||
|
@ -74,7 +74,7 @@ namespace cubical
|
|||
{ intro s, cases s, apply idp},
|
||||
end
|
||||
|
||||
definition rec_on_b {a₀₀ : A}
|
||||
definition rec_on_b [recursor] {a₀₀ : A}
|
||||
{P : Π{a₂₀ a₁₂ : A} {t : a₀₀ = a₂₀} {l : a₀₀ = a₁₂} {r : a₂₀ = a₁₂}, square t idp l r → Type}
|
||||
{a₂₀ a₁₂ : A} {t : a₀₀ = a₂₀} {l : a₀₀ = a₁₂} {r : a₂₀ = a₁₂}
|
||||
(s : square t idp l r) (H : P ids) : P s :=
|
||||
|
@ -82,7 +82,7 @@ namespace cubical
|
|||
from eq.rec_on (eq_of_square s : t ⬝ r = l) (by cases r; cases t; exact H),
|
||||
left_inv (to_fun !square_equiv_eq) s ▸ H2
|
||||
|
||||
definition rec_on_r {a₀₀ : A}
|
||||
definition rec_on_r [recursor] {a₀₀ : A}
|
||||
{P : Π{a₀₂ a₂₁ : A} {t : a₀₀ = a₂₁} {b : a₀₂ = a₂₁} {l : a₀₀ = a₀₂}, square t b l idp → Type}
|
||||
{a₀₂ a₂₁ : A} {t : a₀₀ = a₂₁} {b : a₀₂ = a₂₁} {l : a₀₀ = a₀₂}
|
||||
(s : square t b l idp) (H : P ids) : P s :=
|
||||
|
@ -91,7 +91,7 @@ namespace cubical
|
|||
from @eq.rec_on _ _ (λx p, P (square_of_eq p⁻¹)) _ p (by cases b; cases l; exact H),
|
||||
left_inv (to_fun !square_equiv_eq) s ▸ !inv_inv ▸ H2
|
||||
|
||||
definition rec_on_l {a₀₁ : A}
|
||||
definition rec_on_l [recursor] {a₀₁ : A}
|
||||
{P : Π {a₂₀ a₂₂ : A} {t : a₀₁ = a₂₀} {b : a₀₁ = a₂₂} {r : a₂₀ = a₂₂},
|
||||
square t b idp r → Type}
|
||||
{a₂₀ a₂₂ : A} {t : a₀₁ = a₂₀} {b : a₀₁ = a₂₂} {r : a₂₀ = a₂₂}
|
||||
|
@ -101,7 +101,7 @@ namespace cubical
|
|||
from eq.rec_on p (by cases r; cases t; exact H),
|
||||
left_inv (to_fun !square_equiv_eq) s ▸ !con_inv_cancel_right ▸ H2
|
||||
|
||||
definition rec_on_t {a₁₀ : A}
|
||||
definition rec_on_t [recursor] {a₁₀ : A}
|
||||
{P : Π {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂}, square idp b l r → Type}
|
||||
{a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂}
|
||||
(s : square idp b l r) (H : P ids) : P s :=
|
||||
|
@ -116,7 +116,7 @@ namespace cubical
|
|||
left_inv (to_fun !square_equiv_eq) s ▸ H4
|
||||
qed
|
||||
|
||||
definition rec_on_tb {a : A}
|
||||
definition rec_on_tb [recursor] {a : A}
|
||||
{P : Π{b : A} {l : a = b} {r : a = b}, square idp idp l r → Type}
|
||||
{b : A} {l : a = b} {r : a = b}
|
||||
(s : square idp idp l r) (H : P ids) : P s :=
|
||||
|
|
|
@ -148,15 +148,15 @@ namespace circle
|
|||
by rewrite [tr_inv_fn,↑to_inv]; apply inv_eq_inv; apply elim_type_loop
|
||||
end circle
|
||||
|
||||
attribute circle.base circle.base1 circle.base2 [constructor]
|
||||
attribute circle.rec circle.elim [unfold-c 4]
|
||||
attribute circle.elim_type [unfold-c 3]
|
||||
attribute circle.rec_on circle.elim_on [unfold-c 2]
|
||||
attribute circle.elim_type_on [unfold-c 1]
|
||||
attribute circle.rec2 circle.elim2 [unfold-c 6]
|
||||
attribute circle.base1 circle.base2 circle.base [constructor]
|
||||
attribute circle.rec2 circle.elim2 [unfold-c 6] [recursor 6]
|
||||
attribute circle.elim2_type [unfold-c 5]
|
||||
attribute circle.rec2_on circle.elim2_on [unfold-c 2]
|
||||
attribute circle.elim2_type [unfold-c 1]
|
||||
attribute circle.elim circle.rec [unfold-c 4] [recursor 4]
|
||||
attribute circle.elim_type [unfold-c 3]
|
||||
attribute circle.rec_on circle.elim_on [unfold-c 2]
|
||||
attribute circle.elim_type_on [unfold-c 1]
|
||||
|
||||
namespace circle
|
||||
definition pointed_circle [instance] [constructor] : pointed circle :=
|
||||
|
|
|
@ -79,7 +79,7 @@ end
|
|||
end coeq
|
||||
|
||||
attribute coeq.coeq_i [constructor]
|
||||
attribute coeq.rec coeq.elim [unfold-c 8]
|
||||
attribute coeq.elim coeq.rec [unfold-c 8] [recursor 8]
|
||||
attribute coeq.elim_type [unfold-c 7]
|
||||
attribute coeq.rec_on coeq.elim_on [unfold-c 6]
|
||||
attribute coeq.elim_type_on [unfold-c 5]
|
||||
|
|
|
@ -171,11 +171,11 @@ end
|
|||
end seq_colim
|
||||
|
||||
attribute colimit.incl seq_colim.inclusion [constructor]
|
||||
attribute colimit.rec colimit.elim [unfold-c 10]
|
||||
attribute colimit.elim colimit.rec [unfold-c 10] [recursor 10]
|
||||
attribute colimit.elim_type [unfold-c 9]
|
||||
attribute colimit.rec_on colimit.elim_on [unfold-c 8]
|
||||
attribute colimit.elim_type_on [unfold-c 7]
|
||||
attribute seq_colim.rec seq_colim.elim [unfold-c 6]
|
||||
attribute seq_colim.elim seq_colim.rec [unfold-c 6] [recursor 6]
|
||||
attribute seq_colim.elim_type [unfold-c 5]
|
||||
attribute seq_colim.rec_on seq_colim.elim_on [unfold-c 4]
|
||||
attribute seq_colim.elim_type_on [unfold-c 3]
|
||||
|
|
|
@ -89,7 +89,7 @@ end
|
|||
end cylinder
|
||||
|
||||
attribute cylinder.base cylinder.top [constructor]
|
||||
attribute cylinder.rec cylinder.elim [unfold-c 8]
|
||||
attribute cylinder.elim cylinder.rec [unfold-c 8] [recursor 8]
|
||||
attribute cylinder.elim_type [unfold-c 7]
|
||||
attribute cylinder.rec_on cylinder.elim_on [unfold-c 5]
|
||||
attribute cylinder.elim_type_on [unfold-c 4]
|
||||
|
|
|
@ -111,7 +111,7 @@ end
|
|||
end pushout
|
||||
|
||||
attribute pushout.inl pushout.inr [constructor]
|
||||
attribute pushout.rec pushout.elim [unfold-c 10]
|
||||
attribute pushout.elim pushout.rec [unfold-c 10] [recursor 10]
|
||||
attribute pushout.elim_type [unfold-c 9]
|
||||
attribute pushout.rec_on pushout.elim_on [unfold-c 7]
|
||||
attribute pushout.elim_type_on [unfold-c 6]
|
||||
|
|
|
@ -72,5 +72,5 @@ end
|
|||
end quotient
|
||||
|
||||
attribute quotient.class_of [constructor]
|
||||
attribute quotient.rec quotient.elim [unfold-c 7]
|
||||
attribute quotient.elim quotient.rec [unfold-c 7] [recursor]
|
||||
attribute quotient.rec_on quotient.elim_on [unfold-c 4]
|
||||
|
|
|
@ -72,7 +72,7 @@ namespace suspension
|
|||
end suspension
|
||||
|
||||
attribute suspension.north suspension.south [constructor]
|
||||
attribute suspension.rec suspension.elim [unfold-c 6]
|
||||
attribute suspension.elim suspension.rec [unfold-c 6] [recursor 6]
|
||||
attribute suspension.elim_type [unfold-c 5]
|
||||
attribute suspension.rec_on suspension.elim_on [unfold-c 3]
|
||||
attribute suspension.elim_type_on [unfold-c 2]
|
||||
|
|
|
@ -16,7 +16,7 @@ open is_trunc eq equiv is_equiv function prod sum sigma
|
|||
|
||||
namespace trunc
|
||||
|
||||
protected definition elim {n : trunc_index} {A : Type} {P : Type}
|
||||
protected definition elim [recursor 6] {n : trunc_index} {A : Type} {P : Type}
|
||||
[Pt : is_trunc n P] (H : A → P) : trunc n A → P :=
|
||||
trunc.rec H
|
||||
|
||||
|
@ -132,3 +132,4 @@ end trunc
|
|||
|
||||
attribute trunc.elim [unfold-c 6]
|
||||
attribute trunc.elim_on [unfold-c 4]
|
||||
attribute trunc.rec [recursor]
|
||||
|
|
|
@ -48,7 +48,8 @@ namespace type_quotient
|
|||
type_quotient.elim_type H.1 H.2
|
||||
end type_quotient
|
||||
|
||||
attribute type_quotient.elim [unfold-c 6]
|
||||
attribute type_quotient.elim [unfold-c 6] [recursor 6]
|
||||
attribute type_quotient.elim_type [unfold-c 5]
|
||||
attribute type_quotient.elim_on [unfold-c 4]
|
||||
attribute type_quotient.elim_type_on [unfold-c 3]
|
||||
attribute type_quotient.rec [recursor]
|
||||
|
|
|
@ -253,6 +253,6 @@ is_equiv.left_inv apd10 idp
|
|||
definition naive_funext_of_ua : naive_funext :=
|
||||
λ A P f g h, eq_of_homotopy h
|
||||
|
||||
protected definition homotopy.rec_on {Q : (f ∼ g) → Type} (p : f ∼ g)
|
||||
protected definition homotopy.rec_on [recursor] {Q : (f ∼ g) → Type} (p : f ∼ g)
|
||||
(H : Π(q : f = g), Q (apd10 q)) : Q p :=
|
||||
right_inv apd10 p ▸ H (eq_of_homotopy p)
|
||||
|
|
|
@ -39,8 +39,9 @@ namespace trunc
|
|||
protected constant rec {n : trunc_index} {A : Type} {P : trunc n A → Type}
|
||||
[Pt : Πaa, is_trunc n (P aa)] (H : Πa, P (tr a)) : Πaa, P aa
|
||||
|
||||
protected definition rec_on [reducible] {n : trunc_index} {A : Type} {P : trunc n A → Type}
|
||||
(aa : trunc n A) [Pt : Πaa, is_trunc n (P aa)] (H : Πa, P (tr a)) : P aa :=
|
||||
protected definition rec_on [reducible] {n : trunc_index} {A : Type}
|
||||
{P : trunc n A → Type} (aa : trunc n A) [Pt : Πaa, is_trunc n (P aa)] (H : Πa, P (tr a))
|
||||
: P aa :=
|
||||
trunc.rec H aa
|
||||
end trunc
|
||||
|
||||
|
|
Loading…
Reference in a new issue