第71章：単純型付きラムダ計算の圏論的意味論——判断を射へ移す#

namespace FormalLab.Bridges.STLCCategoricalSemantics

open FormalLab.TypeTheory.SimplyTypedLambdaCalculus
open FormalLab.TypeTheory.StructuralRules

universe u

def interpretType (Base : Type u) : SimpleType → Type u
  | .atom => Base
  | A ⇒ B => interpretType Base A → interpretType Base B

def interpretContext (Base : Type u) : Context → Type u
  | [] => PUnit.{u + 1}
  | A :: Γ => interpretType Base A × interpretContext Base Γ

def denoteVar {Base : Type u} {Γ : Context} {A : SimpleType} :
    Var Γ A → interpretContext Base Γ → interpretType Base A
  | .zero => Prod.fst
  | .succ v => denoteVar v ∘ Prod.snd

example {Base : Type u} {Γ : Context} {A : SimpleType} :
    denoteVar (Base := Base) (Var.zero : Var (A :: Γ) A) = Prod.fst := rfl

example {Base : Type u} {Γ : Context} {A B : SimpleType} (v : Var Γ A) :
    denoteVar (Base := Base) (Var.succ (B := B) v) = denoteVar v ∘ Prod.snd := rfl

def denoteTm {Base : Type u} {Γ : Context} {A : SimpleType} :
    Tm Γ A → interpretContext Base Γ → interpretType Base A
  | .var v => denoteVar v
  | .app fn argument =>
      fun environment => denoteTm fn environment (denoteTm argument environment)
  | .lam body =>
      fun environment value => denoteTm body (value, environment)

def EnvironmentsAgree {Base : Type u} {Γ Δ : Context} (ρ : Renaming Γ Δ)
    (source : interpretContext Base Γ) (target : interpretContext Base Δ) : Prop :=
  ∀ {A : SimpleType} (v : Var Γ A), denoteVar v source = denoteVar (ρ v) target

theorem environmentsAgree_lift {Base : Type u} {Γ Δ : Context} {A : SimpleType}
    {ρ : Renaming Γ Δ} {source : interpretContext Base Γ} {target : interpretContext Base Δ}
    (h : EnvironmentsAgree ρ source target) (value : interpretType Base A) :
    EnvironmentsAgree (liftRenaming ρ) (value, source) (value, target) := by
  intro B v
  cases v with
  | zero => rfl
  | succ rest => exact h rest

theorem denote_rename {Base : Type u} {Γ : Context} {A : SimpleType} (term : Tm Γ A) :
    ∀ {Δ : Context} (ρ : Renaming Γ Δ)
      (source : interpretContext Base Γ) (target : interpretContext Base Δ),
      EnvironmentsAgree ρ source target →
        denoteTm term source = denoteTm (rename ρ term) target := by
  induction term with
  | var v =>
      intro Δ ρ source target h
      exact h v
  | app fn argument fn_ih argument_ih =>
      intro Δ ρ source target h
      change denoteTm fn source (denoteTm argument source) =
        denoteTm (rename ρ fn) target (denoteTm (rename ρ argument) target)
      rw [fn_ih ρ source target h, argument_ih ρ source target h]
  | lam body body_ih =>
      intro Δ ρ source target h
      funext value
      exact body_ih (liftRenaming ρ) (value, source) (value, target)
        (environmentsAgree_lift h value)

theorem denote_weakenFront {Base : Type u} {Γ : Context} {A B : SimpleType}
    (term : Tm Γ A) (value : interpretType Base B) (environment : interpretContext Base Γ) :
    denoteTm (weakenFront term) (value, environment) = denoteTm term environment := by
  symm
  exact denote_rename term (fun v => .succ v) environment (value, environment) (by
    intro C v
    rfl)

theorem denote_identity (Base : Type u) (A : SimpleType) :
    denoteTm (Base := Base) (identity A) .unit =
      (id : interpretType Base A → interpretType Base A) := rfl

theorem denote_constant (Base : Type u) (A B : SimpleType) :
    denoteTm (Base := Base) (constant A B) .unit =
      (fun a : interpretType Base A => fun _ : interpretType Base B => a) := rfl

def identityRedex {A : SimpleType} (argument : Tm [] A) : Tm [] A :=
  .app (identity A) argument

theorem denote_identityRedex {Base : Type u} {A : SimpleType}
    (argument : Tm [] A) :
    denoteTm (Base := Base) (identityRedex argument) .unit = denoteTm argument .unit := rfl

def etaExpansion {A B : SimpleType} (function : Tm [] (A ⇒ B)) : Tm [] (A ⇒ B) :=
  .lam (.app (weakenFront function) (.var .zero))

theorem denote_etaExpansion {Base : Type u} {A B : SimpleType}
    (function : Tm [] (A ⇒ B)) :
    denoteTm (Base := Base) (etaExpansion function) .unit = denoteTm function .unit := by
  funext value
  exact congrFun (denote_weakenFront function value .unit) value

abbrev SemanticTerm (Base : Type u) (Γ : Context) (A : SimpleType) :=
  interpretContext Base Γ → interpretType Base A

abbrev SemanticSubstitution (Base : Type u) (Γ Δ : Context) :=
  interpretContext Base Δ → interpretContext Base Γ

def semanticSubstitute {Base : Type u} {Γ Δ : Context} {A : SimpleType}
    (substitution : SemanticSubstitution Base Γ Δ)
    (term : SemanticTerm Base Γ A) : SemanticTerm Base Δ A :=
  term ∘ substitution

theorem semanticSubstitute_id {Base : Type u} {Γ : Context} {A : SimpleType}
    (term : SemanticTerm Base Γ A) :
    semanticSubstitute id term = term := by
  funext environment
  rfl

theorem semanticSubstitute_comp {Base : Type u} {Γ Δ Θ : Context} {A : SimpleType}
    (first : SemanticSubstitution Base Γ Δ)
    (second : SemanticSubstitution Base Δ Θ)
    (term : SemanticTerm Base Γ A) :
    semanticSubstitute second (semanticSubstitute first term) =
      semanticSubstitute (first ∘ second) term := by
  funext environment
  rfl

open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.CartesianMonoidalCategory
open _root_.CategoryTheory.MonoidalClosed

universe uC vC

variable {C : Type uC} [Category.{vC} C]
variable [CartesianMonoidalCategory C] [MonoidalClosed C]
variable {Γ A B : C}

def interpretZeroVariable : A ⊗ Γ ⟶ A := fst A Γ

def interpretWeakening (term : Γ ⟶ B) : A ⊗ Γ ⟶ B :=
  snd A Γ ≫ term

def interpretApplication (function : Γ ⟶ A ⟶[C] B) (argument : Γ ⟶ A) : Γ ⟶ B :=
  lift argument function ≫ (ihom.ev A).app B

def interpretAbstraction (body : A ⊗ Γ ⟶ B) : Γ ⟶ A ⟶[C] B :=
  curry body

example (body : A ⊗ Γ ⟶ B) : uncurry (interpretAbstraction body) = body :=
  uncurry_curry body

example (function : Γ ⟶ A ⟶[C] B) :
    interpretAbstraction (uncurry function) = function :=
  curry_uncurry function

theorem categorical_beta (body : A ⊗ Γ ⟶ B) :
    A ◁ interpretAbstraction body ≫ (ihom.ev A).app B = body :=
  whiskerLeft_curry_ihom_ev_app A B body

theorem categorical_eta (function : Γ ⟶ A ⟶[C] B) :
    interpretAbstraction (uncurry function) = function :=
  curry_uncurry function