Skip to content

Instantly share code, notes, and snippets.

@bond15

bond15/operad.agda

Created July 15, 2022 00:19
Show Gist options
  • Save bond15/84f27bee8552d7a2c7da9035e415de63 to your computer and use it in GitHub Desktop.
Save bond15/84f27bee8552d7a2c7da9035e415de63 to your computer and use it in GitHub Desktop.
Download ZIP
operad
Raw
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
@bond15
Copy link
Author

bond15 commented Jul 15, 2022

problem in comp3... P 3 only includes op5

@bond15
Copy link
Author

bond15 commented Jul 15, 2022

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 = {!!}

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment