Infinitary mutual inductive families signatures with a single index

infinitary-mutual-single-index.agda

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

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

data IxCtx : Set where
  Nil : IxCtx
  Cons : Set -> IxCtx -> IxCtx

data IxVar : IxCtx -> Set -> Set where
  VZ : ∀ {C A} -> IxVar (Cons A C) A
  VS : ∀ {C A B} -> IxVar C A -> IxVar (Cons B C) A

data IxTm (C : IxCtx) : Set where
  Con : ∀ {A} -> IxVar C A -> A -> IxTm C

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

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

data Ctx (I : IxCtx) : Set where
  Nil : Ctx I
  Cons : Ty I -> Ctx I -> Ctx I

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

ElInd : ∀ {I} -> Ind I -> (IxTm I -> Set) -> Set
ElInd (U i) X = X i
ElInd (Pi A B) X = (x : A) -> ElInd (B x) X

data Tm {I} (C : Ctx I) : Ty I -> 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 (λ i -> Tm C (U i)) -> Tm C B

Data : ∀ {I} -> Ctx I -> IxTm I -> Set
Data C i = Tm C (U i)

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

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

Elim : ∀ {I} {C' : Ctx I} (P : {i : IxTm I} -> Data C' i -> Set) (C : Ctx I) -> (∀ {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' : ∀ {I} (C : Ctx I) (P : {i : IxTm I} -> Data C i -> Set) -> Set
Elim' C P = Elim P C (λ x -> x)

elimVar : ∀ {I} {C' : Ctx I} (P : {i : IxTm I} -> Data C' i -> 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 : ∀ {I} {C : Ctx I} (P : {i : IxTm I} -> Data C i -> Set) -> (A : Ind I) -> (f : ElInd A (Data C)) -> ({i : IxTm I} -> (x : Data C i) -> ElimTy P (U i) x) -> ElimInd P A f
elimInd P (U i) x ind = ind x
elimInd P (Pi A B) f ind x = elimInd P (B x) (f x) ind

{-# TERMINATING #-}
elimTm : ∀ {I} {C : Ctx I} (P : {i : IxTm I} -> Data C i -> 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 : ∀ {I} (C : Ctx I) (P : {i : IxTm I} -> Data C i -> Set) {i : IxTm I} (x : Data C i) -> Elim' C P -> P x
elim C P x ps = elimTm P ps x

-- testing
NatCtx : Ctx (Cons ⊤ Nil)
NatCtx = Cons (U (Con VZ tt)) (Cons (PiInd (U (Con VZ tt)) (U (Con VZ tt))) Nil)

Nat : Set
Nat = Data NatCtx (Con VZ tt)

Z : Nat
Z = El VZ

S : Nat -> Nat
S n = AppInd (El (VS VZ)) n

FinSortCtx : IxCtx
FinSortCtx = Cons Nat Nil

FinCtx : Ctx FinSortCtx
FinCtx = Cons (Pi Nat λ n -> U (Con VZ (S n))) (Cons (Pi Nat λ n -> PiInd (U (Con VZ n)) (U (Con VZ (S n)))) Nil)

Fin : Nat -> Set
Fin n = Data FinCtx (Con VZ n)

FZ : {n : Nat} -> Fin (S n)
FZ {n} = App (El VZ) n

FS : {n : Nat} -> Fin n -> Fin (S n)
FS {n} x = AppInd (App (El (VS VZ)) n) x

lift : ({n : Nat} -> Fin n -> Set) -> ({n : IxTm FinSortCtx} -> Data FinCtx n -> Set)
lift f {Con VZ n} d = f {n} d

indFin :
  (P : {n : Nat} -> Fin n -> Set)
  (z : {n : Nat} -> P {S n} FZ)
  (s : {n : Nat} -> (x : Fin n) -> P x -> P (FS x))
  {n : Nat} (x : Fin n) -> P x
indFin P z s x = elim _ (lift P) x ((λ n -> z {n}) , (λ n -> s {n}) , tt)

finToNat : ∀ {n} -> Fin n -> Nat
finToNat = indFin (λ _ -> Nat) Z (λ _ ind -> S ind)

-- even odd
EvenOddSortCtx : IxCtx
EvenOddSortCtx = Cons Nat (Cons Nat Nil)

EvenOddCtx : Ctx EvenOddSortCtx
EvenOddCtx = Cons (U (Con VZ Z)) (Cons (Pi Nat λ n -> PiInd (U (Con (VS VZ) n)) (U (Con VZ (S n)))) (Cons (Pi Nat λ n -> PiInd (U (Con VZ n)) (U (Con (VS VZ) (S n)))) Nil))

Even : Nat -> Set
Even n = Data EvenOddCtx (Con VZ n)

Odd : Nat -> Set
Odd n = Data EvenOddCtx (Con (VS VZ) n)

EvenZ : Even Z
EvenZ = El VZ

EvenS : {n : Nat} -> Odd n -> Even (S n)
EvenS {n} o = AppInd (App (El (VS VZ)) n) o 

OddS : {n : Nat} -> Even n -> Odd (S n)
OddS {n} o = AppInd (App (El (VS (VS VZ))) n) o

lift' : ({n : Nat} -> Even n -> Set) -> ({n : Nat} -> Odd n -> Set) -> ({i : IxTm EvenOddSortCtx} -> Data EvenOddCtx i -> Set)
lift' P Q {Con VZ n} d = P {n} d
lift' P Q {Con (VS VZ) n} d = Q {n} d

indEven :
  (P : {n : Nat} -> Even n -> Set)
  (Q : {n : Nat} -> Odd n -> Set)
  (eZ : P EvenZ)
  (eS : {n : Nat} (o : Odd n) -> Q o -> P (EvenS o))
  (oS : {n : Nat} (e : Even n) -> P e -> Q (OddS e))
  {n : Nat} (x : Even n) -> P x
indEven P Q eZ eS oS {n} x = elim _ (lift' P Q) x (eZ , (λ n -> eS {n}) , (λ n -> oS {n}) , tt)

indOdd :
  (P : {n : Nat} -> Even n -> Set)
  (Q : {n : Nat} -> Odd n -> Set)
  (eZ : P EvenZ)
  (eS : {n : Nat} (o : Odd n) -> Q o -> P (EvenS o))
  (oS : {n : Nat} (e : Even n) -> P e -> Q (OddS e))
  {n : Nat} (x : Odd n) -> Q x
indOdd P Q eZ eS oS {n} x = elim _ (lift' P Q) x (eZ , (λ n -> eS {n}) , (λ n -> oS {n}) , tt)