From 39e38719bff94c80f79c7c62793db1edd59bdae7 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Fri, 6 Oct 2023 02:22:44 -0400
Subject: [PATCH] bidir paper

---
 src/2023-10-05-bidir.agda      | 35 ++++++++++++++++++++++++++++++++++
 src/HottBook/Chapter2.lagda.md |  3 ---
 src/HottBook/Common.agda       |  4 +++-
 3 files changed, 38 insertions(+), 4 deletions(-)
 create mode 100644 src/2023-10-05-bidir.agda

diff --git a/src/2023-10-05-bidir.agda b/src/2023-10-05-bidir.agda
new file mode 100644
index 0000000..13d92fa
--- /dev/null
+++ b/src/2023-10-05-bidir.agda
@@ -0,0 +1,35 @@
+open import Data.Nat
+open import Data.Unit
+open import Data.String
+
+data Type : Set
+
+data Term : Set where
+  VarTerm : String → Term
+  UnitTerm : Term
+  Lambda : String → Term → Term
+  AppTerm : Term → Term → Term
+  AnnotTerm : Term → Type → Term
+
+data Type where
+  UnitType : Type
+  VarType : String → Type
+  UniversalType : Type → Type
+  ArrowType : Type → Type → Type
+
+data Context : Set where
+  NilContext : Context
+
+check : (Ψ : Context) → (e : Term) → (A : Type) → ⊤
+check Ψ (VarTerm x) A = {!   !}
+check Ψ UnitTerm A = {!   !}
+check Ψ (Lambda x e) A = {!   !}
+check Ψ (AppTerm e e₁) A = {!   !}
+check Ψ (AnnotTerm e x) A = {!   !}
+
+synthesize : (Ψ : Context) → (e : Term) → Type
+synthesize Ψ (VarTerm x) = {!   !}
+synthesize _ UnitTerm = UnitType
+synthesize Ψ (Lambda x e) = {!   !}
+synthesize Ψ (AppTerm e e₁) = {!   !}
+synthesize Ψ (AnnotTerm e x) = {!   !}
\ No newline at end of file
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index b194e8b..d3e3820 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -10,9 +10,6 @@ open import HottBook.Common
 open import HottBook.Chapter1
 ```
 
-> An internal error has occurred. Please report this as a bug.
-> Location of the error: `__IMPOSSIBLE__`, called at src/full/Agda/Interaction/Imports.hs:915:15 in Agd-2.6.3-d4728884:Agda.Interaction.Imports
-
 ## 2.2 Functions are functors
 
 ### Lemma 2.2.1
diff --git a/src/HottBook/Common.agda b/src/HottBook/Common.agda
index 2e0f4db..015c173 100644
--- a/src/HottBook/Common.agda
+++ b/src/HottBook/Common.agda
@@ -1,4 +1,6 @@
-open import Relation.Binary.PropositionalEquality
+module HottBook.Common where
+
+open import Relation.Binary.PropositionalEquality using (trans)
 
 Type = Set