ABTs.agda

module ABT1 where

  {-# NO_POSITIVITY_CHECK #-}
  data Syntax {S : Set} (F : (S → Set) → S → Set) : S → Set where
    var : ∀ {s} → ℕ → Syntax F s
    <_> : ∀ {s} → F (Syntax F) s → Syntax F s


module ABT2 where

  mutual
    data Syntax' {S : Set} (C : List S → S → Set) : S → Set where
      var : ∀ {s} → ℕ → Syntax' C s
      _$_ : ∀ {ss s} → C ss s → Args C ss → Syntax' C s
    
    data Args {S : Set} (C : List S → S → Set) : List S → Set where
      [] : Args C []
      _∷_ : ∀ {s ss} → Syntax' C s → Args C ss → Args C (s ∷ ss)