Prove that weakening of relational context preserves realizers

rahulc29 · Feb 8, 2024 · 1019d79 · 1019d79
1 parent 0a0ef50
commit 1019d79
Show file tree

Hide file tree

Showing 3 changed files with 58 additions and 18 deletions.
diff --git a/src/Realizability/Tripos/Logic/RelContextStructural.agda b/src/Realizability/Tripos/Logic/RelContextStructural.agda
@@ -1,6 +1,7 @@
 {-# OPTIONS --lossy-unification #-}
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Univalence
 open import Cubical.Data.Vec
 open import Cubical.Data.Nat
 open import Cubical.Data.FinData
@@ -34,7 +35,6 @@ module WeakenSyntax
   transportAlongWeakening {Γ} (form Relational.`∨ form₁) = transportAlongWeakening form SyntaxΞR.`∨ transportAlongWeakening form₁
   transportAlongWeakening {Γ} (form Relational.`∧ form₁) = transportAlongWeakening form SyntaxΞR.`∧ transportAlongWeakening form₁
   transportAlongWeakening {Γ} (form Relational.`→ form₁) = transportAlongWeakening form SyntaxΞR.`→ transportAlongWeakening form₁
-  transportAlongWeakening {Γ} (Relational.`¬ form) = SyntaxΞR.`¬ transportAlongWeakening form
   transportAlongWeakening {Γ} (Relational.`∃ form) = SyntaxΞR.`∃ (transportAlongWeakening form)
   transportAlongWeakening {Γ} (Relational.`∀ form) = SyntaxΞR.`∀ (transportAlongWeakening form)
   transportAlongWeakening {Γ} (Relational.rel k x) = SyntaxΞR.rel (suc k) x
@@ -74,8 +74,22 @@ module WeakenSemantics
     module SoundnessΞ = Soundness {relSym = Ξ} isNonTrivial Ξsem
     module SoundnessΞR = Soundness {relSym = R ∷ Ξ} isNonTrivial RΞsem
 
-    syntacticTransportPreservesRealizers⁺ : ∀ {Γ} → (γ : ⟨ ⟦ Γ ⟧ᶜ ⟩) → (r : A) → (f : ΞFormula Γ) → ∣ InterpretationΞ.⟦ f ⟧ᶠ ∣ γ r → r ⊩ ∣ InterpretationΞR.⟦ transportAlongWeakening f ⟧ᶠ ∣ γ
-    syntacticTransportPreservesRealizers⁻ : ∀ {Γ} → (γ : ⟨ ⟦ Γ ⟧ᶜ ⟩) → (r : A) → (f : ΞFormula Γ) → r ⊩ ∣ InterpretationΞR.⟦ transportAlongWeakening f ⟧ᶠ ∣ γ → r ⊩ ∣ InterpretationΞ.⟦ f ⟧ᶠ ∣ γ
+    syntacticTransportPreservesRealizers⁺ :
+      ∀ {Γ}
+      → (γ : ⟨ ⟦ Γ ⟧ᶜ ⟩)
+      → (r : A)
+      → (f : ΞFormula Γ)
+      → ∣ InterpretationΞ.⟦ f ⟧ᶠ ∣ γ r
+      -------------------------------------------------------------
+      → r ⊩ ∣ InterpretationΞR.⟦ transportAlongWeakening f ⟧ᶠ ∣ γ
+    syntacticTransportPreservesRealizers⁻ :
+      ∀ {Γ}
+      → (γ : ⟨ ⟦ Γ ⟧ᶜ ⟩)
+      → (r : A)
+      → (f : ΞFormula Γ)
+      → r ⊩ ∣ InterpretationΞR.⟦ transportAlongWeakening f ⟧ᶠ ∣ γ
+      -------------------------------------------------------------
+      → r ⊩ ∣ InterpretationΞ.⟦ f ⟧ᶠ ∣ γ
 
     syntacticTransportPreservesRealizers⁺ {Γ} γ r Relational.⊤ᵗ r⊩⟦f⟧Ξ = r⊩⟦f⟧Ξ
     syntacticTransportPreservesRealizers⁺ {Γ} γ r (f Relational.`∨ f₁) r⊩⟦f⟧Ξ =
@@ -87,7 +101,6 @@ module WeakenSemantics
       syntacticTransportPreservesRealizers⁺ γ (pr₂ ⨾ r) f₁ pr₂r⊩⟦f₁⟧
     syntacticTransportPreservesRealizers⁺ {Γ} γ r (f Relational.`→ f₁) r⊩⟦f⟧Ξ =
       λ b b⊩⟦f⟧ΞR → syntacticTransportPreservesRealizers⁺ γ (r ⨾ b) f₁ (r⊩⟦f⟧Ξ b (syntacticTransportPreservesRealizers⁻ γ b f b⊩⟦f⟧ΞR))
-    syntacticTransportPreservesRealizers⁺ {Γ} γ r (Relational.`¬ f) r⊩⟦f⟧Ξ = {!!}
     syntacticTransportPreservesRealizers⁺ {Γ} γ r (Relational.`∃ f) r⊩⟦f⟧Ξ =
       r⊩⟦f⟧Ξ >>=
         λ { ((γ' , b) , γ'≡γ , r⊩⟦f⟧Ξγ'b) → ∣ (γ' , b) , (γ'≡γ , (syntacticTransportPreservesRealizers⁺ (γ' , b) r f r⊩⟦f⟧Ξγ'b)) ∣₁ }
@@ -100,14 +113,44 @@ module WeakenSemantics
         r⊩⟦f⟧Ξ
 
     syntacticTransportPreservesRealizers⁻ {Γ} γ r Relational.⊤ᵗ r⊩⟦f⟧ΞR = r⊩⟦f⟧ΞR
-    syntacticTransportPreservesRealizers⁻ {Γ} γ r (f Relational.`∨ f₁) r⊩⟦f⟧ΞR = {!!}
-    syntacticTransportPreservesRealizers⁻ {Γ} γ r (f Relational.`∧ f₁) r⊩⟦f⟧ΞR = {!!}
-    syntacticTransportPreservesRealizers⁻ {Γ} γ r (f Relational.`→ f₁) r⊩⟦f⟧ΞR = {!!}
-    syntacticTransportPreservesRealizers⁻ {Γ} γ r (Relational.`¬ f) r⊩⟦f⟧ΞR = {!!}
-    syntacticTransportPreservesRealizers⁻ {Γ} γ r (Relational.`∃ f) r⊩⟦f⟧ΞR = {!!}
-    syntacticTransportPreservesRealizers⁻ {Γ} γ r (Relational.`∀ f) r⊩⟦f⟧ΞR = {!!}
-    syntacticTransportPreservesRealizers⁻ {Γ} γ r (Relational.rel k₁ x) r⊩⟦f⟧ΞR = {!!}
+    syntacticTransportPreservesRealizers⁻ {Γ} γ r (f Relational.`∨ f₁) r⊩⟦f⟧ΞR =
+      r⊩⟦f⟧ΞR >>=
+        λ { (inl (pr₁r≡k , pr₂r⊩⟦f⟧)) →
+            ∣ inl (pr₁r≡k , (syntacticTransportPreservesRealizers⁻ γ (pr₂ ⨾ r) f pr₂r⊩⟦f⟧)) ∣₁
+          ; (inr (pr₁r≡k' , pr₂r⊩⟦f₁⟧)) →
+            ∣ inr (pr₁r≡k' , (syntacticTransportPreservesRealizers⁻ γ (pr₂ ⨾ r) f₁ pr₂r⊩⟦f₁⟧)) ∣₁ }
+    syntacticTransportPreservesRealizers⁻ {Γ} γ r (f Relational.`∧ f₁) r⊩⟦f⟧ΞR =
+      (syntacticTransportPreservesRealizers⁻ γ (pr₁ ⨾ r) f (r⊩⟦f⟧ΞR .fst)) ,
+      (syntacticTransportPreservesRealizers⁻ γ (pr₂ ⨾ r) f₁ (r⊩⟦f⟧ΞR .snd))
+    syntacticTransportPreservesRealizers⁻ {Γ} γ r (f Relational.`→ f₁) r⊩⟦f→f₁⟧ΞR =
+      λ b b⊩⟦f⟧Ξ → syntacticTransportPreservesRealizers⁻ γ (r ⨾ b) f₁ (r⊩⟦f→f₁⟧ΞR b (syntacticTransportPreservesRealizers⁺ γ b f b⊩⟦f⟧Ξ))
+    syntacticTransportPreservesRealizers⁻ {Γ} γ r (Relational.`∃ f) r⊩⟦f⟧ΞR =
+      r⊩⟦f⟧ΞR >>=
+        λ { ((γ' , b) , γ'≡γ , r⊩⟦f⟧γ'b) → ∣ (γ' , b) , γ'≡γ , (syntacticTransportPreservesRealizers⁻ (γ' , b) r f r⊩⟦f⟧γ'b) ∣₁ }
+    syntacticTransportPreservesRealizers⁻ {Γ} γ r (Relational.`∀ f) r⊩⟦f⟧ΞR =
+      λ { b (γ' , b') γ'≡γ → syntacticTransportPreservesRealizers⁻ (γ' , b') (r ⨾ b) f (r⊩⟦f⟧ΞR b (γ' , b') γ'≡γ) }
+    syntacticTransportPreservesRealizers⁻ {Γ} γ r (Relational.rel Rsym t) r⊩⟦f⟧ΞR =
+      subst
+        (λ R' → r ⊩ ∣ R' ∣ (⟦ t ⟧ᵗ γ))
+        (sym (RΞsem (suc Rsym) ≡⟨ refl ⟩ (Ξsem Rsym ∎)))
+        r⊩⟦f⟧ΞR
+
+    syntacticTransportPreservesRealizers :
+      ∀ {Γ}
+      → (γ : ⟨ ⟦ Γ ⟧ᶜ ⟩)
+      → (r : A)
+      → (f : ΞFormula Γ)
+      ----------------------------------------------------------
+      → r ⊩ ∣ InterpretationΞR.⟦ transportAlongWeakening f ⟧ᶠ ∣ γ
+      ≡ r ⊩ ∣ InterpretationΞ.⟦ f ⟧ᶠ ∣ γ
+    syntacticTransportPreservesRealizers {Γ} γ r f =
+      hPropExt
+        (InterpretationΞR.⟦ transportAlongWeakening f ⟧ᶠ .isPropValued γ r)
+        (InterpretationΞ.⟦ f ⟧ᶠ .isPropValued γ r)
+        (λ r⊩⟦f⟧ΞR → syntacticTransportPreservesRealizers⁻ γ r f r⊩⟦f⟧ΞR)
+        λ r⊩⟦f⟧Ξ → syntacticTransportPreservesRealizers⁺ γ r f r⊩⟦f⟧Ξ
 
     transportPreservesHoldsInTripos : ∀ {Γ} → (f : ΞFormula Γ) → SoundnessΞ.holdsInTripos f → SoundnessΞR.holdsInTripos (transportAlongWeakening f)
-    transportPreservesHoldsInTripos {Γ} f holds = {!!}
+    transportPreservesHoldsInTripos {Γ} f holds =
+      {!!}
 
diff --git a/src/Realizability/Tripos/Logic/Semantics.agda b/src/Realizability/Tripos/Logic/Semantics.agda
@@ -137,7 +137,6 @@ module Interpretation
   ⟦_⟧ᶠ {Γ} (form `∨ form₁) = _⊔_ ⟨ ⟦ Γ ⟧ᶜ ⟩ ⟦ form ⟧ᶠ ⟦ form₁ ⟧ᶠ
   ⟦_⟧ᶠ {Γ} (form `∧ form₁) = _⊓_ ⟨ ⟦ Γ ⟧ᶜ ⟩ ⟦ form ⟧ᶠ ⟦ form₁ ⟧ᶠ
   ⟦_⟧ᶠ {Γ} (form `→ form₁) = _⇒_ ⟨ ⟦ Γ ⟧ᶜ ⟩ ⟦ form ⟧ᶠ ⟦ form₁ ⟧ᶠ
-  ⟦_⟧ᶠ {Γ} (`¬ form) = _⇒_ ⟨ ⟦ Γ ⟧ᶜ ⟩ ⟦ form ⟧ᶠ ⟦ ⊥ᵗ {Γ = Γ} ⟧ᶠ
   ⟦_⟧ᶠ {Γ} (`∃ {B = B} form) = `∃[_] (isSet× (str ⟦ Γ ⟧ᶜ) (str ⟦ B ⟧ˢ)) (str ⟦ Γ ⟧ᶜ) (λ { (⟦Γ⟧ , ⟦B⟧) → ⟦Γ⟧ }) ⟦ form ⟧ᶠ
   ⟦_⟧ᶠ {Γ} (`∀ {B = B} form) = `∀[_] (isSet× (str ⟦ Γ ⟧ᶜ) (str ⟦ B ⟧ˢ)) (str ⟦ Γ ⟧ᶜ) (λ { (⟦Γ⟧ , ⟦B⟧) → ⟦Γ⟧ }) ⟦ form ⟧ᶠ
   ⟦_⟧ᶠ {Γ} (rel R t) = ⋆_ (str ⟦ Γ ⟧ᶜ) (str ⟦ lookup R relSym ⟧ˢ) ⟦ t ⟧ᵗ ⟦ R ⟧ʳ
@@ -215,8 +214,6 @@ module Interpretation
                 (λ form → b ⊩ ∣ form ∣ γ)
                 (substitutionFormulaSound subs f)
                 b⊩substFormulaFs))
-  substitutionFormulaSound {Γ} {Δ} subs (`¬ f) =
-    substitutionFormulaSound subs (f `→ ⊥ᵗ)
   substitutionFormulaSound {Γ} {Δ} subs (`∃ {B = B} f) =
     Predicate≡
       ⟨ ⟦ Γ ⟧ᶜ ⟩

diff --git a/src/Realizability/Tripos/Logic/Syntax.agda b/src/Realizability/Tripos/Logic/Syntax.agda
@@ -93,19 +93,19 @@ module Relational {n} (relSym : Vec Sort n) where
    ⊥ᵗ : ∀ {Γ} → Formula Γ
    _`∨_ : ∀ {Γ} → Formula Γ → Formula Γ → Formula Γ 
    _`∧_ : ∀ {Γ} → Formula Γ → Formula Γ → Formula Γ 
-   _`→_ : ∀ {Γ} → Formula Γ → Formula Γ → Formula Γ 
-   `¬_ : ∀ {Γ} → Formula Γ → Formula Γ
+   _`→_ : ∀ {Γ} → Formula Γ → Formula Γ → Formula Γ
    `∃ : ∀ {Γ B} → Formula (Γ ′ B) → Formula Γ
    `∀ : ∀ {Γ B} → Formula (Γ ′ B) → Formula Γ
    rel : ∀ {Γ} (k : Fin n) → Term Γ (lookup k relSym) → Formula Γ
 
+ pattern `¬ f = f `→ ⊥ᵗ
+
  substitutionFormula : ∀ {Γ Δ} → Substitution Γ Δ → Formula Δ → Formula Γ
  substitutionFormula {Γ} {Δ} subs ⊤ᵗ = ⊤ᵗ
  substitutionFormula {Γ} {Δ} subs ⊥ᵗ = ⊥ᵗ
  substitutionFormula {Γ} {Δ} subs (form `∨ form₁) = substitutionFormula subs form `∨ substitutionFormula subs form₁
  substitutionFormula {Γ} {Δ} subs (form `∧ form₁) = substitutionFormula subs form `∧ substitutionFormula subs form₁
  substitutionFormula {Γ} {Δ} subs (form `→ form₁) = substitutionFormula subs form `→ substitutionFormula subs form₁
- substitutionFormula {Γ} {Δ} subs (`¬ form) = `¬ substitutionFormula subs form
  substitutionFormula {Γ} {Δ} subs (`∃ form) = `∃ (substitutionFormula (var here , drop subs) form )
  substitutionFormula {Γ} {Δ} subs (`∀ form) = `∀ (substitutionFormula (var here , drop subs) form)
  substitutionFormula {Γ} {Δ} subs (rel k x) = rel k (substitutionTerm subs x)