Skip to content

Instantly share code, notes, and snippets.

@atennapel
Last active January 4, 2022 17:50
Show Gist options
  • Save atennapel/3080f5cfd240efc1cb3ef275e07fc85b to your computer and use it in GitHub Desktop.
Save atennapel/3080f5cfd240efc1cb3ef275e07fc85b to your computer and use it in GitHub Desktop.
Finitary non-indexed datatype signatures
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
data Ty : Set where
U : Ty
Pi : (A : Set) -> (A -> Ty) -> Ty
PiInd : 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
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 : ∀ {B} -> Tm C (PiInd B) -> Tm C U -> Tm C B
Data : Ctx -> Set
Data C = Tm C U
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 B) x = (a : Data C) -> P 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
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 t a) = elimTm P ps t a (elimTm P ps a)
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
NatCtx : Ctx
NatCtx = Cons U (Cons (PiInd U) Nil)
Nat : Set
Nat = Data NatCtx
Z : Nat
Z = El VZ
S : Nat -> Nat
S n = AppInd (El (VS VZ)) n
indNat : (P : Nat -> Set) (z : P Z) (s : (m : Nat) -> P m -> P (S m)) (n : Nat) -> P n
indNat P z s n = elim _ P n (z , s , tt)
paraNat : ∀ {A} -> Nat -> A -> (Nat -> A -> A) -> A
paraNat {A} n z s = indNat (λ _ -> A) z s n
add : Nat -> Nat -> Nat
add a b = paraNat a b (λ _ -> S)
n1 = S Z
n2 = S (S Z)
n3 = S (S (S Z))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment