lics24.lagda

\begin{code}
{-# OPTIONS --rewriting #-}
{-# OPTIONS --guardedness #-}

open import Level renaming (suc to lsuc)
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma
open import Axiom.ExcludedMiddle
open import Axiom.Extensionality.Propositional
open import Data.Empty
open import Data.Maybe
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Relation.Nullary

open import util
open import name
open import calculus
open import terms
open import world
open import choice
open import compatible
open import progress
open import choiceExt
open import choiceVal
open import getChoice
open import newChoice
open import freeze
open import freezeExt
open import progress
open import choiceBar
open import mod
open import encode
open import MarkovPrinciple

module lics24 {L   : Level}
              (W   : PossibleWorlds {L})
              (M   : Mod W)
              (C   : Choice)
              (K   : Compatible W C)
              (P   : Progress W C K)
              (G   : GetChoice W C K)
              (X   : ChoiceExt W C)
              (N   : NewChoice W C K G)
              (EC  : Encode)
              (V   : ChoiceVal W C K G X N EC)
              (F   : Freeze W C K P G N)
              (FE : FreezeExt W C K P G N F)
              (EM  : ExcludedMiddle (lsuc(L)))
              (MP  : MarkovPrinciple (lsuc(L)))
              (Ext : Extensionality 0ℓ 0ℓ)
              (CB  : ChoiceBar W M C K P G X N EC V F) where


  -- Notation
  open import worldDef(W)
  open import getChoiceDef(W)(C)(K)(G)
  open import freezeDef(W)(C)(K)(P)(G)(N)(F)
  open import choiceBarDef(W)(M)(C)(K)(P)(G)(X)(N)(EC)(V)(F)(CB)
  open import compatibleDef(W)(C)(K)
  open import choiceDef{L}(C)
  open import barI(W)(M)

  -- Boxtt model definition and its properties
  open import computation(W)(C)(K)(G)(X)(N)(EC)
  open import forcing(W)(M)(C)(K)(G)(X)(N)(EC)
  open import terms8(W)(C)(K)(G)(X)(N)(EC)
  open import props1(W)(M)(C)(K)(G)(X)(N)(EC)
  open import props2(W)(M)(C)(K)(G)(X)(N)(EC)
  open import props3(W)(M)(C)(K)(G)(X)(N)(EC)
  open import pure(W)(M)(C)(K)(G)(X)(N)(EC)
  open import pure2(W)(M)(C)(K)(G)(X)(N)(EC)
  open import sequent(W)(M)(C)(K)(G)(X)(N)(EC)

  -- Types of choice sequences
  open import typeC(W)(M)(C)(K)(P)(G)(X)(N)(EC)(V)(F)(CB)
  open import boolC(W)(M)(C)(K)(P)(G)(X)(N)(EC)(V)(F)(CB)
  open import choiceProp(W)(C)(K)(G)(X)(N)(EC)

  -- Markov's principles
  open import not_mp(W)(M)(C)(K)(P)(G)(X)(N)(EC)(V)(F)(FE)(CB)
  open import mp_prop(W)(M)(C)(K)(P)(G)(X)(N)(EC)(V)(F)(CB)
  open import mp_prop2(W)(M)(C)(K)(P)(G)(X)(N)(EC)(V)(F)(FE)(CB)(EM)
  open import mp_props(W)(M)(C)(K)(G)(X)(N)(EC) hiding (MP)
  open import mp_props3(W)(M)(C)(K)(G)(X)(N)(EC)
  open import mpp(W)(M)(C)(K)(G)(X)(N)(EM)(EC)
  open import mpp2(W)(M)(C)(K)(G)(X)(N)(MP)(EC)

  -- MLTT definition and translation
  import Definition.Untyped as MLTT
  open import Definition.Typed using (_⊢_)
  open import mltt(W)(M)(C)(K)(G)(X)(N)(EC)

  -- Instances of modalities and choice sequences
  open import barBeth(W)(C)(K)(P)
  open import worldInstanceCSbool(Ext)
  import modInstanceBethCsBool2(Ext) as InstanceBeth

\end{code}

\section{Markov's Principles}

\begin{code}

  -- Primitive recursive Markov's principles using Σ
  MP-pr : CTerm
  MP-pr = #MPp₇

  -- Primitive recursive Markov's principles using squashed Σ
  MP-squashed-pr : CTerm
  MP-squashed-pr = #MPp₆

  -- Boolean Markov's principle using Σ
  MP-𝔹 : CTerm
  MP-𝔹 = #MPₘ

  -- Boolean Markov's principles using squashed Σ
  MP-squashed-𝔹 : CTerm
  MP-squashed-𝔹 = #MP₆

  MP-squashed-𝔹' : CTerm
  MP-squashed-𝔹' = #MP₇

  -- Propositional Markov's principle using squahsed Σ
  MP-squashed-ℙ : CTerm
  MP-squashed-ℙ = #MPℙ 0

\end{code}

\section{TTbox primer}

\begin{code}

  definition-5∙1 : Set(lsuc L)
  definition-5∙1 = PossibleWorlds {L}

  definition-5∙2 : Set(lsuc L)
  definition-5∙2 = NewChoice W C K G

  example-5∙3 : NewChoice(PossibleWorldsCS)(choiceCS)(compatibleCS)(getChoiceCS)
  example-5∙3 = newChoiceCS

  operational-semantics : (T : Term) (w : 𝕎·) → Maybe (Term × 𝕎·)
  operational-semantics = step

  definition-5∙4 : Set(lsuc (lsuc L))
  definition-5∙4 = Mod(W)

  example-5∙5 : (w : 𝕎·) (f : wPred w) → Set(lsuc(L))
  example-5∙5 = inBethBar

  theorem-5∙6 : (n : ℕ) → is-TSP-univs (uni n)
  theorem-5∙6 = typeSysConds

  -- The following definition differs slightly from the paper, as in the paper
  -- we have specified it to the case of choice sequences and the beth modality.
  definition-5∙7 : _
  definition-5∙7 = (w : 𝕎·) (c : Name) (m : ℕ) (r : Res)
                     → compatible· c w r
                     → □· w (λ w' _ → ∀𝕎 w' (λ w'' _ → Lift {0ℓ} (lsuc(L)) (Σ ℂ· (λ t → getChoice· m c w'' ≡ just t × ·ᵣ r m t))))

  -- The assumption that the modalities are retrieving is part of the
  -- record type ChoiceBar, namely the □·-choice field seen below.
  _ : definition-5∙7
  _ = □·-choice·

  beth-satisfies-def-5∙7 : _
  beth-satisfies-def-5∙7 = InstanceBeth.□·-choice-beth-cs0

  theorem-5∙8 : (w : 𝕎·)
                (δ : Name)
              → Bool₀!ℂ CB
              → compatible· δ w Resℂ
              → member w #NAT!→BOOL₀! (#CS δ)
  theorem-5∙8 w δ choicesAreBools comp = 0 , →equalInType-CS-NAT!→BOOL₀! δ-output-is-bool
   where
    NUMm-in-NAT! : (m : ℕ) (w' : 𝕎·) → equalInType 0 w' #NAT! (#NUM m) (#NUM m)
    NUMm-in-NAT! m w' = NUM-equalInType-NAT! 0 w' m

    δ-always-comp : {w' : 𝕎·} → w ⊑· w' → compatible· δ w' Resℂ
    δ-always-comp e = ⊑-compatible· e comp

    δ-output-is-choice-type : (w' : 𝕎·) → w ⊑· w'
                            → (m : ℕ)
                            → equalInType 0 w' Typeℂ₀₁· (#APPLY (#CS δ) (#NUM m)) (#APPLY (#CS δ) (#NUM m))
    δ-output-is-choice-type w' e m = →equalInType-APPLY-CS-Typeℂ₀₁· (δ-always-comp e) (NUMm-in-NAT! m w')

    δ-output-is-bool : (w' : 𝕎·) → w ⊑· w'
                     → (m : ℕ)
                     → equalInType 0 w' #BOOL₀! (#APPLY (#CS δ) (#NUM m)) (#APPLY (#CS δ) (#NUM m))
    δ-output-is-bool w' e m = ≡CTerm→equalInType (fst choicesAreBools) (δ-output-is-choice-type w' e m)

\end{code}

\section{Interpretations of MLTT in TTbox}

\begin{code}

  theorem-6∙1 : {n : ℕ} {Γ : MLTT.Con MLTT.Term n} {σ : MLTT.Term n}
                (j : Γ ⊢ σ)
                (i k : ℕ)
              → 1 < k
              → k < i
              → valid∈𝕎 i ⟦ Γ ⟧Γ ⟦ σ ⟧ᵤ (UNIV k)
  theorem-6∙1 = ⟦_⟧⊢

\end{code}

\section{Separation of MPbool and MPpr}

\begin{code}

  can-assume-NAT-is-pure : (i : ℕ) (w : 𝕎·) (F a : CTerm)
                         → ∈Type (suc i) w (#FUN #NAT! (#UNIV i)) F
                         → ∈Type i w (#PI (#TPURE #NAT!) (#[0]SQUASH (#[0]APPLY ⌞ F ⌟ #[0]VAR))) a
                         → ∈Type i w (#PI #NAT! (#[0]SQUASH (#[0]APPLY ⌞ F ⌟ #[0]VAR))) a
  can-assume-NAT-is-pure i w F a = ∈PURE-NAT→ i (suc i) w F a ≤-refl

  definition-7∙1 : Set(lsuc(L))
  definition-7∙1 = Freeze W C K P G N

  definition-7∙2 : Set(lsuc(lsuc(L)))
  definition-7∙2 = (c : Name) {w : 𝕎·} {f : wPred w} {r : Res{0ℓ}}
                     → □· w f
                     → onlyℂ∈𝕎 (Res.c₀ r) c w
                     → compatible· c w r
                     → freezable· c w
                     → ∃𝕎 w (λ w1 e1 → onlyℂ∈𝕎 (Res.c₀ r) c w1
                                        × compatible· c w1 r
                                        × freezable· c w1 × f w1 e1)

  -- The assumption that the modalities are choice-following is part of the
  -- record type ChoiceBar, namely the followChoice field seen below.
  _ : definition-7∙2
  _ = followChoice·

  lemma-7∙3 : (w1 w2 : 𝕎·) (t u : Term)
            → ¬Names t
            → t ⇛! u at w1
            → t ⇛! u at w2
  lemma-7∙3 = ¬Names→⇛!

  -- We formalize choices sequences of natural numbers for this result,
  -- but the same could be achieved with booleans as described in the paper.
  ¬MP-𝔹-holds : Nat!ℂ CB
              → (w : 𝕎·) → member w (#NEG MP-𝔹) #lamAX
  ¬MP-𝔹-holds choicesAreNat w = 0 , ¬MPₘ choicesAreNat w 0

  ¬MP-squashed-𝔹-holds : Bool₀!ℂ CB
                       → (w : 𝕎·) → member w (#NEG MP-squashed-𝔹) #lamAX
  ¬MP-squashed-𝔹-holds choicesAreBool w = 0 , ¬MP₆ choicesAreBool w 0

  MP-pr-holds : (w : 𝕎·) → member w MP-pr #lamInfSearchP
  MP-pr-holds w = 0 , MPp₇-inh 0 w

  MP-squashed-pr-holds : (w : 𝕎·) → member w MP-squashed-pr #lam2AX
  MP-squashed-pr-holds w = 0 , MPp₆-inh₂ 0 w

\end{code}

\section{Separation of MPprop and MPbool}

\begin{code}

  ¬MP-ℙ'-holds : Choiceℙ 0 CB
               → immutableChoices
               → (w : 𝕎·) → member w (#NEG MP-squashed-ℙ) #lamAX
  ¬MP-ℙ'-holds choicesAreProp choicesAreImmutable w =
   1 , ¬MPℙ 0 choicesAreProp choicesAreImmutable w

  -- This lemma has an extra assumption than in the paper as the paper
  -- presents a slightly simplified computation system
  lemma-8·1 : getChoiceℙ
            → (w1 w2 : 𝕎·) (t a b : Term)
            → ¬Enc t            -- assumption not mentioned in paper
            → t ⇛! INL a at w1
            → t ⇛! INR b at w2
            → ⊥
  lemma-8·1 = ¬enc→⇛!INL-INR

  MP-squashed-𝔹'-holds : getChoiceℙ
                       → (w : 𝕎·) → member w MP-squashed-𝔹' #lam2AX
  MP-squashed-𝔹'-holds choicesAreProp w = 0 , MP₇-inh choicesAreProp 0 w

\end{code}