Commit d375dc19 authored by Francois THIRE's avatar Francois THIRE

Add a test about Higher Inductive Inductive types

parent 25bbfedd
#NAME test.
type : Type.
eta : type -> Type.
Con : type.
Ty : eta Con -> type.
dot : eta Con.
ccons : gamma:eta Con -> eta (Ty gamma) -> eta Con.
U : gamma:eta Con -> eta (Ty gamma).
Pi : gamma:eta Con -> A:eta (Ty gamma) -> eta (Ty (ccons gamma A)) -> eta (Ty gamma).
ElimCon : P:(eta Con -> type) -> Q:(gamma:eta Con -> eta (P gamma) -> eta (Ty gamma) -> type) ->
eta (P dot) -> (gamma:eta Con -> p:eta (P gamma) -> ty:eta (Ty gamma) -> eta (Q gamma p ty) -> eta (P (ccons gamma ty))) -> (gamma:eta Con -> p:eta (P gamma) -> eta (Q gamma p (U gamma))) ->
(gamma:eta Con -> A : eta (Ty gamma) -> p:(eta (P gamma)) -> ty:eta (Ty (ccons gamma A)) -> pc:(eta (P (ccons gamma A))) -> eta (Q (ccons gamma A) pc ty) -> eta (Q gamma p (Pi gamma A ty))) -> gamma:eta Con -> eta (P gamma).
ElimTy : P:(eta Con -> type) -> Q:(gamma:eta Con -> eta (P gamma) -> eta (Ty gamma) -> type) ->
a:eta (P dot) -> b:(gamma:eta Con -> p:eta (P gamma) -> ty:eta (Ty gamma) -> eta (Q gamma p ty) -> eta (P (ccons gamma ty))) -> c:(gamma:eta Con -> p:eta (P gamma) -> eta (Q gamma p (U gamma))) ->
d:(gamma:eta Con -> A : eta (Ty gamma) -> p:(eta (P gamma)) -> ty:eta (Ty (ccons gamma A)) -> pc:(eta (P (ccons gamma A))) -> eta (Q (ccons gamma A) pc ty) -> eta (Q gamma p (Pi gamma A ty))) -> gamma : eta Con -> A: eta (Ty gamma) -> eta (Q gamma (ElimCon P Q a b c d gamma) A).
Int : type.
Nat : type.
Bool : type.
plus : eta Nat -> eta Nat -> eta Nat.
pair : eta Nat -> eta Nat -> eta Int.
eq : A:type -> eta A -> eta A -> eta Bool.
eps : eta Bool -> Type.
eq_int : a: eta Nat -> b : eta Nat -> c : eta Nat -> d : eta Nat -> eps (eq Nat (plus a d) (plus b c)) -> eps (eq Int (pair a b) (pair c d)).
eq_type : type -> type -> eta Bool.
transport : A : type -> P : (eta A -> type) -> l : eta A -> r : eta A -> eps (eq A l r) -> eta (P l) -> eta (P r).
elimInt : P : (eta Int -> type) -> p:(a : eta Nat -> b : eta Nat -> eta (P (pair a b))) ->
(a: eta Nat -> b : eta Nat -> c : eta Nat -> d : eta Nat -> (e: eps (eq Nat (plus a d) (plus b c)) -> eps (eq (P (pair c d)) (transport Int P (pair a b) (pair c d) (eq_int a b c d e) (p a b)) (p c d)))) -> n : eta Int -> eta (P n).
\ No newline at end of file
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