module OTT

mutual

  data U : Type where
    MkU : U
    Zero : U
    One : U
    Two : U
    Pi : (s : U) -> (t : El s -> U) -> U

  El : U -> Type
  El MkU = 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 MkU MkU MkU MkU = One
EQ MkU Zero MkU Zero = One
EQ MkU One MkU One = One
EQ MkU Two MkU Two = One
EQ MkU (Pi s t) MkU (Pi s' t') = Pi s $ \x => Pi s' $ \y => EQ s x s' y ~> EQ MkU (t x) MkU (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 : <| (Basics.id == Basics.id in (OTT.Two ~> OTT.Two)) |>
example = ?prf