Finite datatypes signatures

finite.agda

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

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

record Ty : Set where
  instance constructor U

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

data Tm (C : Ctx) : Ty -> Set where
  El : ∀ {A} -> Var C A -> Tm C A

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

Elim : ∀ {C'} (P : Data C' -> Set) (C : Ctx) -> (∀ {A} -> Var C A -> Var C' A) -> Set
Elim P Nil _ = ⊤
Elim P (Cons U ctx) k = P (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} (v : Var C U) (k : ∀ {A} -> Var C A -> Var C' A) -> Elim P C k -> P (El (k v))
elimVar P VZ k (p , _) = p
elimVar P (VS v) k (_ , ps) = elimVar P v (λ x -> (k (VS x))) ps

elim : (C : Ctx) (P : Data C -> Set) (x : Tm C U) -> Elim' C P -> P x
elim C P (El v) ps = elimVar P v (λ x -> x) ps

-- testing
BoolCtx = Cons U (Cons U Nil)
Bool = Data BoolCtx

True : Bool
True = El VZ

False : Bool
False = El (VS VZ)

indBool : (P : Bool -> Set) -> P True -> P False -> (b : Bool) -> P b
indBool P t f b = elim BoolCtx P b (t , f , tt)

not : Bool -> Bool
not = indBool (λ _ -> Bool) False True