diff --git a/.gitignore b/.gitignore
index 887d278..56966b7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -15,6 +15,10 @@
 *.hp
 *.eventlog
 
+### agda2hs ###
+_build
+*.agdai
+
 ### Cabal ###
 dist
 dist-*
diff --git a/lib/fine-types-core/CHANGELOG.md b/lib/fine-types-core/CHANGELOG.md
new file mode 100644
index 0000000..228efdd
--- /dev/null
+++ b/lib/fine-types-core/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for fine-types-core
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.
diff --git a/lib/fine-types-core/README.md b/lib/fine-types-core/README.md
new file mode 100644
index 0000000..5c8f366
--- /dev/null
+++ b/lib/fine-types-core/README.md
@@ -0,0 +1,15 @@
+[FineTypes][] is an interface description language (IDL) focussing on types.
+
+  [finetypes]: https://github.com/cardano-foundation/fine-types
+
+The `fine-types-core` package defines the core data types and functions — and it includes machine-checked proofs!
+
+The proofs are written in Agda and the code is exported to Haskell using [agda2hs][].
+
+The repository layout includes:
+
+* `./src/agda` — Agda source code with proofs.
+* `./src/haskell` — Haskell source code that was **autogenerated** from the Agda code. These files are still checked into the repository.
+* `./generate-haskell.sh` — Script which uses [agda2hs][] to generate the Haskell source code. Run this script whenever you change the Agda source.
+
+  [agda2hs]: https://github.com/agda/agda2hs
diff --git a/lib/fine-types-core/fine-types-core.agda-lib b/lib/fine-types-core/fine-types-core.agda-lib
new file mode 100644
index 0000000..a628343
--- /dev/null
+++ b/lib/fine-types-core/fine-types-core.agda-lib
@@ -0,0 +1,3 @@
+name: fine-types-core
+include: ./src/agda
+depend: agda2hs, standard-library
diff --git a/lib/fine-types-core/fine-types-core.cabal b/lib/fine-types-core/fine-types-core.cabal
new file mode 100644
index 0000000..e3f89dd
--- /dev/null
+++ b/lib/fine-types-core/fine-types-core.cabal
@@ -0,0 +1,63 @@
+cabal-version:      3.0
+name:               fine-types-core
+version:            0.1.0.0
+synopsis:           A interface description language (IDL) focusing on types
+description:        Core definitions and proofs for fine-types.
+homepage:           https://github.com/cardano-foundation/fine-types
+license:            Apache-2.0
+license-file:       LICENSE
+author:             HAL, Cardano Foundation
+maintainer:         hal@cardanofoundation.org
+copyright:          2023 Cardano Foundation
+category:           Language
+
+extra-doc-files:
+  CHANGELOG.md
+extra-source-files:
+  generate-haskell.sh
+  fine-types-core.agda-lib
+  src/agda/**/*.agda
+
+common language
+  default-language:
+    Haskell2010
+  default-extensions:
+    NoImplicitPrelude
+  other-extensions:
+    NamedFieldPuns
+    OverloadedStrings
+
+common opts-lib
+  ghc-options: -Wall -Wcompat -Wredundant-constraints -Wincomplete-uni-patterns -Wincomplete-record-updates
+
+  if flag(release)
+    ghc-options: -O2 -Werror
+
+common opts-exe
+  ghc-options: -threaded -rtsopts
+  ghc-options: -Wall -Wcompat -Wredundant-constraints -Wincomplete-uni-patterns -Wincomplete-record-updates
+
+  if flag(release)
+    ghc-options: -O2 -Werror
+
+flag release
+  description: Enable optimization and `-Werror`
+  default:     False
+  manual:      True
+
+library
+  import:      language, opts-lib
+  hs-source-dirs:
+    src/haskell
+  build-depends:
+    , base >=4.14.3.0
+    , containers
+    , deepseq >= 1.4.4
+    , QuickCheck
+  exposed-modules:
+    Data.Embedding
+    Language.FineTypes
+    Language.FineTypes.Embedding
+    Language.FineTypes.Typ
+    Language.FineTypes.Value.Def
+    Language.FineTypes.Value.Typcheck
diff --git a/lib/fine-types-core/generate-haskell.sh b/lib/fine-types-core/generate-haskell.sh
new file mode 100755
index 0000000..c904642
--- /dev/null
+++ b/lib/fine-types-core/generate-haskell.sh
@@ -0,0 +1,2 @@
+#!/bin/sh
+agda2hs ./src/agda/Language/FineTypes.agda -o ./src/haskell/
diff --git a/lib/fine-types-core/src/agda/Data/Embedding.agda b/lib/fine-types-core/src/agda/Data/Embedding.agda
new file mode 100644
index 0000000..974801b
--- /dev/null
+++ b/lib/fine-types-core/src/agda/Data/Embedding.agda
@@ -0,0 +1,21 @@
+module Data.Embedding where
+
+{-# FOREIGN AGDA2HS
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+#-}
+
+open import Haskell.Prelude
+
+{-----------------------------------------------------------------------------
+    Embedding
+------------------------------------------------------------------------------}
+record Embedding (a b : Set) : Set where
+  field
+    to   : a → b
+    from : b → a
+    @0 from∘to : ∀ (x : a) → from (to x) ≡ x
+
+open Embedding public
+
+{-# COMPILE AGDA2HS Embedding #-}
diff --git a/lib/fine-types-core/src/agda/Language/FineTypes.agda b/lib/fine-types-core/src/agda/Language/FineTypes.agda
new file mode 100644
index 0000000..b4a3d6f
--- /dev/null
+++ b/lib/fine-types-core/src/agda/Language/FineTypes.agda
@@ -0,0 +1,12 @@
+module Language.FineTypes where
+
+{-# FOREIGN AGDA2HS
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+#-}
+
+import Data.Embedding
+import Language.FineTypes.Typ
+import Language.FineTypes.Value.Def
+import Language.FineTypes.Embedding
+-- import Language.FineTypes.Value.Typcheck
diff --git a/lib/fine-types-core/src/agda/Language/FineTypes/Embedding.agda b/lib/fine-types-core/src/agda/Language/FineTypes/Embedding.agda
new file mode 100644
index 0000000..91bfc36
--- /dev/null
+++ b/lib/fine-types-core/src/agda/Language/FineTypes/Embedding.agda
@@ -0,0 +1,77 @@
+module Language.FineTypes.Embedding where
+
+{-# FOREIGN AGDA2HS
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+#-}
+
+open import Haskell.Prelude hiding (_×_; _+_; Pair)
+open import Relation.Nullary using (¬_)
+
+open import Data.Embedding
+open import Language.FineTypes.Value.Def
+open import Language.FineTypes.Typ
+  using (Typ; _+_; _×_)
+
+import Language.FineTypes.Typ as Typ
+
+{-----------------------------------------------------------------------------
+    Embedding with Typ information
+------------------------------------------------------------------------------}
+record EmbeddingTyp (@0 A B : Typ) : Set where
+  field
+    embed    : Embedding (Value A) (Value B)
+    typcheck : Typ → Maybe Typ
+    @0 accepts : typcheck A ≡ Just B
+    @0 rejects : ∀ (C : Typ) → typcheck C ≡ Nothing → ¬(C ≡ A)
+
+open EmbeddingTyp public
+
+{-# COMPILE AGDA2HS EmbeddingTyp #-}
+
+{-----------------------------------------------------------------------------
+    Specific Embeddings
+------------------------------------------------------------------------------}
+distributeVal
+  : ∀ {@0 A B C : Typ}
+  → Embedding
+      (Value ((A + B) × C))
+      (Value ((A × C) + (B × C)))
+distributeVal =
+  record
+    { to = λ
+      { (Product2 (Sum2L a) c) → Sum2L (Product2 a c)
+      ; (Product2 (Sum2R b) c) → Sum2R (Product2 b c)
+      }
+    ; from = λ
+      { (Sum2L (Product2 a c)) → (Product2 (Sum2L a) c)
+      ; (Sum2R (Product2 b c)) → (Product2 (Sum2R b) c)
+      }
+    ; from∘to = λ
+      { (Product2 (Sum2L a) c) → refl
+      ; (Product2 (Sum2R b) c) → refl
+      }
+    }
+
+{-# COMPILE AGDA2HS distributeVal #-}
+
+distribute
+  : ∀ {@0 A B C : Typ}
+  → EmbeddingTyp
+      ((A + B) × C)
+      ((A × C) + (B × C))
+distribute =
+  record
+    { embed = distributeVal
+    ; typcheck = λ
+      { (Typ.Two Typ.Product2 (Typ.Two Typ.Sum2 a b) c)
+          → Just (Typ.Two Typ.Sum2 (Typ.Two Typ.Product2 a c) (Typ.Two Typ.Product2 b c))
+      ; _ → Nothing
+      }
+    ; accepts = refl
+    ; rejects = λ
+      { (Typ.Two Typ.Product2 (Typ.Two Typ.Sum2 _ _) _) → λ ()
+      }
+    }
+
+{-# COMPILE AGDA2HS distribute #-}
diff --git a/lib/fine-types-core/src/agda/Language/FineTypes/Typ.agda b/lib/fine-types-core/src/agda/Language/FineTypes/Typ.agda
new file mode 100644
index 0000000..bf778e4
--- /dev/null
+++ b/lib/fine-types-core/src/agda/Language/FineTypes/Typ.agda
@@ -0,0 +1,149 @@
+module Language.FineTypes.Typ where
+
+{-# FOREIGN AGDA2HS
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+#-}
+
+open import Haskell.Prelude
+  using (String; List; True; False)
+  renaming (_×_ to Pair)
+open import Haskell.Law.Eq
+open import Haskell.Prim.Eq
+
+import Haskell.Prelude as Hs
+
+ConstructorName = String
+FieldName = String
+TypName = String
+VarName = String
+
+{-# COMPILE AGDA2HS ConstructorName #-}
+{-# COMPILE AGDA2HS FieldName #-}
+{-# COMPILE AGDA2HS TypName #-}
+{-# COMPILE AGDA2HS VarName #-}
+
+{-----------------------------------------------------------------------------
+    Haskell - Typ
+------------------------------------------------------------------------------}
+data TypConst : Set where
+  Bool     : TypConst
+  Bytes    : TypConst
+  Integer  : TypConst
+  Natural  : TypConst
+  Text     : TypConst
+  Rational : TypConst
+  Unit     : TypConst
+
+data OpOne : Set where
+  Option   : OpOne
+  Sequence : OpOne
+  PowerSet : OpOne
+
+data OpTwo : Set where
+  Sum2     : OpTwo
+  Product2 : OpTwo
+  PartialFunction : OpTwo
+  FiniteSupport   : OpTwo
+
+data Constraint1 : Set where
+  Braces : List Constraint1 → Constraint1
+  Token  : String → Constraint1
+
+Constraint = List Constraint1
+
+data Typ : Set where
+  Var  : TypName → Typ
+  Zero : TypConst → Typ
+  One  : OpOne → Typ → Typ
+  Two  : OpTwo → Typ → Typ → Typ
+  ProductN : List (Pair FieldName Typ) → Typ
+  SumN : List (Pair ConstructorName Typ) → Typ
+  Constrained : VarName → Typ → Constraint → Typ 
+
+{-# COMPILE AGDA2HS TypConst #-}
+{-# COMPILE AGDA2HS OpOne #-}
+{-# COMPILE AGDA2HS OpTwo #-}
+{-# COMPILE AGDA2HS Constraint1 #-}
+{-# COMPILE AGDA2HS Constraint #-}
+{-# COMPILE AGDA2HS Typ #-}
+
+{-----------------------------------------------------------------------------
+    Agda - Equality
+------------------------------------------------------------------------------}
+instance
+  iTypConst : Eq TypConst
+  iTypConst ._==_ Bool Bool = True
+  iTypConst ._==_ Bytes Bytes = True
+  iTypConst ._==_ Integer Integer = True
+  iTypConst ._==_ Natural Natural = True
+  iTypConst ._==_ Text Text = True
+  iTypConst ._==_ Rational Rational = True
+  iTypConst ._==_ Unit Unit = True
+  iTypConst ._==_ _ _ = Hs.False
+
+{-# COMPILE AGDA2HS iTypConst derive #-}
+
+-- Created by automati case splitting C^c C^c
+-- and automatic goal finding C^c C^a
+instance
+  iLawfulEqTypConst : IsLawfulEq TypConst
+
+  iLawfulEqTypConst .isEquality Bool Bool = Hs.ofY Hs.refl
+  iLawfulEqTypConst .isEquality Bool Bytes = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bool Integer = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bool Natural = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bool Text = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bool Rational = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bool Unit = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bytes Bool = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bytes Bytes = Hs.ofY Hs.refl
+  iLawfulEqTypConst .isEquality Bytes Integer = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bytes Natural = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bytes Text = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bytes Rational = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bytes Unit = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Integer Bool = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Integer Bytes = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Integer Integer = Hs.ofY Hs.refl
+  iLawfulEqTypConst .isEquality Integer Natural = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Integer Text = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Integer Rational = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Integer Unit = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Natural Bool = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Natural Bytes = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Natural Integer = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Natural Natural = Hs.ofY Hs.refl
+  iLawfulEqTypConst .isEquality Natural Text = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Natural Rational = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Natural Unit = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Text Bool = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Text Bytes = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Text Integer = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Text Natural = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Text Text = Hs.ofY Hs.refl
+  iLawfulEqTypConst .isEquality Text Rational = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Text Unit = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Rational Bool = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Rational Bytes = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Rational Integer = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Rational Natural = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Rational Text = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Rational Rational = Hs.ofY Hs.refl
+  iLawfulEqTypConst .isEquality Rational Unit = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Bool = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Bytes = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Integer = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Natural = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Text = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Rational = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Unit = Hs.ofY Hs.refl
+
+{-----------------------------------------------------------------------------
+    Agda - Syntactic sugar
+------------------------------------------------------------------------------}
+_×_ : Typ → Typ → Typ
+A × B = Two Product2 A B
+
+_+_ : Typ → Typ → Typ
+A + B = Two Sum2 A B
diff --git a/lib/fine-types-core/src/agda/Language/FineTypes/Value.agda b/lib/fine-types-core/src/agda/Language/FineTypes/Value.agda
new file mode 100644
index 0000000..bff15b9
--- /dev/null
+++ b/lib/fine-types-core/src/agda/Language/FineTypes/Value.agda
@@ -0,0 +1,199 @@
+module Language.FineTypes.Value where
+
+{-# FOREIGN AGDA2HS
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+#-}
+
+open import Haskell.Prelude hiding (_×_; _+_; Pair; case_of_)
+open import Function.Base using (case_of_)
+open import Language.FineTypes.Typ
+
+isJust : ∀ {a : Set} → Maybe a → Bool
+isJust (Just _) = True
+isJust Nothing  = False
+
+{-----------------------------------------------------------------------------
+    Values index by a typ
+------------------------------------------------------------------------------}
+data Val : @0 Typ → Set where
+  Unit : Val (Zero TUnit)
+  Pair : ∀ {@0 A B : Typ} → Val A → Val B → Val (A × B)
+  SumL : ∀ {@0 A B : Typ} → Val A → Val (A + B)
+  SumR : ∀ {@0 A B : Typ} → Val B → Val (A + B)
+
+{-# COMPILE AGDA2HS Val #-}
+
+{-----------------------------------------------------------------------------
+    Equality of Values at run-time
+------------------------------------------------------------------------------}
+data Eq-runtime : {@0 A B : Typ} → Val A → Val B → Set where
+  eq-Unit : Eq-runtime Unit Unit
+  eq-Pair
+    : ∀ {@0 A1 A2 B1 B2 : Typ}
+      {a1 : Val A1} {a2 : Val A2}
+      {b1 : Val B1} {b2 : Val B2}
+    → Eq-runtime a1 a2
+    → Eq-runtime b1 b2
+    → Eq-runtime (Pair a1 b1) (Pair a2 b2)
+  eq-SumL
+    : ∀ {@0 A1 A2 B1 B2 : Typ}
+      {a1 : Val A1} {a2 : Val A2}
+    → Eq-runtime a1 a2
+    → Eq-runtime (SumL {A1} {B1} a1) (SumL {A2} {B2} a2)
+  eq-SumR
+    : ∀ {@0 A1 A2 B1 B2 : Typ}
+      {b1 : Val B1} {b2 : Val B2}
+    → Eq-runtime b1 b2
+    → Eq-runtime (SumR {A1} {B1} b1) (SumR {A2} {B2} b2)
+
+-- Lemma:
+-- When to values are related by a run-time equality,
+-- we can translate this into a function that maps one into the other.
+
+{-----------------------------------------------------------------------------
+    Type checking on the value level
+------------------------------------------------------------------------------}
+data Typchecks {@0 A : Typ} (va : Val A) (B : Typ) : Set where
+  Checks
+    : (vb : Val B)
+    → Eq-runtime va vb
+    → Typchecks va B
+
+-- | Helper function that recurses into the typ and returns proof.
+checkTyp
+  : ∀ {@0 A : Typ} (v : Val A) (B : Typ)
+  → Maybe (Typchecks v B)
+checkTyp Unit (Zero TUnit) =
+  Just (Checks Unit eq-Unit)
+checkTyp (Pair x y) (Two Product2 X Y) =
+  case (checkTyp x X) of λ
+    { Nothing → Nothing
+    ; (Just (Checks x' ex)) →
+      case (checkTyp y Y) of λ
+        { Nothing → Nothing
+        ; (Just (Checks y' ey)) →
+          Just (Checks (Pair x' y') (eq-Pair ex ey))
+      }
+    }
+checkTyp (SumL x) (Two Sum2 X _) =
+  case (checkTyp x X) of λ
+    { Nothing → Nothing
+    ; (Just (Checks x' ex)) →
+      Just (Checks (SumL x') (eq-SumL ex))
+    }
+checkTyp (SumR y) (Two Sum2 _ Y) =
+  case (checkTyp y Y) of λ
+    { Nothing → Nothing
+    ; (Just (Checks y' ey)) →
+      Just (Checks (SumR y') (eq-SumR ey))
+    }
+checkTyp _ _ = Nothing
+
+-- | Value-level check whether the typ matches.
+hasTyp : ∀ {@0 A : Typ} → Val A → Typ → Bool
+hasTyp Unit (Zero TUnit) = True
+hasTyp (Pair x y) (Two Product2 tx ty) =
+  hasTyp x tx && hasTyp y ty
+hasTyp (SumL x) (Two Sum2 tx _) =
+  hasTyp x tx
+hasTyp (SumR y) (Two Sum2 _ ty) =
+  hasTyp y ty
+hasTyp _ _ =
+  False
+
+{-
+test : (A : Typ) {@0 A = A₁ : Typ} (a : Val A₁)
+  (w : Maybe (Typchecks a A)) →
+  checkTyp a A ≡ w →
+  (B : Typ) {@0 B = B₁ : Typ} (b : Val B₁) →
+  (isJust w && isJust (checkTyp b B)) ≡
+  isJust
+  ((λ { Nothing → Nothing
+      ; (Just (Checks x' ex))
+          → case checkTyp b B of
+            (λ { Nothing → Nothing
+              ; (Just (Checks y' ey))
+                  → Just (Checks (Pair x' y') (eq-Pair ex ey))
+              })
+      })
+  w)
+test = {!   !}
+-}
+
+{-
+lemma-upgrade-hasTyp
+  : ∀ {@0 A : Typ} (va : Val A) (B : Typ)
+  → hasTyp va B ≡ isJust (checkTyp va B)
+lemma-upgrade-hasTyp Unit (Zero TUnit) = refl
+lemma-upgrade-hasTyp (Pair x y) (Two Product2 X Y)
+    rewrite lemma-upgrade-hasTyp x X
+    rewrite lemma-upgrade-hasTyp y Y
+      with checkTyp y Y in eqY
+...      | Nothing with checkTyp x X in eqX
+...                | _ = ? 
+
+-}
+{-
+postulate
+  A : Set
+  B : A → Set
+  H : (x : A) → B x → Set
+
+import Agda.Builtin.Sigma as S
+
+test : (p : S.Σ A B) (w : A) → H w (S.snd p)
+test = ?
+-}
+
+lemma-upgrade-hasTyp
+  : ∀ {@0 A : Typ} (B : Typ) (va : Val A)
+  → hasTyp va B ≡ isJust (checkTyp va B)
+lemma-upgrade-hasTyp (Zero TUnit) Unit = refl
+lemma-upgrade-hasTyp (Two Product2 A B) (Pair a b)
+  rewrite lemma-upgrade-hasTyp A a
+  rewrite lemma-upgrade-hasTyp B b
+    with checkTyp a A
+... | Nothing = refl
+... | Just (Checks _ _) with checkTyp b B
+...   | Nothing  = refl
+...   | Just (Checks _ _) = refl
+lemma-upgrade-hasTyp (Two Sum2 A _) (SumL a)
+  rewrite lemma-upgrade-hasTyp A a
+    with checkTyp a A
+... | Nothing = refl
+... | (Just (Checks x' ex)) = refl
+lemma-upgrade-hasTyp (Two Sum2 _ B) (SumR b)
+  rewrite lemma-upgrade-hasTyp B b
+    with checkTyp b B
+... | Nothing = refl
+... | (Just (Checks y' ey)) = refl
+lemma-upgrade-hasTyp (Zero TBool) Unit = refl
+lemma-upgrade-hasTyp (Zero TNatural) Unit = refl
+lemma-upgrade-hasTyp (One x B) Unit = refl
+lemma-upgrade-hasTyp (Two x B B₁) Unit = refl
+lemma-upgrade-hasTyp (Zero x) (Pair va va₁) = refl
+lemma-upgrade-hasTyp (One x B) (Pair va va₁) = refl
+lemma-upgrade-hasTyp (Two Sum2 B B₁) (Pair va va₁) = refl
+lemma-upgrade-hasTyp (Zero x) (SumL va) = refl
+lemma-upgrade-hasTyp (One x B) (SumL va) = refl
+lemma-upgrade-hasTyp (Two Product2 B B₁) (SumL va) = refl
+lemma-upgrade-hasTyp (Zero x) (SumR va) = refl
+lemma-upgrade-hasTyp (One x B) (SumR va) = refl
+lemma-upgrade-hasTyp (Two Product2 B B₁) (SumR va) = refl
+
+lemma-good-hasTyp
+  : ∀ (A : Typ) (a : Val A)
+  → hasTyp a A ≡ True
+lemma-good-hasTyp (Zero TUnit) Unit = refl
+lemma-good-hasTyp (Two Product2 A B) (Pair a b)
+  rewrite lemma-good-hasTyp A a
+  rewrite lemma-good-hasTyp B b
+  = refl
+lemma-good-hasTyp (Two Sum2 A _) (SumL a) =
+  lemma-good-hasTyp A a
+lemma-good-hasTyp (Two Sum2 _ B) (SumR b) =
+  lemma-good-hasTyp B b
+
+{-# COMPILE AGDA2HS hasTyp #-}
+   
\ No newline at end of file
diff --git a/lib/fine-types-core/src/agda/Language/FineTypes/Value/Def.agda b/lib/fine-types-core/src/agda/Language/FineTypes/Value/Def.agda
new file mode 100644
index 0000000..526f369
--- /dev/null
+++ b/lib/fine-types-core/src/agda/Language/FineTypes/Value/Def.agda
@@ -0,0 +1,135 @@
+module Language.FineTypes.Value.Def where
+
+open import Haskell.Prelude
+    hiding (_×_; _+_; Pair; case_of_; Bool; Integer )
+open import Function.Base
+    using (case_of_)
+open import Language.FineTypes.Typ
+    using (Typ; OpOne; OpTwo; _×_; _+_)
+
+import Haskell.Prelude as Hs
+import Language.FineTypes.Typ as Typ
+
+{-----------------------------------------------------------------------------
+    Values
+------------------------------------------------------------------------------}
+data ZeroF : @0 Typ.TypConst → Set where
+  Bool : Hs.Bool → ZeroF Typ.Bool
+-- Bytes : ByteString → ZeroF
+  Integer : Hs.Integer → ZeroF Typ.Integer
+  Natural : Nat → ZeroF Typ.Natural
+--  Rational : Hs.Rational → ZeroF
+--  Text : Text → ZeroF
+  Unit : ZeroF Typ.Unit
+
+
+data OneF (a : Set) : @0 Typ.OpOne → Set where
+  Option : Maybe a → OneF a Typ.Option
+  Sequence : List a → OneF a Typ.Sequence
+--  PowerSet : Set a → OneF a
+
+data TwoF (a b : Set) : @0 Typ.OpTwo → Set where
+--  FiniteMap : Map a b → TwoF a b
+
+Ix = Hs.Int
+
+data Value : @0 Typ → Set where
+  Zero    : ∀ {@0 A : Typ.TypConst} → ZeroF A → Value (Typ.Zero A)
+  One     : ∀ {@0 A : Typ} {@0 op : OpOne}
+          → OneF (Value A) op → Value (Typ.One op A)
+  Two     : ∀ {@0 A B : Typ} {@0 op : OpTwo}
+          → TwoF (Value A) (Value B) op
+          → Value (Typ.Two op A B)
+  Product2 : ∀ {@0 A B : Typ} → Value A → Value B → Value (A × B)
+  Sum2L    : ∀ {@0 A B : Typ} → Value A → Value (A + B)
+  Sum2R    : ∀ {@0 A B : Typ} → Value B → Value (A + B)
+
+--  Product : ∀ {@0 A : Typ} → List Value → Value
+--  Sum     : Ix → Value → Value
+
+{-# COMPILE AGDA2HS ZeroF #-}
+{-# COMPILE AGDA2HS OneF #-}
+{-# COMPILE AGDA2HS TwoF #-}
+{-# COMPILE AGDA2HS Ix #-}
+{-# COMPILE AGDA2HS Value #-}
+
+{-----------------------------------------------------------------------------
+    Equality of Value
+------------------------------------------------------------------------------}
+eqZeroF : ∀{@0 A B : Typ.TypConst} → ZeroF A → ZeroF B → Hs.Bool
+eqZeroF (Bool x) (Bool y) = x == y
+eqZeroF (Bool _) _ = False
+eqZeroF (Integer x) (Integer y) = True
+eqZeroF (Integer _) _ = False
+eqZeroF (Natural _) (Natural _) = True
+eqZeroF (Natural _) _ = False
+eqZeroF Unit Unit = False
+eqZeroF Unit _ = False
+
+-- mutually recursive definitions
+eqValue
+  : ∀{@0 A B : Typ} → Value A → Value B → Hs.Bool
+eqMaybeValue
+  : ∀{@0 A B : Typ}
+  → Maybe (Value A) → Maybe (Value B) → Hs.Bool
+eqListValue
+  : ∀{@0 A B : Typ}
+  → List (Value A) → List (Value B) → Hs.Bool
+
+eqMaybeValue (Just x) (Just y) = eqValue x y
+eqMaybeValue (Just _) _ = False
+eqMaybeValue Nothing Nothing = True
+eqMaybeValue Nothing _ = False
+
+eqListValue (x ∷ xs) (y ∷ ys) = eqValue x y && eqListValue xs ys
+eqListValue (_ ∷ _) _ = False
+eqListValue [] [] = True
+eqListValue [] _ = False
+
+eqValue (Zero x) (Zero y) = eqZeroF x y
+eqValue (Zero _) _ = False
+eqValue (One (Option x)) (One (Option y)) = eqMaybeValue x y
+eqValue (One (Option _)) _ = False
+eqValue (One (Sequence x)) (One (Sequence y)) = eqListValue x y
+eqValue (One (Sequence _)) _ = False
+eqValue (Two _) (Two _) = True
+eqValue (Two _) _ = False
+eqValue (Product2 x1 x2) (Product2 y1 y2) =
+    (eqValue x1 y1 && eqValue x2 y2)
+eqValue (Product2 _ _) _ = False
+eqValue (Sum2L x) (Sum2L y) = eqValue x y
+eqValue (Sum2L _) _ = False
+eqValue (Sum2R x) (Sum2R y) = eqValue x y
+eqValue (Sum2R _) _ = False
+
+{-# COMPILE AGDA2HS eqZeroF #-}
+{-# COMPILE AGDA2HS eqValue #-}
+{-# COMPILE AGDA2HS eqMaybeValue #-}
+{-# COMPILE AGDA2HS eqListValue #-}
+
+{-
+data Eq-runtime : {@0 A B : Typ} → Value A → Val B → Set where
+  eq-Unit : Eq-runtime Unit Unit
+  eq-Pair
+    : ∀ {@0 A1 A2 B1 B2 : Typ}
+      {a1 : Val A1} {a2 : Val A2}
+      {b1 : Val B1} {b2 : Val B2}
+    → Eq-runtime a1 a2
+    → Eq-runtime b1 b2
+    → Eq-runtime (Pair a1 b1) (Pair a2 b2)
+  eq-SumL
+    : ∀ {@0 A1 A2 B1 B2 : Typ}
+      {a1 : Val A1} {a2 : Val A2}
+    → Eq-runtime a1 a2
+    → Eq-runtime (SumL {A1} {B1} a1) (SumL {A2} {B2} a2)
+  eq-SumR
+    : ∀ {@0 A1 A2 B1 B2 : Typ}
+      {b1 : Val B1} {b2 : Val B2}
+    → Eq-runtime b1 b2
+    → Eq-runtime (SumR {A1} {B1} b1) (SumR {A2} {B2} b2)
+-}
+
+-- Lemma:
+-- When to values are related by a run-time equality,
+-- we can translate this into a function that maps one into the other.
+
diff --git a/lib/fine-types-core/src/agda/Language/FineTypes/Value/Typcheck.agda b/lib/fine-types-core/src/agda/Language/FineTypes/Value/Typcheck.agda
new file mode 100644
index 0000000..930ca23
--- /dev/null
+++ b/lib/fine-types-core/src/agda/Language/FineTypes/Value/Typcheck.agda
@@ -0,0 +1,204 @@
+module Language.FineTypes.Value.Typcheck where
+
+open import Haskell.Prelude
+    hiding (_×_; _+_; Pair; case_of_; Bool; Integer )
+open import Function.Base
+    using (case_of_)
+
+open import Language.FineTypes.Value.Def
+open import Language.FineTypes.Typ
+    using (Typ)
+
+import Haskell.Prelude as Hs
+import Language.FineTypes.Typ as Typ
+
+{-----------------------------------------------------------------------------
+    Haskell — type checking
+------------------------------------------------------------------------------}
+typOf0 : ∀{@0 A : Typ.TypConst} → ZeroF A -> Typ.TypConst
+typOf0 a = case a of λ where
+    (Bool _) -> Typ.Bool
+--    Bytes _ -> Typ.Bytes
+    (Integer _) -> Typ.Integer
+    (Natural _) -> Typ.Natural
+--    Text _ -> Typ.Text
+    Unit -> Typ.Unit
+--    Rational _ -> Typ.Rational
+
+-- mutually recursive definitions
+hasTyp
+    : ∀{@0 A : Typ} → Value A → Typ → Hs.Bool
+hasTyp1
+    : ∀{@0 A : Typ} {@0 op : Typ.OpOne}
+    → OneF (Value A) op
+    -> Typ.OpOne -> Typ -> Hs.Bool
+hasTyp2
+    : ∀{@0 A B : Typ} {@0 op : Typ.OpTwo}
+    → TwoF (Value A) (Value B) op
+    → Typ.OpTwo -> Typ -> Typ -> Hs.Bool
+
+hasTyp1 (Option v) Typ.Option t =
+    all (λ v → hasTyp v t) v
+hasTyp1 (Option _) _ _ =
+    False
+hasTyp1 (Sequence vs) Typ.Sequence t =
+    all (λ v → hasTyp v t) vs
+hasTyp1 (Sequence _) _ _ =
+    False
+
+hasTyp2 = λ()
+
+hasTyp (Zero a) (Typ.Zero b) =
+    typOf0 a == b
+hasTyp (Zero _) _ =
+    False
+hasTyp (One a) (Typ.One op typ) =
+    hasTyp1 a op typ
+hasTyp (One _) _ =
+    False
+hasTyp (Product2 a b) (Typ.Two Typ.Product2 ta tb) =
+    (hasTyp a ta) && (hasTyp b tb)
+hasTyp (Product2 _ _) _ =
+    False
+hasTyp (Sum2L a) (Typ.Two Typ.Sum2 ta _) =
+    hasTyp a ta
+hasTyp (Sum2L _) _ =
+    False
+hasTyp (Sum2R b) (Typ.Two Typ.Sum2 _ tb) =
+    hasTyp b tb
+hasTyp (Sum2R _) _ =
+    False
+hasTyp (Two a) (Typ.Two op typ1 typ2) =
+    hasTyp2 a op typ1 typ2
+hasTyp (Two _) _ =
+    False
+
+{-# COMPILE AGDA2HS typOf0 #-}
+{-# COMPILE AGDA2HS hasTyp1 #-}
+{-# COMPILE AGDA2HS hasTyp2 #-}
+{-# COMPILE AGDA2HS hasTyp #-}
+
+{-----------------------------------------------------------------------------
+    Agda
+------------------------------------------------------------------------------}
+lemma-hasTyp-accepts-own-Typ
+  : ∀ (A : Typ) (v : Value A)
+  → hasTyp v A ≡ True
+
+lemma-sequence-accepts-own-Typ
+  : ∀ (B : Typ) (vs : List (Value B))
+  → hasTyp
+    (One (Sequence vs))
+    (Typ.One Typ.Sequence B) ≡ True
+
+lemma-sequence-accepts-own-Typ B [] = refl
+lemma-sequence-accepts-own-Typ B (v ∷ vs)
+    rewrite lemma-hasTyp-accepts-own-Typ B v
+    rewrite lemma-sequence-accepts-own-Typ B vs
+    = refl
+
+lemma-hasTyp-accepts-own-Typ (Typ.Zero Typ.Unit) (Zero Unit)
+    = refl
+lemma-hasTyp-accepts-own-Typ (Typ.Zero Typ.Bool) (Zero (Bool _))
+    = refl
+lemma-hasTyp-accepts-own-Typ (Typ.Zero Typ.Integer) (Zero (Integer x))
+    = refl
+lemma-hasTyp-accepts-own-Typ (Typ.Zero Typ.Natural) (Zero (Natural x))
+    = refl
+lemma-hasTyp-accepts-own-Typ (Typ.One Typ.Option A) (One (Option Nothing))
+    = refl
+lemma-hasTyp-accepts-own-Typ (Typ.One Typ.Option A) (One (Option (Just x)))
+    = lemma-hasTyp-accepts-own-Typ A x
+lemma-hasTyp-accepts-own-Typ (Typ.One Typ.Sequence A) (One (Sequence []))
+    = refl
+lemma-hasTyp-accepts-own-Typ (Typ.One Typ.Sequence A) (One (Sequence (v ∷ vs)))
+    rewrite lemma-hasTyp-accepts-own-Typ A v
+    rewrite lemma-sequence-accepts-own-Typ A vs
+    = refl
+lemma-hasTyp-accepts-own-Typ (Typ.Two Typ.Product2 A1 A2) (Product2 v1 v2)
+    rewrite lemma-hasTyp-accepts-own-Typ A1 v1
+    rewrite lemma-hasTyp-accepts-own-Typ A2 v2
+    = refl
+lemma-hasTyp-accepts-own-Typ (Typ.Two Typ.Sum2 A1 A2) (Sum2L v1)
+    = lemma-hasTyp-accepts-own-Typ A1 v1
+lemma-hasTyp-accepts-own-Typ (Typ.Two Typ.Sum2 A1 A2) (Sum2R v2)
+    = lemma-hasTyp-accepts-own-Typ A2 v2
+
+{-----------------------------------------------------------------------------
+    Type checking on the value level
+------------------------------------------------------------------------------}
+{-
+data Typchecks {@0 A : Typ} (va : Val A) (B : Typ) : Set where
+  Checks
+    : (vb : Val B)
+    → Eq-runtime va vb
+    → Typchecks va B
+
+-- | Helper function that recurses into the typ and returns proof.
+checkTyp
+  : ∀ {@0 A : Typ} (v : Val A) (B : Typ)
+  → Maybe (Typchecks v B)
+checkTyp Unit (Zero TUnit) =
+  Just (Checks Unit eq-Unit)
+checkTyp (Pair x y) (Two Product2 X Y) =
+  case (checkTyp x X) of λ
+    { Nothing → Nothing
+    ; (Just (Checks x' ex)) →
+      case (checkTyp y Y) of λ
+        { Nothing → Nothing
+        ; (Just (Checks y' ey)) →
+          Just (Checks (Pair x' y') (eq-Pair ex ey))
+      }
+    }
+checkTyp (SumL x) (Two Sum2 X _) =
+  case (checkTyp x X) of λ
+    { Nothing → Nothing
+    ; (Just (Checks x' ex)) →
+      Just (Checks (SumL x') (eq-SumL ex))
+    }
+checkTyp (SumR y) (Two Sum2 _ Y) =
+  case (checkTyp y Y) of λ
+    { Nothing → Nothing
+    ; (Just (Checks y' ey)) →
+      Just (Checks (SumR y') (eq-SumR ey))
+    }
+checkTyp _ _ = Nothing
+
+
+lemma-upgrade-hasTyp
+  : ∀ {@0 A : Typ} (B : Typ) (va : Val A)
+  → hasTyp va B ≡ isJust (checkTyp va B)
+lemma-upgrade-hasTyp (Zero TUnit) Unit = refl
+lemma-upgrade-hasTyp (Two Product2 A B) (Pair a b)
+  rewrite lemma-upgrade-hasTyp A a
+  rewrite lemma-upgrade-hasTyp B b
+    with checkTyp a A
+... | Nothing = refl
+... | Just (Checks _ _) with checkTyp b B
+...   | Nothing  = refl
+...   | Just (Checks _ _) = refl
+lemma-upgrade-hasTyp (Two Sum2 A _) (SumL a)
+  rewrite lemma-upgrade-hasTyp A a
+    with checkTyp a A
+... | Nothing = refl
+... | (Just (Checks x' ex)) = refl
+lemma-upgrade-hasTyp (Two Sum2 _ B) (SumR b)
+  rewrite lemma-upgrade-hasTyp B b
+    with checkTyp b B
+... | Nothing = refl
+... | (Just (Checks y' ey)) = refl
+lemma-upgrade-hasTyp (Zero TBool) Unit = refl
+lemma-upgrade-hasTyp (Zero TNatural) Unit = refl
+lemma-upgrade-hasTyp (One x B) Unit = refl
+lemma-upgrade-hasTyp (Two x B B₁) Unit = refl
+lemma-upgrade-hasTyp (Zero x) (Pair va va₁) = refl
+lemma-upgrade-hasTyp (One x B) (Pair va va₁) = refl
+lemma-upgrade-hasTyp (Two Sum2 B B₁) (Pair va va₁) = refl
+lemma-upgrade-hasTyp (Zero x) (SumL va) = refl
+lemma-upgrade-hasTyp (One x B) (SumL va) = refl
+lemma-upgrade-hasTyp (Two Product2 B B₁) (SumL va) = refl
+lemma-upgrade-hasTyp (Zero x) (SumR va) = refl
+lemma-upgrade-hasTyp (One x B) (SumR va) = refl
+lemma-upgrade-hasTyp (Two Product2 B B₁) (SumR va) = refl
+
+-}
\ No newline at end of file
diff --git a/lib/fine-types-core/src/haskell/Data/Embedding.hs b/lib/fine-types-core/src/haskell/Data/Embedding.hs
new file mode 100644
index 0000000..65ec12c
--- /dev/null
+++ b/lib/fine-types-core/src/haskell/Data/Embedding.hs
@@ -0,0 +1,7 @@
+module Data.Embedding where
+
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+
+data Embedding a b = Embedding{to :: a -> b, from :: b -> a}
+
diff --git a/lib/fine-types-core/src/haskell/Language/FineTypes.hs b/lib/fine-types-core/src/haskell/Language/FineTypes.hs
new file mode 100644
index 0000000..6d8976f
--- /dev/null
+++ b/lib/fine-types-core/src/haskell/Language/FineTypes.hs
@@ -0,0 +1,5 @@
+module Language.FineTypes where
+
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+
diff --git a/lib/fine-types-core/src/haskell/Language/FineTypes/Embedding.hs b/lib/fine-types-core/src/haskell/Language/FineTypes/Embedding.hs
new file mode 100644
index 0000000..453bf4a
--- /dev/null
+++ b/lib/fine-types-core/src/haskell/Language/FineTypes/Embedding.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE LambdaCase #-}
+module Language.FineTypes.Embedding where
+
+import Data.Embedding (Embedding)
+import Language.FineTypes.Typ (OpTwo(Product2, Sum2), Typ(Two))
+import Language.FineTypes.Value (Val(Pair, SumL, SumR))
+
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+
+data EmbeddingTyp = EmbeddingTyp{embed :: Embedding Val Val,
+                                 typcheck :: Typ -> Maybe Typ}
+
+distributeVal :: Embedding Val Val
+distributeVal
+  = Embedding
+      (\case
+           Pair (SumL a) c -> SumL (Pair a c)
+           Pair (SumR b) c -> SumR (Pair b c))
+      (\case
+           SumL (Pair a c) -> Pair (SumL a) c
+           SumR (Pair b c) -> Pair (SumR b) c)
+
+distribute :: EmbeddingTyp
+distribute
+  = EmbeddingTyp distributeVal
+      (\case
+           Two Product2 (Two Sum2 a b) c -> Just
+                                              (Two Sum2 (Two Product2 a c) (Two Product2 b c))
+           _ -> Nothing)
+
diff --git a/lib/fine-types-core/src/haskell/Language/FineTypes/Typ.hs b/lib/fine-types-core/src/haskell/Language/FineTypes/Typ.hs
new file mode 100644
index 0000000..eddf6af
--- /dev/null
+++ b/lib/fine-types-core/src/haskell/Language/FineTypes/Typ.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE StandaloneDeriving #-}
+module Language.FineTypes.Typ where
+
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+
+type ConstructorName = String
+
+type FieldName = String
+
+type TypName = String
+
+type VarName = String
+
+data TypConst = Bool
+              | Bytes
+              | Integer
+              | Natural
+              | Text
+              | Rational
+              | Unit
+
+data OpOne = Option
+           | Sequence
+           | PowerSet
+
+data OpTwo = Sum2
+           | Product2
+           | PartialFunction
+           | FiniteSupport
+
+data Constraint1 = Braces [Constraint1]
+                 | Token String
+
+type Constraint = [Constraint1]
+
+data Typ = Var TypName
+         | Zero TypConst
+         | One OpOne Typ
+         | Two OpTwo Typ Typ
+         | ProductN [(FieldName, Typ)]
+         | SumN [(ConstructorName, Typ)]
+         | Constrained VarName Typ Constraint
+
+deriving instance Eq TypConst
+
diff --git a/lib/fine-types-core/src/haskell/Language/FineTypes/Value/Def.hs b/lib/fine-types-core/src/haskell/Language/FineTypes/Value/Def.hs
new file mode 100644
index 0000000..92b48cc
--- /dev/null
+++ b/lib/fine-types-core/src/haskell/Language/FineTypes/Value/Def.hs
@@ -0,0 +1,63 @@
+module Language.FineTypes.Value.Def where
+
+import Numeric.Natural (Natural)
+import qualified Prelude as Hs (Bool, False, Integer, True)
+
+data ZeroF = Bool Hs.Bool
+           | Integer Hs.Integer
+           | Natural Natural
+           | Unit
+
+data OneF a = Option (Maybe a)
+            | Sequence [a]
+
+data TwoF a b
+
+type Ix = Int
+
+data Value = Zero ZeroF
+           | One (OneF Value)
+           | Two (TwoF Value Value)
+           | Product2 Value Value
+           | Sum2L Value
+           | Sum2R Value
+
+eqZeroF :: ZeroF -> ZeroF -> Hs.Bool
+eqZeroF (Bool x) (Bool y) = x == y
+eqZeroF (Bool _) _ = Hs.False
+eqZeroF (Integer x) (Integer y) = Hs.True
+eqZeroF (Integer _) _ = Hs.False
+eqZeroF (Natural _) (Natural _) = Hs.True
+eqZeroF (Natural _) _ = Hs.False
+eqZeroF Unit Unit = Hs.False
+eqZeroF Unit _ = Hs.False
+
+eqValue :: Value -> Value -> Hs.Bool
+eqValue (Zero x) (Zero y) = eqZeroF x y
+eqValue (Zero _) _ = Hs.False
+eqValue (One (Option x)) (One (Option y)) = eqMaybeValue x y
+eqValue (One (Option _)) _ = Hs.False
+eqValue (One (Sequence x)) (One (Sequence y)) = eqListValue x y
+eqValue (One (Sequence _)) _ = Hs.False
+eqValue (Two _) (Two _) = Hs.True
+eqValue (Two _) _ = Hs.False
+eqValue (Product2 x1 x2) (Product2 y1 y2)
+  = eqValue x1 y1 && eqValue x2 y2
+eqValue (Product2 _ _) _ = Hs.False
+eqValue (Sum2L x) (Sum2L y) = eqValue x y
+eqValue (Sum2L _) _ = Hs.False
+eqValue (Sum2R x) (Sum2R y) = eqValue x y
+eqValue (Sum2R _) _ = Hs.False
+
+eqMaybeValue :: Maybe Value -> Maybe Value -> Hs.Bool
+eqMaybeValue (Just x) (Just y) = eqValue x y
+eqMaybeValue (Just _) _ = Hs.False
+eqMaybeValue Nothing Nothing = Hs.True
+eqMaybeValue Nothing _ = Hs.False
+
+eqListValue :: [Value] -> [Value] -> Hs.Bool
+eqListValue (x : xs) (y : ys) = eqValue x y && eqListValue xs ys
+eqListValue (_ : _) _ = Hs.False
+eqListValue [] [] = Hs.True
+eqListValue [] _ = Hs.False
+