From Denotational Semantics, looking backward - looking forward

這裡嘗試用agda表示Partial Equivalences as Types

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.Equiv
open import UF.Powerset
open import UF.SubtypeClassifier

module ag-U75Z where

我們用agda表示relation

Rel : 𝓤₁ ̇
Rel = 𝓟 ℕ → 𝓟 ℕ → 𝓤₀ ̇

定義一個輔助閱讀的表達記號 X [ R ] Y

_[_]_ : {X : 𝓤 ̇ } → X → (X → X → 𝓥 ̇ ) → X → 𝓥 ̇
x [ R ] y = R x y

一個relation是PER表示它是symmetric且transitive

is-PER : {X : 𝓤 ̇} → (X → X → 𝓥 ̇) → 𝓤 ⊔ 𝓥  ̇
is-PER R = symmetric R × transitive R

提取用的helpers

PER-symm : {A : Rel} → (is-PER A) → symmetric A
PER-symm per-A = per-A .pr₁
PER-trans : {A : Rel} → (is-PER A) → transitive A
PER-trans per-A = per-A .pr₂

現在可以定義PER的exponentiation

_=>_ : Rel → Rel → (𝓟 ℕ → 𝓟 ℕ) → (𝓟 ℕ → 𝓟 ℕ) → 𝓤₁ ̇
(A => B) F G = (X Y : 𝓟 ℕ) → X [ A ] Y → (F X) [ B ] (G Y)
infixr  _=>_

我們希望證明exponentiation依然是一個PER（當然也因此是type）

A=>B-is-PER-if-A-B-are-PERs : {A B : Rel}
     → is-PER A
     → is-PER B
     → is-PER (A => B)
A=>B-is-PER-if-A-B-are-PERs {A}{B} per-A per-B = I , II
  where
  I : symmetric (A => B)
  I F G F[A=>B]G X Y X[A]Y = goal
    where
    Y[A]X : Y [ A ] X
    Y[A]X = PER-symm per-A X Y X[A]Y

    swap : Y [ A ] X → (F Y) [ B ] (G X)
    swap = F[A=>B]G Y X

    apply : (F Y) [ B ] (G X)
    apply = swap Y[A]X

    goal : (G X) [ B ] (F Y)
    goal = PER-symm per-B (F Y) (G X) apply
  II : transitive (A => B)
  II F G H F[A=>B]G G[A=>B]H X Y X[A]Y = goal
    where
    apply₁ : (F X) [ B ] (G Y)
    apply₁ = F[A=>B]G X Y X[A]Y

    Y[A]X : Y [ A ] X
    Y[A]X = PER-symm per-A X Y X[A]Y

    Y[A]Y : Y [ A ] Y
    Y[A]Y = PER-trans per-A Y X Y Y[A]X X[A]Y

    apply₂ : (G Y) [ B ] (H Y)
    apply₂ = G[A=>B]H Y Y Y[A]Y

    goal : F X [ B ] H Y
    goal = PER-trans per-B (F X) (G Y) (H Y) apply₁ apply₂

確認這真的表示了函數類型的概念

this-is-really-function-type : {A B : Rel}
  → (F : 𝓟 ℕ → 𝓟 ℕ) → F [ A => B ] F
  → ((X : 𝓟 ℕ) → X [ A ] X → F X [ B ] F X)
this-is-really-function-type {A}{B} F F:A=>B X X:A = F:A=>B X X X:A

fst : 𝓟 ℕ → 𝓟 ℕ → 𝓟 ℕ
fst x y = x

main : {A B : Rel} → fst [ A => B => A ] fst