From f0412fa091ff84c3986ca5dea04bda3a79415b87 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 26 Nov 2017 14:57:19 +0100
Subject: [PATCH] Add stub for implementing the cubical type system

---
 src/Category/Cubical.agda | 47 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 src/Category/Cubical.agda

diff --git a/src/Category/Cubical.agda b/src/Category/Cubical.agda
new file mode 100644
index 0000000..22709be
--- /dev/null
+++ b/src/Category/Cubical.agda
@@ -0,0 +1,47 @@
+module Category.Cubical where
+
+open import Agda.Primitive
+open import Category
+open import Data.Bool
+open import Data.Product
+open import Data.Sum
+open import Data.Unit
+open import Data.Empty
+
+module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
+  -- Σ is the "namespace"
+  ℓo = (lsuc lzero ⊔ ℓ)
+
+  FiniteDecidableSubset : Set ℓ
+  FiniteDecidableSubset = Ns → Bool
+
+  isTrue : Bool → Set
+  isTrue false = ⊥
+  isTrue true = ⊤
+
+  elmsof : (Ns → Bool) → Set ℓ
+  elmsof P = (σ : Ns) → isTrue (P σ)
+
+  𝟚 : Set
+  𝟚 = Bool
+
+  module _ (I J : FiniteDecidableSubset) where
+    private
+      themap : Set {!!}
+      themap = elmsof I → elmsof J ⊎ 𝟚
+      rules : (elmsof I → elmsof J ⊎ 𝟚) → Set
+      rules f = (i j : elmsof I) → {!!}
+
+    Mor = Σ themap rules
+
+  -- The category of names and substitutions
+  ℂ : Category -- {ℓo} {lsuc lzero ⊔ ℓo}
+  ℂ = record
+    -- { Object = FiniteDecidableSubset
+    { Object = Ns → Bool
+    ; Arrow = Mor
+    ; 𝟙 = {!!}
+    ; _⊕_ = {!!}
+    ; assoc = {!!}
+    ; ident = {!!}
+    }