Commit f532cf9e authored by Francois THIRE's avatar Francois THIRE

Allows a more general induction

parent 52fc15a3
......@@ -43,25 +43,25 @@ refl : i : level -> A : U i -> x:Term i A -> Term i (eq i A x x).
(; Induction principles ;)
def ind_sigma : i : level -> A : U i -> B : (Term i A -> U i) ->
C : (Term i (sigma i A B) -> U i) ->
g: (x :Term i A -> y : Term i (B x) -> Term i (C (pair i A B x y))) ->
p : (Term i (sigma i A B)) -> Term i (C p).
def ind_sum : i : level -> A : U i -> B : U i -> C : (Term i (sum i A B) -> U i) ->
c : (x : Term i A -> Term i (C (inl i A B x))) ->
d : (y : Term i B -> Term i (C (inr i A B y))) ->
p : (Term i (sum i A B)) -> Term i (C p).
def ind_sigma : i : level -> j : level -> A : U i -> B : (Term i A -> U i) ->
C : (Term i (sigma i A B) -> U j) ->
g: (x :Term i A -> y : Term i (B x) -> Term j (C (pair i A B x y))) ->
p : (Term i (sigma i A B)) -> Term j (C p).
def ind_sum : i : level -> j : level -> A : U i -> B : U i -> C : (Term i (sum i A B) -> U j) ->
c : (x : Term i A -> Term j (C (inl i A B x))) ->
d : (y : Term i B -> Term j (C (inr i A B y))) ->
p : (Term i (sum i A B)) -> Term j (C p).
ind_void : i : level -> C : (Term Z void -> U i) -> a : Term Z void -> Term i (C a).
def ind_unit : i : level -> C : (Term Z unit -> U i) -> c : (Term i (C star)) -> a : Term Z unit -> Term i (C a).
def ind_nat : i : level -> C : (Term Z nat -> U i) -> c0 : (Term i (C 0)) -> cs : (x:Term Z nat -> y : Term i (C x) -> Term i (C (s x))) -> n : Term Z nat -> Term i (C n).
def ind_eq : i : level -> A : U i -> C : (x:Term i A -> y:Term i A -> Term i (eq i A x y) -> U i) -> c : (z:Term i A -> Term i (C z z (refl i A z))) ->
x:Term i A -> y:Term i A -> p:Term i (eq i A x y) -> Term i (C x y p).
def ind_eq : i : level -> j : level -> A : U i -> C : (x:Term i A -> y:Term i A -> Term i (eq i A x y) -> U j) -> c : (z:Term i A -> Term j (C z z (refl i A z))) ->
x:Term i A -> y:Term i A -> p:Term i (eq i A x y) -> Term j (C x y p).
(; Computational rules ;)
[i,A,B,C,g,a,b] ind_sigma i A B C g (pair i A B a b) --> g a b.
[i,A,B,C,c,d,x] ind_sum i A B C c d (inl i A B x) --> c x.
[i,A,B,C,c,d,y] ind_sum i A B C c d (inr i A B y) --> d y.
[i,j,A,B,C,g,a,b] ind_sigma i j A B C g (pair i A B a b) --> g a b.
[i,j,A,B,C,c,d,x] ind_sum i j A B C c d (inl i A B x) --> c x.
[i,j,A,B,C,c,d,y] ind_sum i j A B C c d (inr i A B y) --> d y.
[i,C,c] ind_unit i C c star --> c.
[i,C,c0,cs] ind_nat i C c0 cs 0 --> c0.
[i,C,c0,cs,n] ind_nat i C c0 cs (s n) --> cs n (ind_nat i C c0 cs n).
[i,A,C,c,a] ind_eq i A C c a a (refl i A a) --> c a.
\ No newline at end of file
[i,j,A,C,c,a] ind_eq i j A C c a a (refl i A a) --> c a.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment