bidir paper

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) = {!   !}

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

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