Infinitary non-indexed datatype signatures

infinitary.agda

{-# OPTIONS --type-in-type #-}

open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product

data Ind : Set where
  U : Ind
  Pi : (A : Set) -> (A -> Ind) -> Ind

data Ty : Set where
  U : Ty
  Pi : (A : Set) -> (A -> Ty) -> Ty
  PiInd : Ind -> Ty -> Ty

data Ctx : Set where
  Nil : Ctx
  Cons : Ty -> Ctx -> Ctx

data Var : Ctx -> Ty -> Set where
  VZ : ∀ {C A} -> Var (Cons A C) A
  VS : ∀ {C A B} -> Var C A -> Var (Cons B C) A

ElInd : Ind -> Set -> Set
ElInd U X = X
ElInd (Pi A B) X = (x : A) -> ElInd (B x) X

data Tm (C : Ctx) : Ty -> Set where
  El : ∀ {A} -> Var C A -> Tm C A
  App : ∀ {A B} -> Tm C (Pi A B) -> (a : A) -> Tm C (B a)
  AppInd : ∀ {A B} -> Tm C (PiInd A B) -> ElInd A (Tm C U) -> Tm C B

Data : Ctx -> Set
Data C = Tm C U

ElimInd : ∀ {C} (P : Data C -> Set) (A : Ind) -> ElInd A (Data C) -> Set
ElimInd P U t = P t
ElimInd P (Pi A B) f = (x : A) -> ElimInd P (B x) (f x)

ElimTy : ∀ {C} (P : Data C -> Set) (A : Ty) -> Tm C A -> Set
ElimTy P U x = P x
ElimTy P (Pi A B) x = (a : A) -> ElimTy P (B a) (App x a)
ElimTy {C} P (PiInd A B) x = (a : ElInd A (Data C)) -> ElimInd P A a -> ElimTy P B (AppInd x a)

Elim : ∀ {C'} (P : Data C' -> Set) (C : Ctx) -> (∀ {A} -> Var C A -> Var C' A) -> Set
Elim P Nil _ = ⊤
Elim P (Cons ty ctx) k = ElimTy P ty (El (k VZ)) × Elim P ctx (λ x -> k (VS x))

Elim' : (C : Ctx) (P : Data C -> Set) -> Set
Elim' C P = Elim P C (λ x -> x)

elimVar : ∀ {C'} (P : Data C' -> Set) -> ∀ {C A} (v : Var C A) (k : ∀ {A} -> Var C A -> Var C' A) -> Elim P C k -> ElimTy P A (El (k v))
elimVar P VZ k (p , _) = p
elimVar P (VS v) k (_ , ps) = elimVar P v (λ x -> (k (VS x))) ps

elimInd : ∀ {C} (P : Data C -> Set) -> (A : Ind) -> (f : ElInd A (Data C)) -> ((x : Data C) -> ElimTy P U x) -> ElimInd P A f
elimInd P U x ind = ind x
elimInd P (Pi A B) f ind x = elimInd P (B x) (f x) ind

{-# TERMINATING #-}
elimTm : ∀ {C} (P : Data C -> Set) (ps : Elim' C P) -> ∀ {A} (x : Tm C A) -> ElimTy P A x
elimTm P ps (El v) = elimVar P v (λ x -> x) ps
elimTm P ps (App t a) = elimTm P ps t a
elimTm P ps (AppInd {A} t a) = elimTm P ps t a (elimInd P A a (elimTm P ps)) -- I cannot erase A, this is bad!

elim : (C : Ctx) (P : Data C -> Set) (x : Data C) -> Elim' C P -> P x
elim C P x ps = elimTm P ps x

-- testing
UniCtx : Ctx
UniCtx = Cons U (Cons (Pi Set λ A -> PiInd (Pi A λ _ -> U) U) Nil)

Uni : Set
Uni = Data UniCtx

Unit : Uni
Unit = El VZ

UniPi : (A : Set) -> (A -> Uni) -> Uni
UniPi A B = AppInd (App (El (VS VZ)) A) B

indUni : (P : Uni -> Set) (unit : P Unit) (pi : (A : Set) (B : A -> Uni) -> ((x : A) -> P (B x)) -> P (UniPi A B)) (x : Uni) -> P x
indUni P unit pi x = elim _ P x (unit , pi , tt)

el : Uni -> Set
el = indUni (λ _ -> Set) ⊤ (λ A _ ind -> (x : A) -> ind x