initial agda code with Owen's pseudocode from the Geolog lectures, and some universe library code from Escardo's book

.gitignore

@@ -23,7 +23,4 @@ cabal.project.local~
 .HTF/
 .ghc.environment.*
 
-# ---> Agda
-*.agdai
-MAlonzo/**
 

agda-experiments/.gitignore

@@ -0,0 +1,4 @@
+# ---> Agda
+*.agdai
+MAlonzo/**
+

agda-experiments/Owen.agda

@@ -0,0 +1,98 @@
+{-# OPTIONS --guardedness #-}
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Data.Unit
+open import Data.Bool using (Bool)
+import Data.Bool as Bool
+open import Data.Fin using (Fin)
+import Data.Fin as Fin
+open import Data.Nat
+open import Relation.Nullary.Decidable using (Dec)
+
+module Owen where
+
+data Con (S : Set) : Set where
+  • : Con S
+  _▷_ : Con S -> S -> Con S
+
+data Var {S : Set} : Con S -> S -> Set where
+  q : {A : S} -> {Γ : Con S} -> Var (Γ ▷ A) A
+  p_ : {A B : S} -> {Γ : Con S} -> Var Γ A -> Var (Γ ▷ B) A
+
+module RegularLogic (Sort : Set) (Rel : Con Sort -> Set) where
+  variable Γ Δ : Con Sort
+  variable A B : Sort
+  Tm = Var
+  Sub : Con Sort -> Con Sort -> Set
+  Sub Γ Δ = (A : Sort) -> Tm Δ A -> Tm Γ A
+
+  data Prop : Con Sort -> Set where
+    true : Prop Γ
+    _$_ : Rel Δ -> Sub Γ Δ -> Prop Γ
+    _∧_ : Prop Γ -> Prop Γ -> Prop Γ
+    _===_ : Tm Γ A -> Tm Γ A -> Prop Γ
+    ∃ : Prop (Γ ▷ A) -> Prop Γ
+
+  record Axiom : Set where
+    field
+      con : Con Sort
+      ante : Prop con
+      cons : Prop con
+
+record Sig : Set where
+  field
+    sorts : Con ⊤
+    rels : Con (Con (Var sorts tt))
+
+Sort : (S : Sig) -> Set
+Sort S = Var (Sig.sorts S) tt
+
+Rel : (S : Sig) -> Con (Sort S) -> Set
+Rel S = Var (Sig.rels S)
+
+record Theory : Set where
+  field
+    sig : Sig
+    axioms : Con (RegularLogic.Axiom (Sort sig) (Rel sig))
+
+Tuple : (S : Sig) -> (Sort S -> ℕ) -> Con (Sort S) -> Set
+Tuple S elts Γ = (A : Sort S) -> Var Γ A -> Fin (elts A)
+
+record ModelData (S : Sig) : Set where
+  field
+    elts : Sort S -> ℕ
+    sat : {Γ : Con (Sort S)} -> Rel S Γ -> Tuple S elts Γ -> Bool
+
+module Interp (S : Sig) (M : ModelData S) where
+  open RegularLogic (Sort S) (Rel S)
+  t = Tuple S (ModelData.elts M)
+
+  Elt : Sort S -> Set
+  Elt A = Fin (ModelData.elts M A)
+
+  extend : (Γ : Con (Sort S)) -> t Γ -> (A : Sort S) -> Elt A -> t (Γ ▷ A)
+  extend = {!!}
+
+  any : {n : ℕ} -> (Fin n -> Bool) -> Bool
+  any = {!!}
+
+  allTuples : (Γ : Con (Sort S)) -> (t Γ -> Bool) -> Bool
+  allTuples = {!!}
+
+  eval : {Γ : Con (Sort S)} -> {A : Sort S} -> Tm Γ A -> t Γ -> Elt A
+  eval {Γ} {A} v f = f A v
+
+  evalSub : {Γ Δ : Con (Sort S)} -> Sub Γ Δ -> t Γ -> t Δ
+  evalSub s f A v = f A (s A v)
+
+  interp : {Γ : Con (Sort S)} -> Prop Γ -> t Γ -> Bool
+  interp true _ = Bool.true
+  interp (r $ xs) f = ModelData.sat M r (evalSub xs f)
+  interp (ϕ ∧ ψ) f = interp ϕ f Bool.∧ interp ψ f
+  interp (x₁ === x₂) f = Dec.does (eval x₁ f Fin.≟ eval x₂ f)
+  interp (∃ {Γ} {A} ϕ) f = any (λ i -> interp ϕ (extend Γ f A i))
+
+  satisfies : Axiom -> Bool
+  satisfies a = allTuples
+    (Axiom.con a)
+    (λ f -> Dec.does (interp (Axiom.ante a) f Bool.≤? interp (Axiom.cons a) f))