Skip to content

Instantly share code, notes, and snippets.

@Kazark
Last active November 30, 2020 21:37
Show Gist options
  • Save Kazark/5fb4b3600e46ae9d1cac88778452eea2 to your computer and use it in GitHub Desktop.
Save Kazark/5fb4b3600e46ae9d1cac88778452eea2 to your computer and use it in GitHub Desktop.
What if Pair and Either were primitive, and other arities of product and coproduct types were generated from them?
module NTypes where
open import Data.Empty using (⊥)
open import Agda.Builtin.Unit using (⊤)
open import Data.Nat using (ℕ; zero; suc)
open import Function using (id; _∘_)
infixr 5 _∧_ _v_ _-ary_to_ _,_
record _∧_ (a : Set) (b : Set) : Set where
constructor _,_
field 1st : a
field 2nd : b
_∙ : {a : Set} → a -> a ∧ ⊤
_∙ x = x , _
data _v_ a b : Set where
←|_ : a → a v b
|→_ : b → a v b
NSet : ℕ → Set₁
NSet zero = Set
NSet (suc n) = Set → NSet n
_-ary_to_ : (n : ℕ) → (Set → Set → Set) → Set → NSet n
n -ary f to t0 = nary n id f t0 where
nary : (n : ℕ) → (Set → Set) → (Set → Set → Set) → Set → NSet n
nary zero k _ t0 = k t0
nary (suc n) k f t0 t = nary n (k ∘ f t) f t0
/\ : (n : ℕ) → NSet n
/\ n = n -ary _∧_ to ⊤
\/ : (n : ℕ) → NSet n
\/ n = n -ary _v_ to ⊥
data F : Set where
f ph : F
data O : Set where
o oo ooo : O
foo : /\ 3 F O O
foo = ph , oo , ooo ∙
eff : \/ 3 F O O
eff = ←| f
off : \/ 3 F O O
off = |→ ←| o
oof : \/ 3 F O O
oof = |→ |→ ←| oo
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment