Add substitutions renamings and their semantics

docs/Agda.css

@@ -372,3 +372,9 @@ h6 {
     border-radius: .2em;
     background-color: #650099
 }
+@import url('https://fonts.googleapis.com/css2?family=Fira+Mono&display=swap');
+
+pre {
+  font-family: 'Fira Mono', monospace;
+  font-size: 10pt;
+}

realizability.agda-lib

@@ -1,4 +1,4 @@
 name: realizability
 depend: cubical
 include: src
-flags: --cubical
+flags: --cubical  -WnoUnsupportedIndexedMatch

src/Realizability/Tripos/Everything.agda

@@ -3,3 +3,5 @@ open import Realizability.Tripos.Predicate
 open import Realizability.Tripos.Algebra
 open import Realizability.Tripos.Algebra.Base
 open import Realizability.Tripos.Prealgebra.Everything
+open import Realizability.Tripos.Logic.Syntax
+open import Realizability.Tripos.Logic.Semantics

src/Realizability/Tripos/Logic/Semantics.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Realizability.CombinatoryAlgebra
 open import Realizability.ApplicativeStructure renaming (Term to ApplStrTerm)
 open import Cubical.Foundations.Prelude
@@ -30,14 +31,15 @@ open import Realizability.Tripos.Logic.Syntax {ℓ = ℓ'}
 open CombinatoryAlgebra ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
 open Predicate'
-open PredicateProperties
+open PredicateProperties hiding (_≤_ ; isTrans≤)
 open Morphism {ℓ' = ℓ'} {ℓ'' = ℓ''}
 Predicate = Predicate' {ℓ' = ℓ'} {ℓ'' = ℓ''}
-
+RelationInterpretation : ∀ {n : ℕ} → (Vec Sort n) → Type _
+RelationInterpretation {n} relSym = (∀ i →  Predicate ⟨ ⟦ lookup i relSym ⟧ˢ ⟩)
 module Interpretation
   {n : ℕ}
   (relSym : Vec Sort n)
-  (⟦_⟧ʳ : ∀ i → Predicate (⟦ lookup i relSym ⟧ˢ .fst)) (isNonTrivial : s ≡ k → ⊥) where
+  (⟦_⟧ʳ : RelationInterpretation relSym) (isNonTrivial : s ≡ k → ⊥) where
   open Relational relSym
 
   ⟦_⟧ᶜ : Context → hSet ℓ'
@@ -102,3 +104,84 @@ module Interpretation
     fst
     (⟦ f ⟧ᶠ)
   ⟦_⟧ᶠ {Γ ′ x} (rel R t) = ⋆_ (str ⟦ Γ ′ x ⟧ᶜ) (str ⟦ lookup R relSym ⟧ˢ) ⟦ t ⟧ᵗ ⟦ R ⟧ʳ
+
+  -- R for renamings and r for relations
+  ⟦_⟧ᴿ : ∀ {Γ Δ} → Renaming Γ Δ → ⟨ ⟦ Γ ⟧ᶜ ⟩ → ⟨ ⟦ Δ ⟧ᶜ ⟩
+  ⟦ id ⟧ᴿ ctx = ctx
+  ⟦ drop ren ⟧ᴿ (ctx , _) = ⟦ ren ⟧ᴿ ctx
+  ⟦ keep ren ⟧ᴿ (ctx , s) = (⟦ ren ⟧ᴿ ctx) , s
+
+  -- B for suBstitution and s for sorts
+  ⟦_⟧ᴮ : ∀ {Γ Δ} → Substitution Γ Δ → ⟨ ⟦ Γ ⟧ᶜ ⟩ → ⟨ ⟦ Δ ⟧ᶜ ⟩
+  ⟦ id ⟧ᴮ ctx = ctx
+  ⟦ t , sub ⟧ᴮ ctx = (⟦ sub ⟧ᴮ ctx) , (⟦ t ⟧ᵗ ctx)
+  ⟦ drop sub ⟧ᴮ (ctx , s) = ⟦ sub ⟧ᴮ ctx
+
+  renamingVarSound : ∀ {Γ Δ s} → (ren : Renaming Γ Δ) → (v : s ∈ Δ) → ⟦ renamingVar ren v ⟧ⁿ ≡ ⟦ v ⟧ⁿ ∘ ⟦ ren ⟧ᴿ
+  renamingVarSound {Γ} {.Γ} {s} id v = refl
+  renamingVarSound {.(_ ′ _)} {Δ} {s} (drop ren) v = funExt λ { (⟦Γ⟧ , ⟦s⟧) i → renamingVarSound ren v i ⟦Γ⟧ }
+  renamingVarSound {.(_ ′ s)} {.(_ ′ s)} {s} (keep ren) here = funExt λ { (⟦Γ⟧ , ⟦s⟧) i → ⟦s⟧ }
+  renamingVarSound {.(_ ′ _)} {.(_ ′ _)} {s} (keep ren) (there v) = funExt λ { (⟦Γ⟧ , ⟦s⟧) i → renamingVarSound ren v i ⟦Γ⟧ }
+
+  renamingTermSound : ∀ {Γ Δ s} → (ren : Renaming Γ Δ) → (t : Term Δ s) → ⟦ renamingTerm ren t ⟧ᵗ ≡ ⟦ t ⟧ᵗ ∘ ⟦ ren ⟧ᴿ
+  renamingTermSound {Γ} {.Γ} {s} id t = refl
+  renamingTermSound {.(_ ′ _)} {Δ} {s} (drop ren) (var x) = funExt λ { (⟦Γ⟧ , ⟦s⟧) i → renamingVarSound ren x i ⟦Γ⟧ }
+  renamingTermSound {.(_ ′ _)} {Δ} {.(_ `× _)} r@(drop ren) (t `, t₁) = funExt λ { (⟦Γ⟧ , ⟦s⟧) i → renamingTermSound r t i (⟦Γ⟧ , ⟦s⟧) , renamingTermSound r t₁ i (⟦Γ⟧ , ⟦s⟧) }
+  renamingTermSound {.(_ ′ _)} {Δ} {s} r@(drop ren) (π₁ t) = funExt λ { x@(⟦Γ⟧ , ⟦s⟧) i → renamingTermSound r t i x .fst }
+  renamingTermSound {.(_ ′ _)} {Δ} {s} r@(drop ren) (π₂ t) = funExt λ { x@(⟦Γ⟧ , ⟦s⟧) i → renamingTermSound r t i x .snd }
+  renamingTermSound {.(_ ′ _)} {Δ} {s} r@(drop ren) (fun f t) = funExt λ { x@(⟦Γ⟧ , ⟦s⟧) i → f (renamingTermSound r t i x) }
+  renamingTermSound {.(_ ′ _)} {.(_ ′ _)} {s} r@(keep ren) (var v) = funExt λ { x@(⟦Γ⟧ , ⟦s⟧) i → renamingVarSound r v i x }
+  renamingTermSound {.(_ ′ _)} {.(_ ′ _)} {.(_ `× _)} r@(keep ren) (t `, t₁) = funExt λ { x@(⟦Γ⟧ , ⟦s⟧) i → (renamingTermSound r t i x) , (renamingTermSound r t₁ i x) }
+  renamingTermSound {.(_ ′ _)} {.(_ ′ _)} {s} r@(keep ren) (π₁ t) = funExt λ { x@(⟦Γ⟧ , ⟦s⟧) i → renamingTermSound r t i x .fst }
+  renamingTermSound {.(_ ′ _)} {.(_ ′ _)} {s} r@(keep ren) (π₂ t) = funExt λ { x@(⟦Γ⟧ , ⟦s⟧) i → renamingTermSound r t i x .snd }
+  renamingTermSound {.(_ ′ _)} {.(_ ′ _)} {s} r@(keep ren) (fun f t) = funExt λ { x@(⟦Γ⟧ , ⟦s⟧) i → f (renamingTermSound r t i x) }
+
+  substitutionVarSound : ∀ {Γ Δ s} → (subs : Substitution Γ Δ) → (v : s ∈ Δ) → ⟦ substitutionVar subs v ⟧ᵗ ≡ ⟦ v ⟧ⁿ ∘ ⟦ subs ⟧ᴮ
+  substitutionVarSound {Γ} {.Γ} {s} id t = refl
+  substitutionVarSound {Γ} {.(_ ′ s)} {s} (t' , subs) here = funExt λ ⟦Γ⟧ → refl
+  substitutionVarSound {Γ} {.(_ ′ _)} {s} (t' , subs) (there t) = funExt λ ⟦Γ⟧ i → substitutionVarSound subs t i ⟦Γ⟧
+  substitutionVarSound {.(_ ′ _)} {Δ} {s} r@(drop subs) t =
+    -- TODO : Fix unsolved constraints
+    funExt
+      λ { x@(⟦Γ⟧ , ⟦s⟧) →
+        ⟦ substitutionVar (drop subs) t ⟧ᵗ (⟦Γ⟧ , ⟦s⟧)
+          ≡[ i ]⟨  renamingTermSound (drop id) (substitutionVar subs t) i (⟦Γ⟧ , ⟦s⟧)  ⟩
+        ⟦ substitutionVar subs t ⟧ᵗ (⟦ drop id ⟧ᴿ x)
+          ≡⟨ refl ⟩
+        ⟦ substitutionVar subs t ⟧ᵗ ⟦Γ⟧
+          ≡[ i ]⟨ substitutionVarSound subs t i ⟦Γ⟧ ⟩
+        ⟦ t ⟧ⁿ (⟦ subs ⟧ᴮ ⟦Γ⟧)
+          ∎}
+
+  substitutionTermSound : ∀ {Γ Δ s} → (subs : Substitution Γ Δ) → (t : Term Δ s) → ⟦ substitutionTerm subs t ⟧ᵗ ≡ ⟦ t ⟧ᵗ ∘ ⟦ subs ⟧ᴮ
+  substitutionTermSound {Γ} {Δ} {s} subs (var x) = substitutionVarSound subs x
+  substitutionTermSound {Γ} {Δ} {.(_ `× _)} subs (t `, t₁) = funExt λ x i → (substitutionTermSound subs t i x) , (substitutionTermSound subs t₁ i x)
+  substitutionTermSound {Γ} {Δ} {s} subs (π₁ t) = funExt λ x i → substitutionTermSound subs t i x .fst
+  substitutionTermSound {Γ} {Δ} {s} subs (π₂ t) = funExt λ x i → substitutionTermSound subs t i x .snd
+  substitutionTermSound {Γ} {Δ} {s} subs (fun f t) = funExt λ x i → f (substitutionTermSound subs t i x)
+
+module Soundness
+  {n}
+  {relSym : Vec Sort n}
+  (isNonTrivial : s ≡ k → ⊥)
+  (⟦_⟧ʳ : RelationInterpretation relSym) where
+  open Relational relSym
+  open Interpretation relSym ⟦_⟧ʳ isNonTrivial
+
+  infix 24 _⊨_
+
+  module _ {Γ : Context} where
+
+    open PredicateProperties {ℓ'' = ℓ''} ⟨ ⟦ Γ ⟧ᶜ ⟩
+
+    _⊨_ : Formula Γ → Formula Γ → Type _
+    ϕ ⊨ ψ = ⟦ ϕ ⟧ᶠ ≤ ⟦ ψ ⟧ᶠ
+
+    private
+      variable
+        ϕ ψ θ χ : Formula Γ
+
+    cut : ∀ {ϕ ψ θ} → ϕ ⊨ ψ → ψ ⊨ θ → ϕ ⊨ θ
+    cut {ϕ} {ψ} {θ} ϕ⊨ψ ψ⊨θ = isTrans≤ ⟦ ϕ ⟧ᶠ ⟦ ψ ⟧ᶠ ⟦ θ ⟧ᶠ ϕ⊨ψ ψ⊨θ
+
+

src/Realizability/Tripos/Logic/Syntax.agda

@@ -32,6 +32,59 @@ data Term : Context → Sort → Type (ℓ-suc ℓ) where
   π₂ : ∀ {Γ A B} → Term Γ (A `× B) → Term Γ B
   fun : ∀ {Γ A B} → (⟦ A ⟧ˢ .fst → ⟦ B ⟧ˢ .fst) → Term Γ A → Term Γ B
 
+data Renaming : Context → Context → Type (ℓ-suc ℓ) where
+  id : ∀ {Γ} → Renaming Γ Γ
+  drop : ∀ {Γ Δ s} → Renaming Γ Δ → Renaming (Γ ′ s) Δ
+  keep : ∀ {Γ Δ s} → Renaming Γ Δ → Renaming (Γ ′ s) (Δ ′ s)
+
+data Substitution : Context → Context → Type (ℓ-suc ℓ) where
+  id : ∀ {Γ} → Substitution Γ Γ
+  _,_ : ∀ {Γ Δ s} → (t : Term Γ s) → Substitution Γ Δ → Substitution Γ (Δ ′ s)
+  drop : ∀ {Γ Δ s} → Substitution Γ Δ → Substitution (Γ ′ s) Δ
+
+terminatingSubstitution : ∀ {Γ} → Substitution Γ []
+terminatingSubstitution {[]} = id
+terminatingSubstitution {Γ ′ x} = drop terminatingSubstitution
+
+renamingCompose : ∀ {Γ Δ Θ} → Renaming Γ Δ → Renaming Δ Θ → Renaming Γ Θ
+renamingCompose {Γ} {.Γ} {Θ} id Δ→Θ = Δ→Θ
+renamingCompose {.(_ ′ _)} {Δ} {Θ} (drop Γ→Δ) Δ→Θ = drop (renamingCompose Γ→Δ Δ→Θ)
+renamingCompose {.(_ ′ _)} {.(_ ′ _)} {.(_ ′ _)} (keep Γ→Δ) id = keep Γ→Δ
+renamingCompose {.(_ ′ _)} {.(_ ′ _)} {Θ} (keep Γ→Δ) (drop Δ→Θ) = drop (renamingCompose Γ→Δ Δ→Θ)
+renamingCompose {.(_ ′ _)} {.(_ ′ _)} {.(_ ′ _)} (keep Γ→Δ) (keep Δ→Θ) = keep (renamingCompose Γ→Δ Δ→Θ)
+
+renamingVar : ∀ {Γ Δ s} → Renaming Γ Δ → s ∈ Δ → s ∈ Γ
+renamingVar {Γ} {.Γ} {s} id s∈Δ = s∈Δ
+renamingVar {.(_ ′ _)} {Δ} {s} (drop ren) s∈Δ = there (renamingVar ren s∈Δ)
+renamingVar {.(_ ′ s)} {.(_ ′ s)} {s} (keep ren) here = here
+renamingVar {.(_ ′ _)} {.(_ ′ _)} {s} (keep ren) (there s∈Δ) = there (renamingVar ren s∈Δ)
+
+renamingTerm : ∀ {Γ Δ s} → Renaming Γ Δ → Term Δ s → Term Γ s
+renamingTerm {Γ} {.Γ} {s} id term = term
+renamingTerm {.(_ ′ _)} {Δ} {s} (drop ren) (var x) = var (renamingVar (drop ren) x)
+renamingTerm {.(_ ′ _)} {Δ} {.(_ `× _)} (drop ren) (term `, term₁) = renamingTerm (drop ren) term `, renamingTerm (drop ren) term₁
+renamingTerm {.(_ ′ _)} {Δ} {s} (drop ren) (π₁ term) = π₁ (renamingTerm (drop ren) term)
+renamingTerm {.(_ ′ _)} {Δ} {s} (drop ren) (π₂ term) = π₂ (renamingTerm (drop ren) term)
+renamingTerm {.(_ ′ _)} {Δ} {s} (drop ren) (fun f term) = fun f (renamingTerm (drop ren) term)
+renamingTerm {.(_ ′ _)} {.(_ ′ _)} {s} (keep ren) (var x) = var (renamingVar (keep ren) x)
+renamingTerm {.(_ ′ _)} {.(_ ′ _)} {.(_ `× _)} (keep ren) (term `, term₁) = renamingTerm (keep ren) term `, renamingTerm (keep ren) term₁
+renamingTerm {.(_ ′ _)} {.(_ ′ _)} {s} (keep ren) (π₁ term) = π₁ (renamingTerm (keep ren) term)
+renamingTerm {.(_ ′ _)} {.(_ ′ _)} {s} (keep ren) (π₂ term) = π₂ (renamingTerm (keep ren) term)
+renamingTerm {.(_ ′ _)} {.(_ ′ _)} {s} (keep ren) (fun f term) = fun f (renamingTerm (keep ren) term)
+
+substitutionVar : ∀ {Γ Δ s} → Substitution Γ Δ → s ∈ Δ → Term Γ s
+substitutionVar {Γ} {.Γ} {s} id s∈Δ = var s∈Δ
+substitutionVar {Γ} {.(_ ′ s)} {s} (t , subs) here = t
+substitutionVar {Γ} {.(_ ′ _)} {s} (t , subs) (there s∈Δ) = substitutionVar subs s∈Δ
+substitutionVar {.(_ ′ _)} {Δ} {s} (drop subs) s∈Δ = renamingTerm (drop id) (substitutionVar subs s∈Δ)
+
+substitutionTerm : ∀ {Γ Δ s} → Substitution Γ Δ → Term Δ s → Term Γ s
+substitutionTerm {Γ} {Δ} {s} subs (var x) = substitutionVar subs x
+substitutionTerm {Γ} {Δ} {.(_ `× _)} subs (t `, t₁) = substitutionTerm subs t `, substitutionTerm subs t₁
+substitutionTerm {Γ} {Δ} {s} subs (π₁ t) = π₁ (substitutionTerm subs t)
+substitutionTerm {Γ} {Δ} {s} subs (π₂ t) = π₂ (substitutionTerm subs t)
+substitutionTerm {Γ} {Δ} {s} subs (fun x t) = fun x (substitutionTerm subs t)
+
 module Relational {n} (relSym : Vec Sort n) where
 
  data Formula : Context → Type (ℓ-suc ℓ) where
@@ -44,3 +97,4 @@ module Relational {n} (relSym : Vec Sort n) where
    `∃ : ∀ {Γ B} → Formula (Γ ′ B) → Formula Γ
    `∀ : ∀ {Γ B} → Formula (Γ ′ B) → Formula Γ
    rel : ∀ {Γ} (k : Fin n) → Term Γ (lookup k relSym) → Formula Γ
+

src/index.agda

@@ -9,3 +9,6 @@ open import Realizability.ApplicativeStructure
 open import Realizability.Assembly.Everything
 open import Realizability.Tripos.Everything
 open import Realizability.Choice
+open import Tripoi.Tripos
+open import Tripoi.HeytingAlgebra
+open import Tripoi.PosetReflection