Merge branch 'hypergraph-conversion'

12 files changed, 1307 insertions, 0 deletions

diff --git a/Data/Castable.agda b/Data/Castable.agda
new file mode 100644
index 0000000..4f85b3d
--- /dev/null
+++ b/Data/Castable.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Castable where
+
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst; cong; module ≡-Reasoning)
+open import Relation.Binary using (Sym; Trans; _⇒_)
+
+record IsCastable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
+
+  field
+    cast : {e e′ : A} → .(e ≡ e′) → B e → B e′
+    cast-trans
+        : {m n o : A}
+        → .(eq₁ : m ≡ n)
+          .(eq₂ : n ≡ o)
+          (x : B m)
+        → cast eq₂ (cast eq₁ x) ≡ cast (trans eq₁ eq₂) x
+    cast-is-id : {m : A} .(eq : m ≡ m) (x : B m) → cast eq x ≡ x
+    subst-is-cast : {m n : A} (eq : m ≡ n) (x : B m) → subst B eq x ≡ cast eq x
+
+  infix 3 _≈[_]_
+  _≈[_]_ : {n m : A} → B n → .(eq : n ≡ m) → B m → Set ℓ₂
+  _≈[_]_ x eq y = cast eq x ≡ y
+
+  ≈-reflexive : {n : A} → _≡_ ⇒ (λ xs ys → _≈[_]_ {n} xs refl ys)
+  ≈-reflexive {n} {x} {y} eq = trans (cast-is-id refl x) eq
+
+  ≈-sym : {m n : A} .{m≡n : m ≡ n} → Sym _≈[ m≡n ]_ _≈[ sym m≡n ]_
+  ≈-sym {m} {n} {m≡n} {x} {y} x≡y = begin
+      cast (sym m≡n) y             ≡⟨ cong (cast (sym m≡n)) x≡y ⟨
+      cast (sym m≡n) (cast m≡n x)  ≡⟨ cast-trans m≡n (sym m≡n) x ⟩
+      cast (trans m≡n (sym m≡n)) x ≡⟨ cast-is-id (trans m≡n (sym m≡n)) x ⟩
+      x ∎
+    where
+      open ≡-Reasoning
+
+  ≈-trans : {m n o : A} .{m≡n : m ≡ n} .{n≡o : n ≡ o} → Trans _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_
+  ≈-trans {m} {n} {o} {m≡n} {n≡o} {x} {y} {z} x≡y y≡z = begin
+      cast (trans m≡n n≡o) x  ≡⟨ cast-trans m≡n n≡o x ⟨
+      cast n≡o (cast m≡n x)   ≡⟨ cong (cast n≡o) x≡y ⟩
+      cast n≡o y              ≡⟨ y≡z ⟩
+      z ∎
+    where
+      open ≡-Reasoning
+
+record Castable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} : Set (suc (ℓ₁ ⊔ ℓ₂)) where
+  field
+    B : A → Set ℓ₂
+    isCastable : IsCastable B
diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda
new file mode 100644
index 0000000..ce6de69
--- /dev/null
+++ b/Data/Circuit/Convert.agda
@@ -0,0 +1,201 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Circuit.Convert where
+
+open import Data.Nat.Base using (ℕ)
+open import Data.Circuit.Gate using (Gate; GateLabel; cast-gate; cast-gate-is-id; subst-is-cast-gate)
+open import Data.Fin.Base using (Fin)
+open import Data.Hypergraph.Edge GateLabel using (Edge)
+open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph; mkHypergraph)
+open import Data.Hypergraph.Setoid GateLabel using (Hypergraph-Setoid; ≈-Hypergraph)
+open import Data.Permutation using (fromList-↭; toList-↭)
+open import Data.List using (length)
+open import Data.Vec.Functional using (toVec; fromVec; toList; fromList)
+open import Function.Bundles using (Equivalence; _↔_)
+open import Function.Base using (_∘_; id)
+open import Data.List.Relation.Binary.Permutation.Homogeneous using (Permutation)
+open import Data.Product.Base using (proj₁; proj₂; _×_)
+open import Data.Fin.Permutation using (flip; _⟨$⟩ˡ_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
+
+import Function.Reasoning as →-Reasoning
+import Data.List.Relation.Binary.Permutation.Propositional as L
+import Data.Vec.Functional.Relation.Binary.Permutation as V
+import DecorationFunctor.Hypergraph.Labeled as LabeledHypergraph
+
+open LabeledHypergraph using (Hypergraph-same) renaming (Hypergraph to Hypergraph′; Hypergraph-setoid to Hypergraph-Setoid′)
+
+to : {v : ℕ} → Hypergraph v → Hypergraph′ v
+to H = record
+    { h = length edges
+    ; a = arity ∘ fromList edges
+    ; j = fromVec ∘ ports ∘ fromList edges
+    ; l = label ∘ fromList edges
+    }
+  where
+    open Edge using (arity; ports; label)
+    open Hypergraph H
+
+from : {v : ℕ} → Hypergraph′ v → Hypergraph v
+from {v} H = record
+    { edges = toList asEdge
+    }
+  where
+    open Hypergraph′ H
+    asEdge : Fin h → Edge v
+    asEdge e = record { label = l e ; ports = toVec (j e) }
+
+to-cong : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → Hypergraph-same (to H) (to H′)
+to-cong {v} {H} {H′} ≈H = record
+    { ↔h = flip ρ
+    ; ≗a = ≗a
+    ; ≗j = ≗j
+    ; ≗l = ≗l
+    }
+  where
+    open Edge using (arity; ports; label)
+    open ≈-Hypergraph ≈H
+    open import Data.Fin.Permutation using (_⟨$⟩ʳ_; _⟨$⟩ˡ_; Permutation′; inverseʳ)
+    open import Data.Fin.Base using (cast)
+    open import Data.Fin.Properties using (cast-is-id)
+    ρ : Fin (length H′.edges) ↔ Fin (length H.edges)
+    ρ = proj₁ (fromList-↭ ↭edges)
+
+    open ≡.≡-Reasoning
+    edges≗ρ∘edges′ : (i : Fin (length H.edges)) → fromList H.edges i ≡ fromList H′.edges (ρ ⟨$⟩ˡ i)
+    edges≗ρ∘edges′ i = begin
+        fromList H.edges i                    ≡⟨ ≡.cong (fromList H.edges) (inverseʳ ρ) ⟨
+        fromList H.edges (ρ ⟨$⟩ʳ (ρ ⟨$⟩ˡ i))  ≡⟨ proj₂ (fromList-↭ ↭edges) (ρ ⟨$⟩ˡ i) ⟩
+        fromList H′.edges (ρ ⟨$⟩ˡ i)          ∎
+
+    ≗a : (e : Fin (Hypergraph′.h (to H)))
+        → Hypergraph′.a (to H) e
+        ≡ arity (fromList H′.edges (ρ ⟨$⟩ˡ e))
+    ≗a = ≡.cong arity ∘ edges≗ρ∘edges′
+
+    ≗j : (e : Fin (Hypergraph′.h (to H)))
+          (i : Fin (Hypergraph′.a (to H) e))
+        → fromVec (ports (fromList H.edges e)) i
+        ≡ fromVec (ports (fromList H′.edges (ρ ⟨$⟩ˡ e))) (cast (≗a e) i)
+    ≗j e i
+      rewrite edges≗ρ∘edges′ e
+      rewrite cast-is-id ≡.refl i = ≡.refl
+
+    ≗l : (e : Fin (Hypergraph′.h (to H)))
+        → label (fromList H.edges e)
+        ≡ cast-gate (≡.sym (≗a e)) (label (fromList H′.edges (ρ ⟨$⟩ˡ e)))
+    ≗l e
+      rewrite edges≗ρ∘edges′ e
+      rewrite cast-gate-is-id ≡.refl (label (fromList H′.edges (ρ ⟨$⟩ˡ e))) =
+          ≡.refl
+
+module _ {v : ℕ} where
+  open import Data.Hypergraph.Edge GateLabel using (decTotalOrder; ≈-Edge; ≈-Edge-IsEquivalence; ≈-Edge⇒≡)
+  open import Data.List.Sort (decTotalOrder {v}) using (sort; sort-↭)
+  open import Data.Permutation.Sort (decTotalOrder {v}) using (sorted-≋)
+  open import Data.List.Relation.Binary.Pointwise using (Pointwise; Pointwise-≡⇒≡; map)
+  open import Data.Product.Base using (_,_)
+  open import Data.Hypergraph.Label using (HypergraphLabel)
+  open HypergraphLabel GateLabel using (isCastable)
+  open import Data.Castable using (IsCastable)
+  open IsCastable isCastable using (≈-reflexive; ≈-sym; ≈-trans)
+  from-cong
+      : {H H′ : Hypergraph′ v}
+      → Hypergraph-same H H′
+      → ≈-Hypergraph (from H) (from H′)
+  from-cong {H} {H′} ≈H = record
+      { ≡sorted = ≡sorted
+      }
+    where
+      module H = Hypergraph′ H
+      module H′ = Hypergraph′ H′
+      open Hypergraph′
+      open Hypergraph-same ≈H using (↔h; ≗a; ≗l; ≗j; inverseˡ) renaming (from to f; to to t)
+      asEdge : (H : Hypergraph′ v) → Fin (h H) → Edge v
+      asEdge H e = record { label = l H e ; ports = toVec (j H e) }
+
+      to-from : (e : Fin H′.h) → t (f e) ≡ e
+      to-from e = inverseˡ ≡.refl
+
+      a∘to-from : (e : Fin H′.h) → H′.a (t (f e)) ≡ H′.a e
+      a∘to-from = ≡.cong H′.a ∘ to-from
+
+      ≗a′ : (e : Fin H′.h) → H.a (f e) ≡ H′.a e
+      ≗a′ e = ≡.trans (≗a (f e)) (a∘to-from e)
+
+      l≗ : (e : Fin H.h) → cast-gate (≗a e) (H.l e) ≡ H′.l (t e)
+      l≗ e = ≈-sym (≡.sym (≗l e))
+
+      l∘to-from : (e : Fin H′.h) → cast-gate (a∘to-from e) (H′.l (t (f e))) ≡ H′.l e
+      l∘to-from e rewrite to-from e = ≈-reflexive ≡.refl
+
+      ≗l′ : (e : Fin H′.h) → cast-gate (≗a′ e) (H.l (f e)) ≡ H′.l e
+      ≗l′ e = ≈-trans {H.a _} (l≗ (f e)) (l∘to-from e)
+
+      import Data.Vec.Relation.Binary.Equality.Cast as VecCast
+      open import Data.Vec using (cast) renaming (map to vecmap)
+      open import Data.Vec.Properties using (tabulate-cong; tabulate-∘; map-cast)
+
+      open import Data.Fin.Base using () renaming (cast to fincast)
+      open import Data.Fin.Properties using () renaming (cast-trans to fincast-trans; cast-is-id to fincast-is-id)
+
+      j∘to-from
+          : (e : Fin H′.h) (i : Fin (H′.a (t (f e))))
+          → H′.j (t (f e)) i
+          ≡ H′.j e (fincast (a∘to-from e) i)
+      j∘to-from e i rewrite to-from e = ≡.cong (H′.j e) (≡.sym (fincast-is-id ≡.refl i))
+
+      open ≡.≡-Reasoning
+
+      ≗j′ : (e : Fin H′.h) (i : Fin (H.a (f e))) → H.j (f e) i ≡ H′.j e (fincast (≗a′ e) i)
+      ≗j′ e i = begin
+          H.j (f e) i                                   ≡⟨ ≗j (f e) i ⟩
+          H′.j (t (f e)) (fincast _ i)                  ≡⟨ j∘to-from e (fincast _ i) ⟩
+          H′.j e (fincast (a∘to-from e) (fincast _ i))  ≡⟨ ≡.cong (H′.j e) (fincast-trans (≗a (f e)) _ i) ⟩
+          H′.j e (fincast (≗a′ e) i)                    ∎
+
+      cast-toVec
+          : {n m : ℕ}
+            {A : Set}
+            (m≡n : m ≡ n)
+            (f : Fin n → A)
+          → cast m≡n (toVec (f ∘ fincast m≡n)) ≡ toVec f
+      cast-toVec m≡n f rewrite m≡n = begin
+          cast _ (toVec (f ∘ (fincast _)))  ≡⟨ VecCast.cast-is-id ≡.refl (toVec (f ∘ fincast ≡.refl)) ⟩
+          toVec (f ∘ fincast _)             ≡⟨ tabulate-∘ f (fincast ≡.refl) ⟩
+          vecmap f (toVec (fincast _))      ≡⟨ ≡.cong (vecmap f) (tabulate-cong (fincast-is-id ≡.refl)) ⟩
+          vecmap f (toVec id)               ≡⟨ tabulate-∘ f id ⟨
+          toVec f                           ∎
+
+      ≗p′ : (e : Fin H′.h) → cast (≗a′ e) (toVec (H.j (f e))) ≡ toVec (H′.j e)
+      ≗p′ e = begin
+          cast (≗a′ e) (toVec (H.j (f e)))    ≡⟨ ≡.cong (cast (≗a′ e)) (tabulate-cong (≗j′ e)) ⟩
+          cast _ (toVec (H′.j e ∘ fincast _)) ≡⟨ cast-toVec (≗a′ e) (H′.j e) ⟩
+          toVec (H′.j e)                      ∎
+
+      H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (↔h ⟨$⟩ˡ e) ≡ asEdge H′ e
+      H∘ρ≗H′ e = ≈-Edge⇒≡ record
+          { ≡arity = ≗a′ e
+          ; ≡label = ≗l′ e
+          ; ≡ports = ≗p′ e
+          }
+
+      open Hypergraph using (edges)
+      open →-Reasoning
+      ≡sorted : sortHypergraph (from H) ≡ sortHypergraph (from H′)
+      ≡sorted =
+             flip ↔h , H∘ρ≗H′             ∶ asEdge H V.↭ asEdge H′
+          |> toList-↭                     ∶ toList (asEdge H) L.↭ toList (asEdge H′)
+          |> L.↭⇒↭ₛ′ ≈-Edge-IsEquivalence ∶ Permutation ≈-Edge (edges (from H)) (edges (from H′))
+          |> sorted-≋                     ∶ Pointwise ≈-Edge (sort (edges (from H))) (sort (edges (from H′)))
+          |> map ≈-Edge⇒≡                 ∶ Pointwise _≡_ (sort (edges (from H))) (sort (edges (from H′)))
+          |> Pointwise-≡⇒≡                ∶ sort (edges (from H)) ≡ sort (edges (from H′))
+          |> ≡.cong mkHypergraph          ∶ sortHypergraph (from H) ≡ sortHypergraph (from H′)
+
+equiv : (v : ℕ) → Equivalence (Hypergraph-Setoid v) (Hypergraph-Setoid′ v)
+equiv v = record
+    { to = to
+    ; from = from
+    ; to-cong = to-cong
+    ; from-cong = from-cong
+    }
diff --git a/Data/Circuit/Gate.agda b/Data/Circuit/Gate.agda
new file mode 100644
index 0000000..8ce7e0a
--- /dev/null
+++ b/Data/Circuit/Gate.agda
@@ -0,0 +1,137 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Circuit.Gate where
+
+open import Level using (0ℓ)
+open import Data.Castable using (Castable)
+open import Data.Hypergraph.Label using (HypergraphLabel)
+open import Data.String using (String)
+open import Data.Nat.Base using (ℕ; _≤_)
+open import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst; isEquivalence; cong)
+import Relation.Binary.PropositionalEquality as ≡
+
+import Data.Nat as Nat
+import Data.Fin as Fin
+
+data Gate : ℕ → Set where
+    ZERO  : Gate 1
+    ONE   : Gate 1
+    ID    : Gate 2
+    NOT   : Gate 2
+    AND   : Gate 3
+    OR    : Gate 3
+    XOR   : Gate 3
+    NAND  : Gate 3
+    NOR   : Gate 3
+    XNOR  : Gate 3
+
+cast-gate : {e e′ : ℕ} → .(e ≡ e′) → Gate e → Gate e′
+cast-gate {1} {1} eq g = g
+cast-gate {2} {2} eq g = g
+cast-gate {3} {3} eq g = g
+
+cast-gate-trans
+    : {m n o : ℕ}
+    → .(eq₁ : m ≡ n)
+      .(eq₂ : n ≡ o)
+      (g : Gate m)
+    → cast-gate eq₂ (cast-gate eq₁ g) ≡ cast-gate (trans eq₁ eq₂) g
+cast-gate-trans {1} {1} {1} eq₁ eq₂ g = refl
+cast-gate-trans {2} {2} {2} eq₁ eq₂ g = refl
+cast-gate-trans {3} {3} {3} eq₁ eq₂ g = refl
+
+cast-gate-is-id : {m : ℕ} .(eq : m ≡ m) (g : Gate m) → cast-gate eq g ≡ g
+cast-gate-is-id {1} eq g = refl
+cast-gate-is-id {2} eq g = refl
+cast-gate-is-id {3} eq g = refl
+
+subst-is-cast-gate : {m n : ℕ} (eq : m ≡ n) (g : Gate m) → subst Gate eq g ≡ cast-gate eq g
+subst-is-cast-gate refl g = sym (cast-gate-is-id refl g)
+
+GateCastable : Castable
+GateCastable = record
+    { B = Gate
+    ; isCastable = record
+        { cast = cast-gate
+        ; cast-trans = cast-gate-trans
+        ; cast-is-id = cast-gate-is-id
+        ; subst-is-cast = subst-is-cast-gate
+        }
+    }
+
+showGate : (n : ℕ) → Gate n → String
+showGate _ ZERO = "ZERO"
+showGate _ ONE  = "ONE"
+showGate _ ID   = "ID"
+showGate _ NOT  = "NOT"
+showGate _ AND  = "AND"
+showGate _ OR   = "OR"
+showGate _ XOR  = "XOR"
+showGate _ NAND = "NAND"
+showGate _ NOR  = "NOR"
+showGate _ XNOR = "XNOR"
+
+toℕ : (n : ℕ) → Gate n → ℕ
+toℕ 1 ZERO = 0
+toℕ 1 ONE = 1
+toℕ 2 ID = 0
+toℕ 2 NOT = 1
+toℕ 3 AND = 0
+toℕ 3 OR = 1
+toℕ 3 XOR = 2
+toℕ 3 NAND = 3
+toℕ 3 NOR = 4
+toℕ 3 XNOR = 5
+
+toℕ-injective : {n : ℕ} {x y : Gate n} → toℕ n x ≡ toℕ n y → x ≡ y
+toℕ-injective {1} {ZERO} {ZERO} refl = refl
+toℕ-injective {1} {ONE} {ONE} refl = refl
+toℕ-injective {2} {ID} {ID} refl = refl
+toℕ-injective {2} {NOT} {NOT} refl = refl
+toℕ-injective {3} {AND} {AND} refl = refl
+toℕ-injective {3} {OR} {OR} refl = refl
+toℕ-injective {3} {XOR} {XOR} refl = refl
+toℕ-injective {3} {NAND} {NAND} refl = refl
+toℕ-injective {3} {NOR} {NOR} refl = refl
+toℕ-injective {3} {XNOR} {XNOR} refl = refl
+
+open import Relation.Binary using (Rel; Decidable; DecidableEquality)
+import Relation.Nullary.Decidable as Dec
+
+_[_≤_] : (n : ℕ) → Rel (Gate n) 0ℓ
+_[_≤_] n x y = toℕ n x ≤ toℕ n y
+
+_≟_ : {n : ℕ} → DecidableEquality (Gate n)
+_≟_ {n} x y = Dec.map′ toℕ-injective (cong (toℕ n)) (toℕ n x Nat.≟ toℕ n y)
+
+_≤?_ : {n : ℕ} → Decidable (n [_≤_])
+_≤?_ {n} x y = toℕ n x Nat.≤? toℕ n y
+
+GateLabel : HypergraphLabel
+GateLabel = record
+    { Label = Gate
+    ; showLabel = showGate
+    ; isCastable = record
+        { cast = cast-gate
+        ; cast-trans = cast-gate-trans
+        ; cast-is-id = cast-gate-is-id
+        ; subst-is-cast = subst-is-cast-gate
+        }
+    ; _[_≤_] = λ n x y → toℕ n x ≤ toℕ n y
+    ; isDecTotalOrder = λ n → record
+        { isTotalOrder = record
+          { isPartialOrder = record
+              { isPreorder = record
+                  { isEquivalence = isEquivalence
+                  ; reflexive = λ { refl → ≤-refl }
+                  ; trans = ≤-trans
+                  }
+              ; antisym = λ i≤j j≤i → toℕ-injective (≤-antisym i≤j j≤i)
+              }
+          ; total = λ { x y → ≤-total (toℕ n x) (toℕ n y) }
+          }
+        ; _≟_ = _≟_
+        ; _≤?_ = _≤?_
+        }
+    }
diff --git a/Data/Circuit/Typecheck.agda b/Data/Circuit/Typecheck.agda
new file mode 100644
index 0000000..e34ea44
--- /dev/null
+++ b/Data/Circuit/Typecheck.agda
@@ -0,0 +1,78 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Circuit.Typecheck where
+
+open import Data.SExp using (SExp)
+open import Data.Circuit.Gate using (GateLabel; Gate)
+open import Data.Hypergraph.Label using (HypergraphLabel)
+open import Data.Hypergraph.Edge GateLabel using (Edge)
+open import Data.Hypergraph.Base GateLabel using (Hypergraph)
+
+open import Data.List using (List; length) renaming (map to mapL)
+open import Data.List.Effectful using () renaming (module TraversableA to ListTraversable)
+open import Data.Maybe using (Maybe) renaming (map to mapM)
+open import Data.Nat using (ℕ; _<?_; _≟_)
+open import Data.String using (String)
+open import Data.Product using (_×_; _,_; Σ)
+open import Data.Vec using (Vec; []; _∷_; fromList) renaming (map to mapV)
+open import Data.Vec.Effectful using () renaming (module TraversableA to VecTraversable)
+open import Data.Maybe.Effectful using (applicative)
+open import Data.Fin using (Fin; #_; fromℕ<)
+open import Level using (0ℓ)
+
+import Relation.Binary.PropositionalEquality as ≡
+
+open List
+open SExp
+open Gate
+open Maybe
+
+gate : {n a : ℕ} (g : Gate a) → Vec (Fin n) a → Edge n
+gate g p = record { label = g; ports = p }
+
+typeCheckGateLabel : SExp → Maybe (Σ ℕ Gate)
+typeCheckGateLabel (Atom "one")  = just (1 , ONE)
+typeCheckGateLabel (Atom "zero") = just (1 , ZERO)
+typeCheckGateLabel (Atom "not")  = just (2 , NOT)
+typeCheckGateLabel (Atom "id")   = just (2 , ID)
+typeCheckGateLabel (Atom "and")  = just (3 , AND)
+typeCheckGateLabel (Atom "or")   = just (3 , OR)
+typeCheckGateLabel (Atom "xor")  = just (3 , XOR)
+typeCheckGateLabel (Atom "nand") = just (3 , NAND)
+typeCheckGateLabel (Atom "nor")  = just (3 , NOR)
+typeCheckGateLabel (Atom "xnor") = just (3 , XNOR)
+typeCheckGateLabel _ = nothing
+
+open import Relation.Nullary.Decidable using (Dec; yes; no)
+open Dec
+open VecTraversable {0ℓ} applicative using () renaming (sequenceA to vecSequenceA)
+open ListTraversable {0ℓ} applicative using () renaming (sequenceA to listSequenceA)
+
+typeCheckPort : (v : ℕ) → SExp → Maybe (Fin v)
+typeCheckPort v (Nat n) with n <? v
+... | yes n<v = just (fromℕ< n<v)
+... | no _ = nothing
+typeCheckPort _ _ = nothing
+
+typeCheckPorts : (v n : ℕ) → List SExp → Maybe (Vec (Fin v) n)
+typeCheckPorts v n xs with length xs ≟ n
+... | yes ≡.refl = vecSequenceA (mapV (typeCheckPort v) (fromList xs))
+... | no _ = nothing
+
+typeCheckGate : (v : ℕ) → SExp → Maybe (Edge v)
+typeCheckGate v (SExps (labelString ∷ ports)) with typeCheckGateLabel labelString
+... | just (n , label) = mapM (gate label) (typeCheckPorts v n ports)
+... | nothing = nothing
+typeCheckGate v _ = nothing
+
+typeCheckHeader : SExp → Maybe ℕ
+typeCheckHeader (SExps (Atom "hypergraph" ∷ Nat n ∷ [])) = just n
+typeCheckHeader _ = nothing
+
+typeCheckHypergraph : SExp → Maybe (Σ ℕ Hypergraph)
+typeCheckHypergraph (SExps (x ∷ xs)) with typeCheckHeader x
+... | nothing = nothing
+... | just n with listSequenceA (mapL (typeCheckGate n) xs)
+...   | just e = just (n , record { edges = e })
+...   | nothing = nothing
+typeCheckHypergraph _ = nothing
diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
new file mode 100644
index 0000000..6988cf0
--- /dev/null
+++ b/Data/Hypergraph/Base.agda
@@ -0,0 +1,26 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+
+module Data.Hypergraph.Base (HL : HypergraphLabel) where
+
+open import Data.Hypergraph.Edge HL using (Edge; decTotalOrder; showEdge)
+open import Data.List.Base using (List; map)
+open import Data.Nat.Base using (ℕ)
+open import Data.String using (String; unlines)
+
+import Data.List.Sort as Sort
+
+record Hypergraph (v : ℕ) : Set where
+  constructor mkHypergraph
+  field
+    edges : List (Edge v)
+
+sortHypergraph : {v : ℕ} → Hypergraph v → Hypergraph v
+sortHypergraph {v} H = record { edges = sort edges }
+  where
+    open Hypergraph H
+    open Sort decTotalOrder using (sort)
+
+showHypergraph : {v : ℕ} → Hypergraph v → String
+showHypergraph record { edges = e} = unlines (map showEdge e)
diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
new file mode 100644
index 0000000..13b9278
--- /dev/null
+++ b/Data/Hypergraph/Edge.agda
@@ -0,0 +1,335 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+
+module Data.Hypergraph.Edge (HL : HypergraphLabel) where
+
+
+open import Relation.Binary using (Rel; IsStrictTotalOrder; Tri; Trichotomous; _Respects_)
+open import Data.Castable using (IsCastable)
+open import Data.Fin using (Fin)
+open import Data.Fin.Show using () renaming (show to showFin)
+open import Data.Nat.Base using (ℕ; _<_)
+open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Data.String using (String; _<+>_)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡; Pointwise-≡⇒≡)
+open import Data.Vec.Show using () renaming (show to showVec)
+open import Level using (0ℓ)
+open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Nullary using (¬_)
+
+import Data.Fin.Base as Fin
+import Data.Fin.Properties as FinProp
+import Data.Vec.Base as VecBase
+import Data.Vec.Relation.Binary.Equality.Cast as VecCast
+import Data.Vec.Relation.Binary.Lex.Strict as Lex
+import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.Properties.DecTotalOrder as DTOP
+import Relation.Binary.Properties.StrictTotalOrder as STOP
+
+module HL = HypergraphLabel HL
+open HL using (Label; cast; cast-is-id)
+open VecBase using (Vec)
+
+record Edge (v : ℕ) : Set where
+  field
+    {arity} : ℕ
+    label : Label arity
+    ports : Vec (Fin v) arity
+
+open ≡ using (_≡_)
+open VecCast using (_≈[_]_)
+
+record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where
+  module E = Edge E
+  module E′ = Edge E′
+  field
+    ≡arity : E.arity ≡ E′.arity
+    ≡label : cast ≡arity E.label ≡ E′.label
+    ≡ports : E.ports ≈[ ≡arity ] E′.ports
+
+≈-Edge-refl : {v : ℕ} {x : Edge v} → ≈-Edge x x
+≈-Edge-refl {_} {x} = record
+    { ≡arity = ≡.refl
+    ; ≡label = HL.≈-reflexive ≡.refl
+    ; ≡ports = VecCast.≈-reflexive ≡.refl
+    }
+  where
+    open Edge x using (arity; label)
+    open DecTotalOrder (HL.decTotalOrder arity) using (module Eq)
+
+≈-Edge-sym : {v : ℕ} {x y : Edge v} → ≈-Edge x y → ≈-Edge y x
+≈-Edge-sym {_} {x} {y} x≈y = record
+    { ≡arity = ≡.sym ≡arity
+    ; ≡label = HL.≈-sym ≡label
+    ; ≡ports = VecCast.≈-sym ≡ports
+    }
+  where
+    open ≈-Edge x≈y
+    open DecTotalOrder (HL.decTotalOrder E.arity) using (module Eq)
+
+≈-Edge-trans : {v : ℕ} {i j k : Edge v} → ≈-Edge i j → ≈-Edge j k → ≈-Edge i k
+≈-Edge-trans {_} {i} {j} {k} i≈j j≈k = record
+    { ≡arity = ≡.trans i≈j.≡arity j≈k.≡arity
+    ; ≡label = HL.≈-trans i≈j.≡label j≈k.≡label
+    ; ≡ports = VecCast.≈-trans i≈j.≡ports j≈k.≡ports
+    }
+  where
+    module i≈j = ≈-Edge i≈j
+    module j≈k = ≈-Edge j≈k
+
+open import Relation.Binary using (IsEquivalence)
+≈-Edge-IsEquivalence : {v : ℕ} → IsEquivalence (≈-Edge {v})
+≈-Edge-IsEquivalence = record
+    { refl = ≈-Edge-refl
+    ; sym = ≈-Edge-sym
+    ; trans = ≈-Edge-trans
+    }
+
+open HL using (_[_<_])
+_<<_ : {v a : ℕ} → Rel (Vec (Fin v) a) 0ℓ
+_<<_ {v} = Lex.Lex-< _≡_ (Fin._<_ {v})
+data <-Edge {v : ℕ} : Edge v → Edge v → Set where
+  <-arity
+      : {x y : Edge v}
+      → Edge.arity x < Edge.arity y
+      → <-Edge x y
+  <-label
+      : {x y : Edge v}
+        (≡a : Edge.arity x ≡ Edge.arity y)
+      → Edge.arity y [ cast ≡a (Edge.label x) < Edge.label y ]
+      → <-Edge x y
+  <-ports
+      : {x y : Edge v}
+        (≡a : Edge.arity x ≡ Edge.arity y)
+        (≡l : Edge.label x HL.≈[ ≡a ] Edge.label y)
+      → VecBase.cast ≡a (Edge.ports x) << Edge.ports y
+      → <-Edge x y
+
+<-Edge-irrefl : {v : ℕ} {x y : Edge v} → ≈-Edge x y → ¬ <-Edge x y
+<-Edge-irrefl record { ≡arity = ≡a } (<-arity n<m) = <-irrefl ≡a n<m
+<-Edge-irrefl record { ≡label = ≡l } (<-label _ (_ , x≉y)) = x≉y ≡l
+<-Edge-irrefl record { ≡ports = ≡p } (<-ports ≡.refl ≡l x<y)
+    = Lex.<-irrefl FinProp.<-irrefl (≡⇒Pointwise-≡ ≡p) x<y
+
+<-Edge-trans : {v : ℕ} {i j k : Edge v} → <-Edge i j → <-Edge j k → <-Edge i k
+<-Edge-trans (<-arity i<j) (<-arity j<k) = <-arity (<-trans i<j j<k)
+<-Edge-trans (<-arity i<j) (<-label ≡.refl j<k) = <-arity i<j
+<-Edge-trans (<-arity i<j) (<-ports ≡.refl _ j<k) = <-arity i<j
+<-Edge-trans (<-label ≡.refl i<j) (<-arity j<k) = <-arity j<k
+<-Edge-trans {_} {i} (<-label ≡.refl i<j) (<-label ≡.refl j<k)
+    = <-label ≡.refl (<-label-trans i<j (<-respˡ-≈ (HL.≈-reflexive ≡.refl) j<k))
+  where
+    open DTOP (HL.decTotalOrder (Edge.arity i)) using (<-respˡ-≈) renaming (<-trans to <-label-trans)
+<-Edge-trans {k = k} (<-label ≡.refl i<j) (<-ports ≡.refl ≡.refl _)
+    = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) i<j)
+  where
+    open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respʳ-≈)
+<-Edge-trans (<-ports ≡.refl _ _) (<-arity j<k) = <-arity j<k
+<-Edge-trans {k = k} (<-ports ≡.refl ≡.refl _) (<-label ≡.refl j<k)
+    = <-label ≡.refl (<-respˡ-≈ (≡.cong (cast _) (HL.≈-reflexive ≡.refl)) j<k)
+  where
+    open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respˡ-≈)
+<-Edge-trans {j = j} (<-ports ≡.refl ≡l₁ i<j) (<-ports ≡.refl ≡l₂ j<k)
+  rewrite (VecCast.cast-is-id ≡.refl (Edge.ports j))
+    = <-ports ≡.refl
+        (HL.≈-trans ≡l₁ ≡l₂)
+        (Lex.<-trans ≡-isPartialEquivalence FinProp.<-resp₂-≡ FinProp.<-trans i<j j<k)
+  where
+    open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+
+<-Edge-respˡ-≈ : {v : ℕ} {y : Edge v} → (λ x → <-Edge x y) Respects ≈-Edge
+<-Edge-respˡ-≈ ≈x (<-arity x₁<y) = <-arity (proj₂ <-resp₂-≡ ≡arity x₁<y)
+  where
+    open ≈-Edge ≈x using (≡arity)
+<-Edge-respˡ-≈ {_} {y} record { ≡arity = ≡.refl ; ≡label = ≡.refl } (<-label ≡.refl x₁<y)
+    = <-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x₁<y)
+  where
+    module y = Edge y
+    open DTOP (HL.decTotalOrder y.arity) using (<-respˡ-≈)
+<-Edge-respˡ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x₁<y)
+    = <-ports
+        ≡.refl
+        (≡.cong (cast _) (HL.≈-reflexive ≡.refl))
+        (Lex.<-respectsˡ
+            ≡-isPartialEquivalence
+            FinProp.<-respˡ-≡
+            (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
+            x₁<y)
+  where
+    open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+
+<-Edge-respʳ-≈ : {v : ℕ} {x : Edge v} → <-Edge x Respects ≈-Edge
+<-Edge-respʳ-≈ record { ≡arity = ≡a } (<-arity x<y₁) = <-arity (proj₁ <-resp₂-≡ ≡a x<y₁)
+<-Edge-respʳ-≈ {_} {x} record { ≡arity = ≡.refl ; ≡label = ≡.refl } (<-label ≡.refl x<y₁)
+    = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x<y₁)
+  where
+    module x = Edge x
+    open DTOP (HL.decTotalOrder x.arity) using (<-respʳ-≈)
+<-Edge-respʳ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x<y₁)
+    = <-ports
+        ≡.refl
+        (≡.cong (cast _) (≡.sym (HL.≈-reflexive ≡.refl)))
+        (Lex.<-respectsʳ
+            ≡-isPartialEquivalence
+            FinProp.<-respʳ-≡
+            (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
+            x<y₁)
+  where
+    open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+
+open Tri
+open ≈-Edge
+tri : {v : ℕ} → Trichotomous (≈-Edge {v}) (<-Edge {v})
+tri x y with <-cmp x.arity y.arity
+  where
+    module x = Edge x
+    module y = Edge y
+tri x y | tri< x<y x≢y y≮x = tri< (<-arity x<y) (λ x≡y → x≢y (≡arity x≡y)) ¬y<x
+  where
+    ¬y<x :  ¬ <-Edge y x
+    ¬y<x (<-arity y<x) = y≮x y<x
+    ¬y<x (<-label ≡a _) = x≢y (≡.sym ≡a)
+    ¬y<x (<-ports ≡a _ _) = x≢y (≡.sym ≡a)
+tri x y | tri≈ x≮y ≡.refl y≮x = compare-label
+  where
+    module x = Edge x
+    module y = Edge y
+    open StrictTotalOrder (HL.strictTotalOrder x.arity) using (compare)
+    import Relation.Binary.Properties.DecTotalOrder
+    open DTOP (HL.decTotalOrder x.arity) using (<-respˡ-≈)
+    compare-label : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x)
+    compare-label with compare x.label y.label
+    ... | tri< x<y x≢y y≮x′ = tri<
+            (<-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x<y))
+            (λ x≡y → x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) (≡label x≡y)))
+            ¬y<x
+      where
+        ¬y<x :  ¬ <-Edge y x
+        ¬y<x (<-arity y<x) = y≮x y<x
+        ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
+        ¬y<x (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym ≡l) (cast-is-id ≡.refl y.label))
+    ... | tri≈ x≮y′ x≡y′ y≮x′ = compare-ports
+      where
+        compare-ports : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x)
+        compare-ports with Lex.<-cmp ≡.sym FinProp.<-cmp x.ports y.ports
+        ... | tri< x<y x≢y y≮x″ =
+                tri<
+                  (<-ports ≡.refl
+                    (HL.≈-reflexive x≡y′)
+                    (Lex.<-respectsˡ
+                      ≡-isPartialEquivalence
+                      FinProp.<-respˡ-≡
+                      (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
+                      x<y))
+                  (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y))))
+                  ¬y<x
+          where
+            open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+            ¬y<x :  ¬ <-Edge y x
+            ¬y<x (<-arity y<x) = y≮x y<x
+            ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
+            ¬y<x (<-ports _ _ y<x) =
+                y≮x″
+                  (Lex.<-respectsˡ
+                    ≡-isPartialEquivalence
+                    FinProp.<-respˡ-≡
+                    (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
+                    y<x)
+        ... | tri≈ x≮y″ x≡y″ y≮x″ = tri≈
+                ¬x<y
+                (record { ≡arity = ≡.refl ; ≡label = HL.≈-reflexive x≡y′ ; ≡ports = VecCast.≈-reflexive (Pointwise-≡⇒≡ x≡y″) })
+                ¬y<x
+          where
+            open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+            ¬x<y : ¬ <-Edge x y
+            ¬x<y (<-arity x<y) = x≮y x<y
+            ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
+            ¬x<y (<-ports _ _ x<y) =
+                x≮y″
+                  (Lex.<-respectsˡ
+                    ≡-isPartialEquivalence
+                    FinProp.<-respˡ-≡
+                    (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
+                    x<y)
+            ¬y<x : ¬ <-Edge y x
+            ¬y<x (<-arity y<x) = y≮x y<x
+            ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
+            ¬y<x (<-ports _ _ y<x) =
+                y≮x″
+                  (Lex.<-respectsˡ
+                    ≡-isPartialEquivalence
+                    FinProp.<-respˡ-≡
+                    (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
+                    y<x)
+
+        ... | tri> x≮y″ x≢y y<x =
+                tri>
+                  ¬x<y
+                  (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y))))
+                  (<-ports
+                    ≡.refl
+                    (HL.≈-sym (HL.≈-reflexive x≡y′))
+                    (Lex.<-respectsˡ
+                      ≡-isPartialEquivalence
+                      FinProp.<-respˡ-≡
+                      (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
+                      y<x))
+          where
+            open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+            ¬x<y : ¬ <-Edge x y
+            ¬x<y (<-arity x<y) = x≮y x<y
+            ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
+            ¬x<y (<-ports _ _ x<y) =
+                x≮y″
+                  (Lex.<-respectsˡ
+                    ≡-isPartialEquivalence
+                    FinProp.<-respˡ-≡
+                    (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
+                    x<y)
+    ... | tri> x≮y′ x≢y y<x = tri>
+            ¬x<y
+            (λ x≡y → x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) (≡label x≡y)))
+            (<-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) y<x))
+      where
+        ¬x<y : ¬ <-Edge x y
+        ¬x<y (<-arity x<y) = x≮y x<y
+        ¬x<y (<-label ≡a x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
+        ¬x<y (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) ≡l)
+tri x y | tri> x≮y x≢y y<x = tri> ¬x<y (λ x≡y → x≢y (≡arity x≡y)) (<-arity y<x)
+  where
+    ¬x<y :  ¬ <-Edge x y
+    ¬x<y (<-arity x<y) = x≮y x<y
+    ¬x<y (<-label ≡a x<y) = x≢y ≡a
+    ¬x<y (<-ports ≡a _ _) = x≢y ≡a
+
+isStrictTotalOrder : {v : ℕ} → IsStrictTotalOrder (≈-Edge {v}) (<-Edge {v})
+isStrictTotalOrder = record
+    { isStrictPartialOrder = record
+        { isEquivalence = ≈-Edge-IsEquivalence
+        ; irrefl = <-Edge-irrefl
+        ; trans = <-Edge-trans
+        ; <-resp-≈ = <-Edge-respʳ-≈ , <-Edge-respˡ-≈
+        }
+    ; compare = tri
+    }
+
+strictTotalOrder : {v : ℕ} → StrictTotalOrder 0ℓ 0ℓ 0ℓ
+strictTotalOrder {v} = record
+    { Carrier = Edge v
+    ; _≈_ = ≈-Edge {v}
+    ; _<_ = <-Edge {v}
+    ; isStrictTotalOrder = isStrictTotalOrder {v}
+    }
+
+showEdge : {v : ℕ} → Edge v → String
+showEdge record { arity = a ; label = l ; ports = p} = HL.showLabel a l <+> showVec showFin p
+
+open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) public
+
+≈-Edge⇒≡ : {v : ℕ} {x y : Edge v} → ≈-Edge x y → x ≡ y
+≈-Edge⇒≡ {v} {record { label = l ; ports = p }} record { ≡arity = ≡.refl ; ≡label = ≡.refl ; ≡ports = ≡.refl }
+  rewrite cast-is-id ≡.refl l
+  rewrite VecCast.cast-is-id ≡.refl p = ≡.refl
diff --git a/Data/Hypergraph/Label.agda b/Data/Hypergraph/Label.agda
new file mode 100644
index 0000000..c23d33a
--- /dev/null
+++ b/Data/Hypergraph/Label.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --without-K --safe #-}
+module Data.Hypergraph.Label where
+
+open import Data.Castable using (IsCastable)
+open import Data.Nat.Base using (ℕ)
+open import Data.String using (String)
+open import Level using (Level; suc)
+open import Relation.Binary using (Rel; IsDecTotalOrder)
+open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
+open import Relation.Binary.Properties.DecTotalOrder using (<-strictTotalOrder; _<_)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+
+record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
+
+  field
+    Label : ℕ → Set ℓ
+    showLabel : (n : ℕ) → Label n → String
+    isCastable : IsCastable Label
+    _[_≤_] : (n : ℕ) → Rel (Label n) ℓ
+    isDecTotalOrder : (n : ℕ) → IsDecTotalOrder _≡_ (n [_≤_])
+
+  decTotalOrder : (n : ℕ) → DecTotalOrder ℓ ℓ ℓ
+  decTotalOrder n = record
+      { Carrier = Label n
+      ; _≈_ = _≡_
+      ; _≤_ = n [_≤_]
+      ; isDecTotalOrder = isDecTotalOrder n
+      }
+
+  _[_<_] : (n : ℕ) → Rel (Label n) ℓ
+  _[_<_] n =  _<_ (decTotalOrder n)
+
+  strictTotalOrder : (n : ℕ) → StrictTotalOrder ℓ ℓ ℓ
+  strictTotalOrder n = <-strictTotalOrder (decTotalOrder n)
+
+  open IsCastable isCastable public
diff --git a/Data/Hypergraph/Setoid.agda b/Data/Hypergraph/Setoid.agda
new file mode 100644
index 0000000..c39977d
--- /dev/null
+++ b/Data/Hypergraph/Setoid.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+
+module Data.Hypergraph.Setoid (HL : HypergraphLabel) where
+
+open import Data.Hypergraph.Edge HL using (decTotalOrder)
+open import Data.Hypergraph.Base HL using (Hypergraph; sortHypergraph)
+open import Data.Nat.Base using (ℕ)
+open import Level using (0ℓ)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+record ≈-Hypergraph {v : ℕ} (H H′ : Hypergraph v) : Set where
+  module H = Hypergraph H
+  module H′ = Hypergraph H′
+  field
+    ≡sorted : sortHypergraph H ≡ sortHypergraph H′
+  open Hypergraph using (edges)
+  ≡edges : edges (sortHypergraph H) ≡ edges (sortHypergraph H′)
+  ≡edges = ≡.cong edges ≡sorted
+  open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-reflexive; ↭-sym; ↭-trans)
+  open import Data.List.Sort decTotalOrder using (sort-↭)
+  ↭edges : H.edges ↭ H′.edges
+  ↭edges = ↭-trans (↭-sym (sort-↭ H.edges)) (↭-trans (↭-reflexive ≡edges) (sort-↭ H′.edges))
+
+≈-refl : {v : ℕ} {H : Hypergraph v} → ≈-Hypergraph H H
+≈-refl = record { ≡sorted = ≡.refl }
+
+≈-sym : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → ≈-Hypergraph H′ H
+≈-sym ≈H = record { ≡sorted = ≡.sym ≡sorted }
+  where
+    open ≈-Hypergraph ≈H 
+
+≈-trans : {v : ℕ} {H H′ H″ : Hypergraph v} → ≈-Hypergraph H H′ → ≈-Hypergraph H′ H″ → ≈-Hypergraph H H″
+≈-trans ≈H₁ ≈H₂ = record { ≡sorted = ≡.trans ≈H₁.≡sorted ≈H₂.≡sorted }
+  where
+    module ≈H₁ = ≈-Hypergraph ≈H₁
+    module ≈H₂ = ≈-Hypergraph ≈H₂
+
+Hypergraph-Setoid : (v : ℕ) → Setoid 0ℓ 0ℓ
+Hypergraph-Setoid v = record
+    { Carrier = Hypergraph v
+    ; _≈_ = ≈-Hypergraph
+    ; isEquivalence = record
+        { refl = ≈-refl
+        ; sym = ≈-sym
+        ; trans = ≈-trans
+        }
+    }
diff --git a/Data/Permutation.agda b/Data/Permutation.agda
new file mode 100644
index 0000000..55c8748
--- /dev/null
+++ b/Data/Permutation.agda
@@ -0,0 +1,217 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Data.Permutation {ℓ : Level} {A : Set ℓ} where
+
+import Data.Fin as Fin
+import Data.Fin.Properties as FinProp
+import Data.Fin.Permutation as ↔-Fin
+import Data.List as List
+import Data.List.Properties as ListProp
+import Data.List.Relation.Binary.Permutation.Propositional as ↭-List
+import Data.Nat as Nat
+import Data.Vec.Functional as Vector
+import Data.Vec.Functional.Properties as VectorProp
+import Data.Vec.Functional.Relation.Binary.Permutation as ↭-Vec
+import Data.Vec.Functional.Relation.Binary.Permutation.Properties as ↭-VecProp
+
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Data.Vec.Functional.Relation.Unary.Any using (Any)
+open import Function.Base using (_∘_)
+
+open ↭-Vec using () renaming (_↭_ to _↭′_)
+open ↭-List using (_↭_; ↭-sym; module PermutationReasoning)
+open ↔-Fin using (Permutation; _⟨$⟩ˡ_; _⟨$⟩ʳ_)
+open List using (List) hiding (module List)
+open Fin using (Fin; cast) hiding (module Fin)
+open Vector using (Vector; toList; fromList)
+open Fin.Fin
+open Nat using (ℕ; zero; suc)
+open _↭_
+
+module _ where
+
+  open Fin using (#_)
+  open ↔-Fin using (lift₀; insert)
+  open ↭-VecProp using (↭-refl; ↭-trans)
+
+  -- convert a List permutation to a Vector permutation
+  fromList-↭
+      : {xs ys : List A}
+      → xs ↭ ys
+      → fromList xs ↭′ fromList ys
+  fromList-↭ refl = ↭-refl
+  fromList-↭ (prep _ xs↭ys)
+    with n↔m , xs↭ys′ ← fromList-↭ xs↭ys = lift₀ n↔m , λ where
+      zero → ≡.refl
+      (suc i) → xs↭ys′ i
+  fromList-↭ (swap x y xs↭ys)
+    with n↔m , xs↭ys′ ← fromList-↭ xs↭ys = insert (# 0) (# 1) (lift₀ n↔m) , λ where
+      zero → ≡.refl
+      (suc zero) → ≡.refl
+      (suc (suc i)) → xs↭ys′ i
+  fromList-↭ (trans {xs} xs↭ys ys↭zs) =
+      ↭-trans {_} {_} {_} {i = fromList xs} (fromList-↭ xs↭ys) (fromList-↭ ys↭zs)
+
+-- witness for an element in a Vector
+_∈_ : A → {n : ℕ} → Vector A n → Set ℓ
+x ∈ xs = Any (x ≡_) xs
+
+-- apply a permutation to a witness
+apply
+    : {n m : ℕ}
+      {xs : Vector A n}
+      {ys : Vector A m}
+      {x : A}
+    → (xs↭ys : xs ↭′ ys)
+    → x ∈ xs
+    → x ∈ ys
+apply {suc n} {zero} (↔n , _) (i , _) with () ← ↔n ⟨$⟩ˡ i
+apply {suc n} {suc m} {xs} {ys} {x} (↔n , ↔≗) (i , x≡xs-i) = i′ , x≡ys-i′
+  where
+    i′ : Fin (suc m)
+    i′ = ↔n ⟨$⟩ˡ i
+    open ≡.≡-Reasoning
+    x≡ys-i′ : x ≡ ys i′
+    x≡ys-i′ = begin
+      x                         ≡⟨ x≡xs-i ⟩
+      xs i                      ≡⟨ ≡.cong xs (↔-Fin.inverseʳ ↔n) ⟨
+      xs (↔n ⟨$⟩ʳ (↔n ⟨$⟩ˡ i))  ≡⟨⟩
+      xs (↔n ⟨$⟩ʳ i′)           ≡⟨ ↔≗ i′ ⟩
+      ys i′                     ∎
+
+-- remove an element from a Vector
+remove : {n : ℕ} {x : A} (xs : Vector A (suc n)) → x ∈ xs → Vector A n
+remove xs (i , _) = Vector.removeAt xs i
+
+-- remove an element and its image from a permutation
+↭-remove
+    : {n m : ℕ}
+      {xs : Vector A (suc n)}
+      {ys : Vector A (suc m)}
+      {x : A}
+    → (xs↭ys : xs ↭′ ys)
+    → (x∈xs : x ∈ xs)
+    → let x∈ys = apply xs↭ys x∈xs in
+      remove xs x∈xs ↭′ remove ys x∈ys
+↭-remove {n} {m} {xs} {ys} {x} xs↭ys@(ρ , ↔≗) x∈xs@(k , _) = ρ⁻ , ↔≗⁻
+  where
+    k′ : Fin (suc m)
+    k′ = ρ ⟨$⟩ˡ k
+    x∈ys : x ∈ ys
+    x∈ys = apply xs↭ys x∈xs
+    ρ⁻ : Permutation m n
+    ρ⁻ = ↔-Fin.remove k′ ρ
+    xs⁻ : Vector A n
+    xs⁻ = remove xs x∈xs
+    ys⁻ : Vector A m
+    ys⁻ = remove ys x∈ys
+    open ≡.≡-Reasoning
+    open Fin using (punchIn)
+    ↔≗⁻ : (i : Fin m) → xs⁻ (ρ⁻ ⟨$⟩ʳ i) ≡ ys⁻ i
+    ↔≗⁻ i = begin
+        xs⁻ (ρ⁻ ⟨$⟩ʳ i)             ≡⟨⟩
+        remove xs x∈xs (ρ⁻ ⟨$⟩ʳ i)  ≡⟨⟩
+        xs (punchIn k (ρ⁻ ⟨$⟩ʳ i))  ≡⟨ ≡.cong xs (↔-Fin.punchIn-permute′ ρ k i) ⟨
+        xs (ρ ⟨$⟩ʳ (punchIn k′ i))  ≡⟨ ↔≗ (punchIn k′ i) ⟩
+        ys (punchIn k′ i)           ≡⟨⟩
+        remove ys x∈ys i            ≡⟨⟩
+        ys⁻ i                       ∎
+
+open List.List
+open List using (length; insertAt)
+
+-- build a permutation which moves the first element of a list to an arbitrary position
+↭-insert-half
+    : {x₀ : A}
+      {xs : List A}
+    → (i : Fin (suc (length xs)))
+    → x₀ ∷ xs ↭ insertAt xs i x₀
+↭-insert-half zero = refl
+↭-insert-half {x₀} {x₁ ∷ xs} (suc i) = trans (swap x₀ x₁ refl) (prep x₁ (↭-insert-half i))
+
+-- add a mapping to a permutation, given a value and its start and end positions
+↭-insert
+    : {xs ys : List A}
+    → xs ↭ ys
+    → (i : Fin (suc (length xs)))
+      (j : Fin (suc (length ys)))
+      (x : A)
+    → insertAt xs i x ↭ insertAt ys j x
+↭-insert {xs} {ys} xs↭ys i j x = xs↭ys⁺
+  where
+    open PermutationReasoning
+    xs↭ys⁺ : insertAt xs i x ↭ insertAt ys j x
+    xs↭ys⁺ = begin
+      insertAt xs i x ↭⟨ ↭-insert-half i ⟨
+      x ∷ xs          <⟨ xs↭ys ⟩
+      x ∷ ys          ↭⟨ ↭-insert-half j ⟩
+      insertAt ys j x ∎
+
+open ListProp using (length-tabulate; tabulate-cong)
+insertAt-toList
+    : {n : ℕ}
+      {v : Vector A n}
+      (i : Fin (suc (length (toList v))))
+      (i′ : Fin (suc n))
+    → i ≡ cast (≡.cong suc (≡.sym (length-tabulate v))) i′
+    → (x : A)
+    → insertAt (toList v) i x
+    ≡ toList (Vector.insertAt v i′ x)
+insertAt-toList zero zero _ x = ≡.refl
+insertAt-toList {suc n} {v} (suc i) (suc i′) ≡.refl x =
+    ≡.cong (v zero ∷_) (insertAt-toList i i′ ≡.refl x)
+
+-- convert a Vector permutation to a List permutation
+toList-↭
+    : {n m : ℕ}
+      {xs : Vector A n}
+      {ys : Vector A m}
+    → xs ↭′ ys
+    → toList xs ↭ toList ys
+toList-↭ {zero} {zero} _ = refl
+toList-↭ {zero} {suc m} (ρ , _) with () ← ρ ⟨$⟩ʳ zero
+toList-↭ {suc n} {zero} (ρ , _) with () ← ρ ⟨$⟩ˡ zero
+toList-↭ {suc n} {suc m} {xs} {ys} xs↭ys′ = xs↭ys
+  where
+    -- first element and its image
+    x₀ : A
+    x₀ = xs zero
+    x₀∈xs : x₀ ∈ xs
+    x₀∈xs = zero , ≡.refl
+    x₀∈ys : x₀ ∈ ys
+    x₀∈ys = apply xs↭ys′ x₀∈xs
+    -- reduce the problem by removing those elements
+    xs⁻ : Vector A n
+    xs⁻ = remove xs x₀∈xs
+    ys⁻ : Vector A m
+    ys⁻ = remove ys x₀∈ys
+    xs↭ys⁻ : xs⁻ ↭′ ys⁻
+    xs↭ys⁻ = ↭-remove xs↭ys′ x₀∈xs
+    -- recursion on the reduced problem
+    xs↭ys⁻′ : toList xs⁻ ↭ toList ys⁻
+    xs↭ys⁻′ = toList-↭ xs↭ys⁻
+    -- indices for working with vectors
+    i : Fin (suc n)
+    i = proj₁ x₀∈xs
+    j : Fin (suc m)
+    j = proj₁ x₀∈ys
+    i′ : Fin (suc (length (toList xs⁻)))
+    i′ = cast (≡.sym (≡.cong suc (length-tabulate xs⁻))) i
+    j′ : Fin (suc (length (toList ys⁻)))
+    j′ = cast (≡.sym (≡.cong suc (length-tabulate ys⁻))) j
+    -- main construction
+    open VectorProp using (insertAt-removeAt)
+    open PermutationReasoning
+    open Vector using () renaming (insertAt to insertAt′)
+    xs↭ys : toList xs ↭ toList ys
+    xs↭ys = begin
+        toList xs                       ≡⟨ tabulate-cong (insertAt-removeAt xs i) ⟨
+        toList (insertAt′ xs⁻ i x₀)     ≡⟨ insertAt-toList i′ i ≡.refl x₀ ⟨
+        insertAt (toList xs⁻) i′ x₀     ↭⟨ ↭-insert xs↭ys⁻′ i′ j′ x₀ ⟩
+        insertAt (toList ys⁻) j′ x₀     ≡⟨ insertAt-toList j′ j ≡.refl x₀ ⟩
+        toList (insertAt′ ys⁻ j x₀)     ≡⟨ ≡.cong (toList ∘ insertAt′ ys⁻ j) (proj₂ x₀∈ys) ⟩
+        toList (insertAt′ ys⁻ j (ys j)) ≡⟨ tabulate-cong (insertAt-removeAt ys j) ⟩
+        toList ys ∎
diff --git a/Data/Permutation/Sort.agda b/Data/Permutation/Sort.agda
new file mode 100644
index 0000000..8d097f2
--- /dev/null
+++ b/Data/Permutation/Sort.agda
@@ -0,0 +1,29 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Bundles using (DecTotalOrder)
+
+module Data.Permutation.Sort {ℓ₁ ℓ₂ ℓ₃} (dto : DecTotalOrder ℓ₁ ℓ₂ ℓ₃) where
+
+open DecTotalOrder dto using (module Eq; totalOrder) renaming (Carrier to A)
+
+open import Data.List.Base using (List)
+open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid using (_≋_)
+open import Data.List.Relation.Binary.Permutation.Setoid Eq.setoid using (_↭_; module PermutationReasoning)
+open import Data.List.Relation.Unary.Sorted.TotalOrder.Properties using (↗↭↗⇒≋)
+open import Data.List.Sort dto using (sortingAlgorithm)
+open import Data.List.Sort.Base totalOrder using (SortingAlgorithm)
+open SortingAlgorithm sortingAlgorithm using (sort; sort-↭ₛ; sort-↗)
+
+sorted-≋
+    : {xs ys : List A}
+    → xs ↭ ys
+    → sort xs ≋ sort ys
+sorted-≋ {xs} {ys} xs↭ys = ↗↭↗⇒≋ totalOrder (sort-↗ xs) (sort-↗ ys) sort-xs↭sort-ys
+  where
+    open PermutationReasoning
+    sort-xs↭sort-ys : sort xs ↭ sort ys
+    sort-xs↭sort-ys = begin
+      sort xs ↭⟨ sort-↭ₛ xs ⟩
+      xs      ↭⟨ xs↭ys ⟩
+      ys      ↭⟨ sort-↭ₛ ys ⟨
+      sort ys ∎
diff --git a/Data/SExp.agda b/Data/SExp.agda
new file mode 100644
index 0000000..adf4325
--- /dev/null
+++ b/Data/SExp.agda
@@ -0,0 +1,75 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.SExp where
+
+open import Data.List using (List)
+open import Data.Nat.Base using (ℕ)
+open import Data.Nat.Show using () renaming (show to showNat)
+open import Data.String.Base as String using (String; parens; intersperse; _<+>_)
+
+open List
+
+module ListBased where
+
+  data SExp : Set where
+    Atom : String → SExp
+    Nat : ℕ → SExp
+    SExps : List SExp → SExp
+
+  mutual
+    showSExp : SExp → String
+    showSExp (Atom s)   = s
+    showSExp (Nat n)    = showNat n
+    showSExp (SExps xs) = parens (intersperse " " (showList xs))
+
+    -- expanded out map for termination checker
+    showList : List SExp → List String
+    showList []       = []
+    showList (x ∷ xs) = showSExp x ∷ showList xs
+
+module PairBased where
+
+  data SExp : Set where
+    Atom : String → SExp
+    Nat : ℕ → SExp
+    Nil : SExp
+    Pair : SExp → SExp → SExp
+
+  mutual
+    showSExp : SExp → String
+    showSExp (Atom s)   = s
+    showSExp (Nat n)    = showNat n
+    showSExp Nil        = "()"
+    showSExp (Pair l r) = parens (showPair l r)
+
+    showPair : SExp → SExp → String
+    showPair x (Atom s)   = showSExp x <+> "." <+> s
+    showPair x (Nat n)    = showSExp x <+> "." <+> showNat n
+    showPair x Nil        = showSExp x
+    showPair x (Pair l r) = showSExp x <+> showPair l r
+
+open ListBased public
+open PairBased
+
+mutual
+  sexpL→sexpP : ListBased.SExp → PairBased.SExp
+  sexpL→sexpP (Atom s)  = Atom s
+  sexpL→sexpP (Nat n)   = Nat n
+  sexpL→sexpP (SExps xs) = [sexpL]→sexpP xs
+
+  [sexpL]→sexpP : List (ListBased.SExp) → PairBased.SExp
+  [sexpL]→sexpP []       = Nil
+  [sexpL]→sexpP (x ∷ xs) = Pair (sexpL→sexpP x) ([sexpL]→sexpP xs)
+
+mutual
+  sexpP→sexpL : PairBased.SExp → ListBased.SExp
+  sexpP→sexpL (Atom s)   = Atom s
+  sexpP→sexpL (Nat n)    = Nat n
+  sexpP→sexpL Nil        = SExps []
+  sexpP→sexpL (Pair x y) = SExps (sexpP→sexpL x ∷ sexpP→[sexpL] y)
+
+  sexpP→[sexpL] : PairBased.SExp → List (ListBased.SExp)
+  sexpP→[sexpL] (Atom _)   = []
+  sexpP→[sexpL] (Nat _)    = []
+  sexpP→[sexpL] Nil        = []
+  sexpP→[sexpL] (Pair x y) = sexpP→sexpL x ∷ sexpP→[sexpL] y
diff --git a/Data/SExp/Parser.agda b/Data/SExp/Parser.agda
new file mode 100644
index 0000000..ec1b6a5
--- /dev/null
+++ b/Data/SExp/Parser.agda
@@ -0,0 +1,73 @@
+{-# OPTIONS --without-K --guardedness --safe #-}
+
+open import Text.Parser.Types.Core using (Parameters)
+
+module Data.SExp.Parser {l} {P : Parameters l} where
+
+import Data.String.Base as String
+open import Data.List as List using (List)
+
+open import Data.Char.Base using (Char)
+open import Data.List.Sized.Interface using (Sized)
+open import Data.List.NonEmpty as List⁺ using (List⁺) renaming (map to map⁺)
+open import Data.Subset using (Subset; into)
+open import Effect.Monad using (RawMonadPlus)
+open import Function.Base using (_∘_; _$_)
+open import Induction.Nat.Strong using (fix; map; □_)
+open import Relation.Binary.PropositionalEquality.Decidable using (DecidableEquality)
+open import Relation.Unary using (IUniversal; _⇒_)
+open import Level.Bounded using (theSet; [_])
+open import Text.Parser.Types P using (Parser)
+open import Text.Parser.Combinators {P = P} using (_<$>_; list⁺; _<|>_; _<$_; _<&_; _<&?_; box)
+open import Text.Parser.Combinators.Char {P = P} using (alpha; parens; withSpaces; spaces; char)
+open import Text.Parser.Combinators.Numbers {P = P} using (decimalℕ)
+
+open import Data.SExp using (SExp)
+open SExp
+
+open Parameters P using (M; Tok; Toks)
+
+module _
+    {{𝕄 : RawMonadPlus M}}
+    {{𝕊 : Sized Tok Toks}}
+    {{𝔻 : DecidableEquality (theSet Tok)}}
+    {{ℂ : Subset Char (theSet Tok)}}
+    {{ℂ⁻ : Subset (theSet Tok) Char}}
+  where
+
+  -- An atom is just a non-empty list of alphabetical characters.
+  -- We use `<$>` to turn that back into a string and apply the `Atom` constructor.
+  atom : ∀[ Parser [ SExp ] ]
+  atom = Atom ∘ String.fromList⁺ ∘ map⁺ (into ℂ⁻) <$> list⁺ alpha
+
+  -- Natural number parser
+  nat : ∀[ Parser [ SExp ] ]
+  nat = Nat <$> decimalℕ
+
+  -- Empty list parser
+  nil : ∀[ Parser [ SExp ] ]
+  nil = SExps List.[] <$ char '(' <&? box spaces <& box (char ')')
+
+  -- Parser for a list of S-Expressions
+  list : ∀[ Parser [ SExp ] ⇒ Parser [ List SExp ] ]
+  list sexp = List⁺.toList <$> list⁺ (withSpaces sexp)
+
+  -- Compound S-Expression parser
+  compound : ∀[ □ Parser [ SExp ] ⇒ Parser [ SExp ] ]
+  compound rec = nil <|> SExps <$> parens (map list rec)
+
+  -- S-Expression parser
+  sexp : ∀[ □ Parser [ SExp ] ⇒ Parser [ SExp ] ]
+  sexp rec = atom <|> nat <|> compound rec
+
+  -- Build the parser as a fixpoint since SExp is an inductive type
+  sexp-top : ∀[ Parser [ SExp ] ]
+  sexp-top = fix (Parser [ SExp ]) sexp
+
+  -- Top-level parser for list of S-Expressions
+  LIST : ∀[ Parser [ SExp ] ]
+  LIST = SExps <$> list sexp-top
+
+  -- Top-level S-Expression parser
+  SEXP : ∀[ Parser [ SExp ] ]
+  SEXP = withSpaces sexp-top