mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-23 06:57:15 +03:00
43 lines
889 B
Idris
43 lines
889 B
Idris
module OTT
|
|
|
|
mutual
|
|
|
|
data U : Type where
|
|
u : U
|
|
zero : U
|
|
one : U
|
|
two : U
|
|
pi : (s : U) -> (t : El s -> U) -> U
|
|
|
|
El : U -> Type
|
|
El u = U
|
|
El zero = Void
|
|
El one = ()
|
|
El two = Bool
|
|
El (pi s t) = (x : El s) -> El (t x)
|
|
|
|
infixr 10 ~>
|
|
(~>) : U -> U -> U
|
|
s ~> t = pi s $ const t
|
|
|
|
syntax "<|" [s] "|>" = El s
|
|
syntax [x] "==" [y] "in" [s] = EQ s x s y
|
|
|
|
%assert_total
|
|
EQ : (s : U) -> <| s |> -> (t : U) -> <| t |> -> U
|
|
EQ u u u u = one
|
|
EQ u zero u zero = one
|
|
EQ u one u one = one
|
|
EQ u two u two = one
|
|
EQ u (pi s t) u (pi s' t') = pi s $ \x => pi s' $ \y => EQ s x s' y ~> EQ u (t x) u (t' y)
|
|
EQ zero x zero y = one
|
|
EQ one x one y = one
|
|
EQ two True two True = one
|
|
EQ two False two False = one
|
|
EQ (pi s t) f (pi s' t') g = pi s $ \x => pi s' $ \y => EQ s x s' y ~> EQ (t x) (f x) (t' y) (g y)
|
|
EQ _ _ _ _ = zero
|
|
|
|
example : <| (id == id in (two ~> two)) |>
|
|
example = ?prf
|
|
|