InternalLanguage.agda

{-# OPTIONS --universe-polymorphism #-}

-- this agda module depends on https://github.com/copumpkin/categories

open import Categories.Category

module Categories.InternalLanguage {o ℓ e} (C : Category o ℓ e) where

open Category C
open Equiv

open import Categories.Morphisms using (Iso)

open import Level using (_⊔_; Lift; lift)
open import Data.Nat using (ℕ)
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec using (Vec; lookup; _∷_; [])
open import Data.Unit using (⊤)
open import Data.Product

Ctx : ℕ → Set o
Ctx = Vec Obj

data Term {n} (Γ : Ctx n) : Obj → Obj → Set (o ⊔ ℓ ⊔ e) where
  Lit : {I Y : Obj} → (f : I ⇒ Y) → Term Γ I Y
  Var : {I Y : Obj} → (v : Fin n) → (f : lookup v Γ ⇒ Y) → Term Γ I Y

-- Closed terms
CTerm : Obj → Obj → Set (o ⊔ ℓ ⊔ e)
CTerm = Term []

var : ∀ {I n} {Γ : Ctx n} → (v : Fin n) → Term Γ I (lookup v Γ)
var {I} {n} {Γ} v = Var v id

data Bindings : ∀ {n} (Γ : Ctx n) → Obj → Set (o ⊔ ℓ ⊔ e) where
  BNil : ∀ {I} → Bindings [] I
  BCons : ∀ {I X n Γ} → (I ⇒ X) → Bindings {n} Γ I → Bindings (X ∷ Γ) I

lookupBindings : ∀ {I n Γ} → (v : Fin n) → Bindings Γ I → (I ⇒ lookup v Γ)
lookupBindings Data.Fin.zero (BCons f _) = f
lookupBindings (Data.Fin.suc v) (BCons _ bs) = lookupBindings v bs

pullbackBindings : ∀ {K I n} {Γ : Ctx n} → (K ⇒ I) → Bindings Γ I → Bindings Γ K
pullbackBindings g BNil = BNil
pullbackBindings g (BCons f bs) = BCons (f ∘ g) (pullbackBindings g bs)

_**_ : ∀ {K I n} {Γ : Ctx n} → (K ⇒ I) → Bindings Γ I → Bindings Γ K
_**_ = pullbackBindings

closeTerm : ∀ {I Y n} {Γ : Ctx n} → Bindings Γ I → Term Γ I Y → (I ⇒ Y)
closeTerm bs (Lit f) = f
closeTerm bs (Var v f) = f ∘ lookupBindings v bs

pullbackTerm : ∀ {K I Y n} {Γ : Ctx n} → (K ⇒ I) → Term Γ I Y → Term Γ K Y
pullbackTerm g (Lit f) = Lit (f ∘ g)
pullbackTerm g (Var v f) = Var v f

_*_ : ∀ {K I Y n} {Γ : Ctx n} → (K ⇒ I) → Term Γ I Y → Term Γ K Y
_*_ = pullbackTerm

data Formula {n} (Γ : Ctx n) : Obj → Set (o ⊔ ℓ ⊔ e) where
  _≡≡_ : {I X : Obj} → (x y : Term Γ I X) → Formula Γ I
  ⊤⊤ : ∀ {I} → Formula Γ I
  _∧∧_ : ∀ {I} → (φ ψ : Formula Γ I) → Formula Γ I
  _⇒⇒_ : ∀ {I} → (φ ψ : Formula Γ I) → Formula Γ I
  ∀∀_,_ : ∀ {I} (X : Obj) → Formula (X ∷ Γ) I → Formula Γ I
  ∃∃_,_ : ∀ {I} (X : Obj) → Formula (X ∷ Γ) I → Formula Γ I

-- Closed formulas
CFormula : Obj → Set (o ⊔ ℓ ⊔ e)
CFormula = Formula []

Epi : ∀ {B A} → (f : A ⇒ B) → Set (o ⊔ ℓ ⊔ e)
Epi {B} f = ∀ {C} → (g₁ g₂ : B ⇒ C) → g₁ ∘ f ≡ g₂ ∘ f → g₁ ≡ g₂

interp : ∀ {I n} {Γ : Ctx n} → (K : Obj) → (K ⇒ I) → Bindings Γ K → Formula Γ I → Set (o ⊔ ℓ ⊔ e)
interp I q bs (x ≡≡ y) = Lift {e} {o ⊔ ℓ} (closeTerm bs (q * x) ≡ closeTerm bs (q * y))
interp I q bs ⊤⊤ = Lift ⊤
interp I q bs (φ ∧∧ ψ) = (interp I q bs φ) × (interp I q bs ψ)
interp I q bs (φ ⇒⇒ ψ) = ∀ {J} (p : J ⇒ I) → (interp J (q ∘ p) (p ** bs) φ)
                                            → (interp J (q ∘ p) (p ** bs) ψ)
interp I q bs (∀∀ X , ψ) = ∀ {J} (p : J ⇒ I) → (x : J ⇒ X) → interp J (q ∘ p) (BCons x (p ** bs)) ψ
interp I q bs (∃∃ X , ψ) = Σ Obj (λ J → Σ (J ⇒ I) (λ p → Σ (J ⇒ X) (λ x →
                                Epi p × interp J (q ∘ p) (BCons x (p ** bs)) ψ)))

_⊧_ : (I : Obj) → CFormula I → Set (o ⊔ ℓ ⊔ e)
I ⊧ φ = interp I id BNil φ

-- I ⊧ ∀ (x : X). x = x
.pReflexivity : ∀ {I X} → I ⊧ (∀∀ X , (var zero ≡≡ var zero))
pReflexivity p x = lift refl

-- help lemma
.idEpi : ∀ {X} → Epi (id {X})
idEpi f g eq = trans (sym identityʳ) (trans eq identityʳ)

-- I ⊧ ∀ (x : X). ∃ (y : X). x = y
.pEasy : ∀ {I X} → I ⊧ (∀∀ X , (∃∃ X , (var zero ≡≡ var (suc zero))))
pEasy {I} {X} {J} p x = J , id , x , idEpi , lift (trans identityˡ (sym (trans identityˡ identityʳ)))