operad

operad.agda

open import Data.Nat
open import Data.Bool hiding(_<?_)
open import Level hiding (suc)

data ⊥ {ℓ : Level} : Set ℓ where

data type : Set where
  𝕦 𝕓 𝕟 : type

--P : Set
--P = ℕ → type

data nary (n : ℕ) : Set₁ where 

--data unary : Set₁ where
--  op : Set → Set → unary

data unary : Set₁ where
  id : {A : Set} → (A → A) → unary
  op1 : (Bool → Bool) → unary
  op2 : (Bool → ℕ) → unary

data binary : Set₁ where
  op3 : (Bool → Bool → Bool) → binary
  op4 : (ℕ → Bool → Bool) → binary

data trinary : Set₁ where
  op5 : (ℕ → ℕ → ℕ → ℕ) → trinary

P : ℕ → Set₁
P 0 = ⊥ -- nary 0
P 1 = unary
P 2 = binary
P 3 = trinary
P n = ⊥


sum : (n : ℕ) → ℕ
sum 0 = 0
sum (suc n) = suc n + sum n

{-# TERMINATING #-}
telescope' : (n i : ℕ) → Set₁
telescope' n 0 = ⊥ -- dne
telescope' n 1 = P 1 → (telescope' n 2)
telescope' n m with m <ᵇ n
... | true = P m → telescope' n (suc m) 
... | false = P n

telescope : ℕ → Set₁
telescope n = telescope' n 1 

comp :  { n : ℕ} → P n → telescope n → P (sum n)
comp = {!telescope 3 !}

comp3 : P 3 → telescope 3 → P (sum 3)
comp3 (op5 x) y = {! !}


--idP : ∀{P : ℕ → Set} → P 1
--idP = {!!}


idP : {A : Set} → P 1
idP {A} = id {A} λ x → x

problem in comp3... P 3 only includes op5

nope

data base : Set where
  𝕦 𝕟 𝕓 : base

data type : Set where
  [_] : base → type
  _⇒_ : type → type → type

open import Data.Unit

⦅_⦆ : type → Set
⦅ [ 𝕦 ] ⦆ = ⊤
⦅ [ 𝕓 ] ⦆ = Bool
⦅ [ 𝕟 ] ⦆ = ℕ
⦅ x ⇒ y ⦆ = ⦅ x ⦆ → ⦅ y ⦆

nary : (n : ℕ) → Set
nary 0 = type
nary (suc n) = type → nary n

-- P ≡ nary
P : ℕ → Set
P = nary 

_ : P 3
_ = λ t₁ t₂ t₃ → {!!}

comp3 : {!!}
comp3 = {!!}