Extremely composable embeddable programming language

可以先從這些截圖感受一下這什麼程式語言xd

系統上執行的某個程式或服務 - 無論是 process、service 或綁定到連接埠的程式。都必然有其原因，但這些原因通常間接、不易察覺，或是跨越多個層級，例如監控程式、容器、服務或 shell。而 witr 的用途就是一次展示這些資訊。

看不懂 OCaml formatter 要怎麼設定？這個專案把排版選項、原始碼跟結果都展示出來，讓人直覺的做出選擇。

A covering space of a type (space) $A$ is a family of sets indexed by $A$ .

{-# OPTIONS --safe --without-K #-}
module ag-000L where

open import MLTT.Spartan hiding (fiber)
open import UF.Sets

record covering (A : 𝓤 ̇ ) : 𝓤 ⁺  ̇ where
  constructor cov[_,_]
  field
    fiber : A → 𝓤 ̇
    fiber-is-set : ∀ (a : A) → is-set (fiber a)

https://sdiehl.github.io/zero-to-qed/01_introduction.html 這個專案教了很多很細節的 tactics，是很好的參考工具。

{-# OPTIONS --safe --without-K #-}
module ag-000K where

open import MLTT.Spartan
open import Naturals.Properties

Eliminator of ℕ

ℕ-elim : ∀ (P : ℕ → 𝓤 ̇) → P  → (∀ (n : ℕ) → P n → P (succ n)) → (∀ (n : ℕ) → P n)
ℕ-elim P P0 Ps zero = P0
ℕ-elim P P0 Ps (succ n) = Ps n (ℕ-elim P P0 Ps n)

Define with pattern matching

plus : ℕ → ℕ → ℕ
plus zero b = b
plus (succ a) b = succ (plus a b)

mul : ℕ → ℕ → ℕ
mul zero c = zero
mul (succ a) b = plus b (mul a b)

exp : ℕ → ℕ → ℕ
exp x zero = 
exp x (succ k) = mul x (exp x k)

Now use the eliminator to define them

plus' : ℕ → ℕ → ℕ
plus' x = ℕ-elim (λ _ → ℕ → ℕ) (λ z → z) (λ x' plus-x' → λ y → succ (plus-x' y)) x

t5 : plus'   ＝ 
t5 = refl

p1 : (a b : ℕ) → plus a b ＝ plus' a b
p1 zero b = refl
p1 (succ a) b =
  succ (plus a b)  ＝⟨ ap succ (p1 a b) ⟩
  succ (plus' a b) ＝⟨by-definition⟩
  succ (ℕ-elim (λ _ → ℕ → ℕ) (λ z → z) (λ x' plus-x' → λ y → succ (plus-x' y)) a b)
    ＝⟨by-definition⟩
  plus' (succ a) b ∎

mul' : ℕ → ℕ → ℕ
mul' x = ℕ-elim (λ _ → ℕ → ℕ) (λ z → zero) (λ x' mul-x' → λ y → plus' y (mul-x' y)) x

t7 : mul'   ＝ 
t7 = refl
t8 : mul'   ＝ 
t8 = refl
t9 : mul'   ＝ 
t9 = refl

p2 : (a b : ℕ) → mul a b ＝ mul' a b
p2 zero b = refl
p2 (succ a) zero = p2 a 
p2 (succ a) (succ b) =
  plus (succ b) (mul a (succ b))   ＝⟨ p1 (succ b) (mul a (succ b)) ⟩
  plus' (succ b) (mul a (succ b))  ＝⟨ ap (plus' (succ b)) (p2 a (succ b)) ⟩
  plus' (succ b) (mul' a (succ b)) ＝⟨by-definition⟩
  mul' (succ a) (succ b) ∎

exp' : ℕ → ℕ → ℕ
exp' x y = ℕ-elim (λ _ → ℕ → ℕ) (λ x → ) (λ y' exp-y' → λ x → mul' x (exp-y' x)) y x

t10 : exp'   ＝ 
t10 = refl
t11 : exp'   ＝ 
t11 = refl

p3 : (a b : ℕ) → exp a b ＝ exp' a b
p3 a zero = refl
p3 zero (succ b) = refl
p3 (succ a) (succ b) =
  exp (succ a) (succ b)           ＝⟨by-definition⟩
  mul (succ a) (exp (succ a) b)   ＝⟨ p2 (succ a) (exp (succ a) b) ⟩
  mul' (succ a) (exp (succ a) b)  ＝⟨ ap (mul' (succ a)) (p3 (succ a) b) ⟩
  mul' (succ a) (exp' (succ a) b) ＝⟨by-definition⟩
  exp' (succ a) (succ b) ∎

Plus commutative yoga

C : commutative plus
C zero zero = refl
C zero (succ b) =
  succ b ＝⟨ ap succ (C  b) ⟩
  succ (plus b zero) ∎
C (succ a) zero =
  succ (plus a ) ＝⟨ ap succ (C a ) ⟩
  succ (plus  a) ＝⟨ refl ⟩
  plus  (succ a) ∎
C (succ a) (succ b) =
  succ (plus a (succ b)) ＝⟨ ap succ (C a (succ b)) ⟩
  succ (plus (succ b) a) ＝⟨ ap succ refl ⟩
  succ (succ (plus b a)) ＝⟨ ap (λ x → succ (succ x)) (C b a) ⟩
  succ (succ (plus a b)) ＝⟨ ap succ refl ⟩
  succ (plus (succ a) b) ＝⟨ ap succ (C (succ a) b) ⟩
  succ (plus b (succ a)) ∎

Remind

add1 : ℕ → ℕ
add1 = ℕ-elim (λ _ → ℕ) (succ zero) λ _ n → succ n

t1 : add1  ＝ 
t1 = refl

double' : ℕ → ℕ
double' = ℕ-elim (λ _ → ℕ) zero λ _ mn → succ (succ mn)

t2 : double'  ＝ 
t2 = refl
t3 : double'  ＝ 
t3 = refl
t4 : double'  ＝ 
t4 = refl

{-# OPTIONS --cubical --guardedness --two-level --no-level-universe #-}
module ag-000J where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sum
open import Cubical.Data.Nat

data 𝟘 : Type where
data 𝟙 : Type where
  ⋆ : 𝟙
data Maybe (X : Type) : Type where
  none : Maybe X
  some : X → Maybe X
record ℕ∞ : Type where
  coinductive
  field
    pred∞ : Maybe ℕ∞

M-type 是 non-well-formed, labelled trees 的型別，有可能有有限也可能有無限長的 path。 M 是 strictly positive coinductive types 的 universal type。

record M (S : Type) (P : S → Type) : Type where
  coinductive
  field
    shape : S
    pos : P shape → M S P

M S P 代表了 conatural number

module conatural-number where
  open ℕ∞
  open M

  S = 𝟙 ⊎ 𝟙

  P : S → Type
  P (inl _) = 𝟘
  P (inr _) = 𝟙

  N∞ = M S P

  inf : ℕ∞
  pred∞ inf = none
  inf' : ℕ∞
  pred∞ inf' = some inf

  i : N∞
  shape i = inl ⋆
  pos i = λ ()

  i' : N∞
  shape i' = inr ⋆
  pos i' = λ x → i

{-# OPTIONS --cubical --guardedness --two-level --no-level-universe #-}
module ag-000I where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sum
open import Cubical.Data.Nat

data 𝟘 : Type where
data 𝟙 : Type where
  ⋆ : 𝟙

W-type (due to Martin-Löf) 是 well-founded, labelled trees 的型別。每棵 W-type 的樹都可以有無限多分支，但 path 都是有限長。W 有兩個參數

1. S : Type 表示 shape
2. P : S → Type 表示有 (P s)-many positions

W 是 strictly positive inductive types 的 universal type。

data W (S : Type) (P : S → Type) : Type where
  sup-W : (s : S) → (P s → W S P) → W S P

Example: 自然數

module natural-number where
  S = 𝟙 ⊎ 𝟙

  P : S → Type
  P (inl _) = 𝟘 -- therefore, in this direction cannot go further
  P (inr _) = 𝟙 -- this direction has one continuation

  N = W S P

  z : N
  z = sup-W (inl ⋆) λ ()
  s : N → N
  s n = sup-W (inr ⋆) λ ⋆ → n

  α : ℕ → N
  α zero = z
  α (suc n) = s (α n)
  β : N → ℕ
  β (sup-W (inl ⋆) x) = zero
  β (sup-W (inr ⋆) f) = suc (β (f ⋆))

  main : (n : ℕ) → β (α n) ≡ n
  main zero =
    β (α zero) ≡⟨ refl ⟩
    β z ≡⟨ refl ⟩
    zero ∎
  main (suc n) = cong suc (main n)

  main⁻¹ : (n : N) → α (β n) ≡ n
  main⁻¹ (sup-W (inl ⋆) f) =
    α (β (sup-W (inl ⋆) f)) ≡⟨ refl ⟩
    z                       ≡⟨ refl ⟩
    sup-W (inl ⋆) (λ ())    ≡⟨ cong (sup-W (inl ⋆)) (sym (funExt λ ())) ⟩
    sup-W (inl ⋆) f ∎
  main⁻¹ (sup-W (inr ⋆) f) =
    α (β (sup-W (inr ⋆) f))           ≡⟨ refl ⟩
    α (suc (β (f ⋆)))                 ≡⟨ refl ⟩
    s (α (β (f ⋆)))                   ≡⟨ refl ⟩
    sup-W (inr ⋆) (λ _ → α (β (f ⋆))) ≡⟨ cong (sup-W (inr ⋆)) (funExt t) ⟩
    sup-W (inr ⋆) f ∎
    where
    t : (x : 𝟙) → α (β (f ⋆)) ≡ f x
    t ⋆ = main⁻¹ (f ⋆)

根據定義，每個 simplicial set $S$ 都是 simplex category $\Delta$ 的一個 presheaf

這些 morphism 可以用一類特殊的 maps 組出來，叫做 face maps，舉例來說

這個定義乍一看實在沒辦法理解這在定義什麼，所以要實際看看幾個案例：從 $[0]$ 到 $[1]$ 可以畫成

從 $[1]$ 到 $[2]$ 可以畫成

事實上，如果畫成 simplex 的幾何表示 $\text{Simp}_n$ 就更明顯了：

標準 $n$ -simplex $\text{Simp}_n$ 可以定義成：

所以 face maps 就是在表示 $[n-1]$ 表示 $[n]$ 的哪一個邊界，線的邊界是兩個點，面的邊界是三條線。

在看過

之後的一點嘗試。

就我的認知，有限多的 singular points 無法破壞這裡的拓墣特性，所以討論非碎形曲線的時候，頂多討論能夠減少內接矩形到什麼程度。所以我真正有興趣的是局部構成沒有內接矩形時，如何重複這個構成還是保持特性。

然而一次跨出這步太超出我目前所知了，所以只能先考慮相關的變形問題：首先，開放的曲線可能沒有內接矩形，比如下圖由兩個有界直線構成（箭頭表示無限延伸方向）

1. 如果選擇了頂點與其中一邊的點，那麼法向只能再跟此圖交於一點，無法構成矩形。另一邊因為對稱性所以一樣。
2. 如果選擇一邊的兩點，那法向接觸到另一邊的長度不同，自然也不是矩形。
3. 如果一邊各自選一點，因為這條邊往任意一邊移動都會改變長度，也沒辦法構成矩形。

但這張圖如果稍作修改，比如加一個直線拉回來變成三角形，就會再次有內接矩形。

另一種值得考慮的基本構造是圓，因為可以說圓的內接矩形有無限多個，但也可以說某種程度上只有一個內接矩形。所以如果考慮取半圓形，另一半則是想辦法破壞對稱性，比如我考慮過的其中一種形狀是

想法就是一直取一半直徑的半圓去填右半部。這個旋轉一下就可以弄成方程組，所以要驗證這個圖形可以嘗試看看方程組中出現矩形要怎麼驗證。

Reading https://github.com/ayberkt/formal-topology-in-UF and use TypeTopology to understand

{-# OPTIONS --safe --without-K #-}
module ag-000F where

open import MLTT.Spartan
open import UF.Sets
open import UF.SubtypeClassifier

order-structure : 𝓤 ̇  → 𝓤 ⁺ ̇
order-structure {𝓤} A = A → A → Ω 𝓤

poset-axioms : (A : 𝓤 ̇ ) → order-structure A → 𝓤 ̇
poset-axioms A _≤_ = is-set A
                    × ((x : A) → (x ≤ x) holds)
                    × ((x y z : A) → (x ≤ y) holds → (y ≤ z) holds → (x ≤ z) holds)
                    × ((x y : A) → (x ≤ y) holds → (y ≤ x) holds → x ＝ y)

Poset-structure : 𝓤 ̇  → 𝓤 ⁺ ̇
Poset-structure A = Σ _≤_ ꞉ order-structure A , (poset-axioms A _≤_)

Poset : (𝓤 : Universe) → 𝓤 ⁺ ̇
Poset 𝓤 = Σ A ꞉ 𝓤 ̇ , Poset-structure A

⟨_⟩ : {S : 𝓤 ̇ → 𝓥 ̇ } → Σ S → 𝓤 ̇
⟨ X , s ⟩ = X

order-of : (P : Poset 𝓤) → ⟨ P ⟩ → ⟨ P ⟩ → Ω 𝓤
order-of (X , _≤_ , _) x y = x ≤ y

syntax order-of P x y = x ≤⟨ P ⟩ y

posets-are-sets : (P : Poset 𝓤) → is-set ⟨ P ⟩
posets-are-sets (X , _≤_ , i , rfl , trans , ir) = i

is-hom : (P : Poset 𝓤) (Q : Poset 𝓥) → (⟨ P ⟩ → ⟨ Q ⟩) → 𝓤 ⊔ 𝓥 ̇
is-hom P Q f = ∀ {x y} → (x ≤⟨ P ⟩ y) holds → (f x ≤⟨ Q ⟩ f y) holds

id-is-hom : (P : Poset 𝓤) → is-hom P P id
id-is-hom P x≤y = x≤y

∘-is-hom : (P : Poset 𝓤) (Q : Poset 𝓥) (R : Poset 𝓦)
            (f : ⟨ P ⟩ → ⟨ Q ⟩) (g : ⟨ Q ⟩ → ⟨ R ⟩)
          → is-hom P Q f → is-hom Q R g → is-hom P R (g ∘ f)
∘-is-hom P Q R f g f-is-hom g-is-hom x≤y = g-is-hom (f-is-hom x≤y)

{-# OPTIONS --safe --without-K #-}
module ag-000G where

open import MLTT.Spartan
open import UF.SubtypeClassifier
open import ag-000F

Fam : 𝓤 ̇  → 𝓤 ⁺ ̇
Fam {𝓤} A = Σ I ꞉ 𝓤 ̇ , (I → A)

module JoinStntax {A : 𝓤 ̇ } (join : Fam A → A) where
  join-of : {I : 𝓤 ̇ } → (I → A) → A
  join-of {I} f = join (I , f)

  syntax join-of (λ i → e) = ∨⟨ i ⟩ e

index : {X : 𝓤 ̇ } → Fam X → 𝓤 ̇
index (I , _) = I

_$_ : {X : 𝓤 ̇ } → (F : Fam X) → index F → X
_$_ (_ , f) = f
infixl  _$_

_∈_ : {X : 𝓤 ̇ } → X → Fam X → 𝓤 ̇
x ∈ (_ , f) = fiber f x

frame-axioms : (X : 𝓤 ̇ ) → order-structure X → X → (X → X → X) → (Fam X → X) → 𝓤 ⁺ ̇
frame-axioms X _≤_ ⊤ _∧_ ∨ =
  ((x : X) → (x ≤ ⊤) holds)
  × ((x y : X) → ((x ∧ y) ≤ x) holds × ((x ∧ y) ≤ y) holds)
  × ((x y z : X) → (z ≤ x) holds → (z ≤ y) holds → (z ≤ (x ∧ y)) holds)
  × ((U : Fam X) → (x : X) → x ∈ U → (x ≤ ∨ U) holds)
  × ((U : Fam X) → (x : X) → ((y : X) → y ∈ U → (y ≤ x) holds) → (∨ U ≤ x) holds)
  × distrib
  where
  open JoinStntax ∨
  distrib = ((U : Fam X) → (x : X) → x ∧ (∨ U) ＝ ∨⟨ i ⟩ (x ∧ U $ i))

Frame-structure : 𝓤 ̇  → 𝓤 ⁺ ̇
Frame-structure X =
  Σ _≤_ ꞉ order-structure X ,
  Σ ⊤ ꞉ X ,
  Σ _∧_ ꞉ (X → X → X) ,
  Σ ∨ ꞉ (Fam X → X) ,
  (poset-axioms X _≤_) × (frame-axioms X _≤_ ⊤ _∧_ ∨)

Frame : (𝓤 : Universe) → 𝓤 ⁺ ̇
Frame 𝓤 = Σ X ꞉ 𝓤 ̇ , Frame-structure X

{-# OPTIONS --safe --without-K #-}
module ag-000H where

open import MLTT.Spartan
open import UF.SubtypeClassifier
open import ag-000F
open import ag-000G

meet-is-comm : (F : Frame 𝓤) → (x y : ⟨ F ⟩) → 𝓤 ̇
meet-is-comm (X , _≤_ , ⊤ , _∧_ , _ ) x y = x ∧ y ＝ y ∧ x

prove-meet-is-comm : (F : Frame 𝓤) → (x y : ⟨ F ⟩) → meet-is-comm F x y
prove-meet-is-comm (X , _≤_ , ⊤ , _∧_ , ∨ , (_ , _ , _ , split) , (_ , meet , lim , _ , _) ) x y = split (x ∧ y) (y ∧ x) I II
  where
  I : ((x ∧ y) ≤ (y ∧ x)) holds
  I = lim y x (x ∧ y) (meet x y .pr₂) (meet x y .pr₁)
  II : ((y ∧ x) ≤ (x ∧ y)) holds
  II = lim x y (y ∧ x) (meet y x .pr₂) (meet y x .pr₁)

To see why

behave same as the complex numbers $z_\theta = \cos\theta + i\sin\theta$ is to write $R_\theta$ as a linear combination:

and hence we are wondering, what if we define

and multiplication as matrix multiplication, addition as matrix addition? Are these behave same as complex numbers? Since $\bold{1}$ is the identity matrix, we simply get followings

1. $\bold{1}^2 = \bold{1}$
2. $\bold{1}\bold{i} = \bold{i}\bold{1} = \bold{i}$

we would like to know if $\bold{i}^2 = -\bold{1}$ :

as desired. Then we also know linear combinations based on $\bold{1}$ and $\bold{i}$ maps to complex numbers bijectively:

so now we can see this indeed is a representation of complex numbers.

{-# OPTIONS --without-K #-}
module ag-000E where

open import MLTT.Spartan hiding (_+_; _×_)
open import MLTT.Fin

因為不想引入太多其餘結構，把實數跟三角函數的一些性質直接公理化來用

module _ (ℝ : 𝓤₀ ̇) where
  variable
    a b : ℝ
  postulate
    cos : ℝ → ℝ
    sin : ℝ → ℝ
    -_  : ℝ → ℝ
    _+_ : ℝ → ℝ → ℝ
    _×_ : ℝ → ℝ → ℝ

    tri1 : cos (a + b) ＝ cos a × cos b + - (sin a × sin b)
    tri2 : sin (a + b) ＝ sin a × cos b + sin b × cos a

    ℝ-neg-1 : a × - b ＝ - (a × b)
    ℝ-neg-add : - a + - b ＝ - (a + b)
    ℝ-+-comm : a + b ＝ b + a
    ℝ-×-comm : a × b ＝ b × a
  infixl  -_
  infixl  _+_
  infixl  _×_
  ℝ-neg-2 : - a × b ＝ - (a × b)
  ℝ-neg-2 {a}{b} =
    - a × b   ＝⟨ ℝ-×-comm ⟩
    b × - a   ＝⟨ ℝ-neg-1 ⟩
    - (b × a) ＝⟨ ap -_ ℝ-×-comm ⟩
    - (a × b) ∎

矩陣可以看成由兩個索引指向某其 Field K 的元素的型別

  Matrix : (m n : ℕ) → (K : 𝓤 ̇) → 𝓤 ̇
  Matrix m n K = Fin m → Fin n → K

只定義 2 × 2 的矩陣乘法

  _⊗_ : Matrix   ℝ → Matrix   ℝ → Matrix   ℝ
  _⊗_ m n 𝟎 𝟎 = m 𝟎 𝟎 × n 𝟎 𝟎 + m 𝟎 𝟏 × n 𝟏 𝟎
  _⊗_ m n 𝟎 𝟏 = m 𝟎 𝟎 × n 𝟎 𝟏 + m 𝟎 𝟏 × n 𝟏 𝟏
  _⊗_ m n 𝟏 𝟎 = m 𝟏 𝟎 × n 𝟎 𝟎 + m 𝟏 𝟏 × n 𝟏 𝟎
  _⊗_ m n 𝟏 𝟏 = m 𝟏 𝟎 × n 𝟎 𝟏 + m 𝟏 𝟏 × n 𝟏 𝟏
  infixl  _⊗_

旋轉矩陣它本人，這個用來表示 R_θ，其中 θ ∈ ℝ 是角度的值

  R : ℝ → Matrix   ℝ
  R θ 𝟎 𝟎 = cos θ
  R θ 𝟎 𝟏 = sin θ
  R θ 𝟏 𝟎 = - sin θ
  R θ 𝟏 𝟏 = cos θ

證明目標：R_θR_φ = R_θ + φ

證明方式就是按 component 去證明等式成立。

  thm : {θ φ : ℝ} (i j : Fin ) → (R θ ⊗ R φ) i j ＝ R (θ + φ) i j
  thm {θ}{φ} 𝟎 𝟎 =
    (R θ ⊗ R φ) 𝟎 𝟎                   ＝⟨by-definition⟩
    cos θ × cos φ + sin θ × (- sin φ) ＝⟨ ap (cos θ × cos φ +_) ℝ-neg-1 ⟩
    cos θ × cos φ + - (sin θ × sin φ) ＝⟨ tri1 ⁻¹ ⟩
    cos (θ + φ)                       ＝⟨by-definition⟩
    R (θ + φ) 𝟎 𝟎 ∎
  thm {θ}{φ} 𝟎 𝟏 =
    (R θ ⊗ R φ) 𝟎 𝟏               ＝⟨by-definition⟩
    cos θ × sin φ + sin θ × cos φ ＝⟨ ℝ-+-comm ⟩
    sin θ × cos φ + cos θ × sin φ ＝⟨ ap (sin θ × cos φ +_) ℝ-×-comm ⟩
    sin θ × cos φ + sin φ × cos θ ＝⟨ tri2 ⁻¹ ⟩
    sin (θ + φ)                   ＝⟨by-definition⟩
    R (θ + φ) 𝟎 𝟏 ∎
  thm {θ}{φ} 𝟏 𝟎 =
    (R θ ⊗ R φ) 𝟏 𝟎                       ＝⟨by-definition⟩
    (- sin θ) × cos φ + cos θ × (- sin φ) ＝⟨ ap (_+ cos θ × - sin φ) ℝ-neg-2 ⟩
    - (sin θ × cos φ) + cos θ × (- sin φ) ＝⟨ ap (- (sin θ × cos φ) +_) ℝ-neg-1 ⟩
    - (sin θ × cos φ) + - (cos θ × sin φ) ＝⟨ ℝ-neg-add ⟩
    - (sin θ × cos φ + cos θ × sin φ)     ＝⟨ ap -_ (ap (sin θ × cos φ +_) ℝ-×-comm) ⟩
    - (sin θ × cos φ + sin φ × cos θ)     ＝⟨ ap -_ (tri2 ⁻¹) ⟩
    - sin (θ + φ)                         ＝⟨by-definition⟩
    R (θ + φ) 𝟏 𝟎 ∎
  thm {θ}{φ} 𝟏 𝟏 =
    (R θ ⊗ R φ) 𝟏 𝟏                   ＝⟨by-definition⟩
    - sin θ × sin φ + cos θ × cos φ   ＝⟨ ℝ-+-comm ⟩
    cos θ × cos φ + - sin θ × sin φ   ＝⟨ ap (cos θ × cos φ +_) ℝ-neg-2 ⟩
    cos θ × cos φ + - (sin θ × sin φ) ＝⟨ tri1 ⁻¹ ⟩
    R (θ + φ) 𝟏 𝟏 ∎

  addition : {θ φ : ℝ} (i j : Fin ) → (R θ ⊗ R φ) i j ＝ (R φ ⊗ R θ) i j
  addition {θ} {φ} i j =
    (R θ ⊗ R φ) i j ＝⟨ thm i j ⟩
    R (θ + φ) i j   ＝⟨ ap (λ x → R x i j) ℝ-+-comm ⟩
    R (φ + θ) i j   ＝⟨ thm i j ⁻¹ ⟩
    (R φ ⊗ R θ) i j ∎

From Topology via logic

{-# OPTIONS --safe --without-K --guardedness --no-exact-split #-}
module ag-000D where

open import MLTT.Spartan
open import MLTT.List

Stream can be defined as a coinductive record.

record Stream (A : 𝓤 ̇ ) : 𝓤 ̇ where
  coinductive
  constructor _∷_
  field
    head : A
    tail : Stream A

open Stream

For example a stream of all zero.

zeros : Stream 𝟚
head zeros = ₀
tail zeros = zeros

s ⊨starts o defines a relation that a stream can be realized by a finite observation.

_⊨starts_ : Stream 𝟚 → List 𝟚 → 𝓤₀ ̇
s ⊨starts [] = ₀ ＝ ₀
s ⊨starts (x ∷ xs) = (x ＝ head s) × (tail s ⊨starts xs)

For example, the first bit zeros produces is ₀.

first-bit : zeros ⊨starts [ ₀ ]
first-bit = refl , refl

Every stream can be realized by “no” observation.

realize-by-no-observation : (s : Stream 𝟚) → s ⊨starts []
realize-by-no-observation s = refl

We can define order relation for these finite observations.

_⊇_ : List 𝟚 → List 𝟚 → 𝓤₀ ̇
_ ⊇ [] = ₀ ＝ ₀
[] ⊇ _ = 𝟘
(x ∷ l) ⊇ (x₁ ∷ l2) = (x ＝ x₁) × (l ⊇ l2)

This order has antisymmetric

eq-condition : (l1 l2 : List 𝟚) → l1 ⊇ l2 → l2 ⊇ l1 → l1 ＝ l2
eq-condition [] [] p q = refl
eq-condition (x ∷ l1) (y ∷ l2) (ph , pt) (qh , qt) =
  x ∷ l1 ＝⟨ ap (_∷ l1) ph ⟩
  y ∷ l1 ＝⟨ ap (y ∷_) (eq-condition l1 l2 pt qt) ⟩
  y ∷ l2 ∎

, in fact total, which means a boring order. The order induces refinement of observations: if a observation is subsequence of another observation that realise the stream, then the stream also be realized by this subsequence.

refine-observation : {s : Stream 𝟚} → (l l2 : List 𝟚) → s ⊨starts l → l ⊇ l2 → s ⊨starts l2
refine-observation l2 [] _ _ = refl
refine-observation (x ∷ l) (y ∷ l2) (x=head , tail) (x=y , rest) =
  (x=y ⁻¹ ∙ x=head) , refine-observation l l2 tail rest

這是從 https://mathstodon.xyz/@MartinEscardo/114751426538568913 學到的技巧。

{-# OPTIONS --safe --without-K #-}
module ag-000C where

open import Agda.Primitive
  renaming (Set to Type; Setω to Typeω)
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

假設我們有

1. a type X : Type
2. a family of types A : X → Type indexed by X

那我們常常會遇到有

1. x y : X
2. a : A x
3. b : A y
4. p : x ＝ y

＝ 是 MLTT 的 identity type，p 是一個 x ＝ y 的證明，這時候如果我們問 a ＝ b 是沒有答案的，因為根據 MLTT，a 跟 b 的類型壓根兒就不一樣，這導致問題連寫都寫不下來，那怎麼辦？

方法是定義高階等式（又稱為 dependent equality 或是 PathOver 或是 path transport），在該依賴項等價的情況下把問題變成新的等式來讓 dependent type 語言表達等式

用案例來說就是如果有個 equality 是「類型不同」的（出於依賴項的不透明性，比如這裡 vector length 輸入的 associative 不同）

先定義一些下面案例會用到的輔助程式：

cong : {X Y : Type} (f : X → Y) {x₀ x₁ : X} → x₀ ≡ x₁ → f x₀ ≡ f x₁
cong {X} {Y} f refl = refl

+-assoc : ∀ l m n → (l + m) + n ≡ l + (m + n)
+-assoc zero     m n = refl
+-assoc (suc l) m n = cong suc (+-assoc l m n)

具體案例 vector ++ 的 associativity

data Vec (A : Type) : Nat → Type where
  [] : Vec A 
  _::_ : ∀{n} → A → Vec A n → Vec A (suc n)
infixl  _::_

_++_ : {Y : Type} {l m : Nat} → (xs : Vec Y l) → (ys : Vec Y m) → Vec Y (l + m)
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
infixl  _++_

基於 x₀ ≡ x₁ 定義一個更高階的 equality

higher-equality : {X : Type} (A : X → Type) {x₀ x₁ : X} → A x₀ → x₀ ≡ x₁ → A x₁ → Type
higher-equality A a₀ refl a₁ = a₀ ≡ a₁

但可以根據案例定義比較簡單的版本

_≡[_]_ : {X : Type} {x₀ x₁ : Nat} → Vec X x₀ → x₀ ≡ x₁ → Vec X x₁ → Type
a₀ ≡[ refl ] a₁ = a₀ ≡ a₁

命題 (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs) 無法寫下，因為（meta-level 的）型別不同。 所以需要用高階等式描述

cong-cons : {X : Type} {m n : Nat} {xs : Vec X m} {ys : Vec X n}
  (x : X) (p : m ≡ n)
  → xs ≡[ p ] ys → x :: xs ≡[ cong suc p ] x :: ys
cong-cons {X}{A} x refl refl = refl

++-assoc : {X : Type} (l m n : Nat)
  (xs : Vec X l) (ys : Vec X m) (zs : Vec X n)
  → (xs ++ ys) ++ zs ≡[ +-assoc l m n ] xs ++ (ys ++ zs)
++-assoc {X} zero     m n []       ys zs = refl
++-assoc {X} (suc l) m n (x :: xs) ys zs = I
  where
  I : x :: (xs ++ ys) ++ zs ≡[ cong suc (+-assoc l m n) ] x :: (xs ++ (ys ++ zs))
  I = cong-cons x (+-assoc l m n) (++-assoc l m n xs ys zs)

NOTE about Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics

這篇文章主要在探討程式語法的表示方式，並展示如何結合代數方法跟 HOAS。作者說他們跟隨 Uemura 把語言定義成 second-order generalised algebraic theories (SOGATs)，通過一系列案例揭示 non-substructural languages 可以自然的定義成 SOGATs

1. SOGAT 的形式定義 (using the syntax of a particular SOGAT)
2. 定義兩種 SOGAT signatures 到 GAT signatures (signatures for quotient inductive-inductive types) 的轉換，分別基於同時替換（parallel substitution）與單一替換（single substitution）

Internal language 的觀點可以用來定義程式語言是什麼：有綁定的語言不是一個 GAT，而是一個二階的廣義代數理論（second-order generalised algebraic theory，簡稱 SOGAT），這種理論可以有二階操作（但不是任意高階）。

Untyped 或是 Simply typed 都有被定義成二階理論過，但 Uemura 是第一個用 SOGATs 定義有綁定的語言的人。這個理論真的很厲害，一個語言的 SOGAT 定義比 well-typed quotiented 定義還要抽象：SOGAT 連 contexts 跟 substitutions 都不用提到，這些會自動生成。但這不是一個 well-behaved 的代數理論，比如 second-order models 之間沒有有意義的 homomorphism。

為了描述 SOGAT 的一階模型、homomorphisms 或是 syntax 的 notion，作者把它轉成一個 GAT。這個過程中引入新的 sorts 給 contexts 跟 substitutions，然後把每個操作都用其 context index，second-order 的函數空間也由 context indexing 轉換成 first-order。因此得到一個有 some “correctness by construction” properties 的 GAT，比如每個操作都自動保留替換。這對複雜的理論來說，如果不是從 SOGAT 出發而是直接用其 GAT 表示，那這種屬性並不 trivial。

Cubical type theory 跟有 internal parametricity 的 type theory 都可以定義成 SOGATs，這些方法已經用來證明型別論的屬性。

Substructural (像是 linear or modal) type theories 無法用這篇論文說的方法用 SOGATs 定義，但有時候 presheaves over a substructural theory 提供的 substructural internal language 可以用來描述理論，像是 multi-modal type theory。

簡單的代數理論可以用 signatures 和方程式來表示，也可以 presentation independently 為 Lawvere theories。

GATs 的 syntactic signatures 可以用 preterms 跟 well-formedness relations 定義，也可以 presentation-independent 為 contextual categories 或 categories with families (CwFs) 或 clans。

GATs 的 theory of signatures (ToS) 方法落在 syntactic 跟 presentation-independent 方法中間：signatures 用某個 GAT 語法定義，這是一種設計來專用於定義簽名的類型理論。簽名跟我們在 Agda 裡寫下的 inductive datatype 定義一模一樣：A list (telescope) of the curried types of sorts and constructors。ToS 裡一個 signature 是一個理論的具體表示，但在 well-typed quotiented syntax 這層抽象上給出。這讓我們得到優雅的語意構造，又還是能用 signatures 工作。

SOGATs 同樣可以定義成 syntactically 或 presentation-independently（用 representable map categories 或是 CwFs with locally representable types）

這篇論文貢獻了 ToS 風格的 SOGATs 定義。SOGAT signatures 的理論本身也是 SOGAT，所以這個理論可以描述自己。

避免了循環論證，因為我們首先將 SOGAT 簽名定義為 GAT，從而引導 SOGAT 簽名理論，而 GAT 簽名理論（即 GAT 的語法）本身可以使用 Church 編碼進行引導。

作者開始展示如何把各種 logic 或程式語言定義成代數理論。這邊我寫下每個代數理論的 agda 版本

{-# OPTIONS --safe --without-K #-}
module ag-0003 where

open import MLTT.Spartan

record combinator-calculus : 𝓤₁ ̇ where
  field
    Tm : 𝓤₀ ̇

    _·_ : Tm → Tm → Tm

    K : Tm
    S : Tm

    Kβ : {u f : Tm} → K · u · f ＝ u
    Sβ : {f g u : Tm} → S · f · g · u ＝ f · u · (g · u)

  infixl  _·_

module ag-0004 where

open import MLTT.Spartan

record typed-combinator-calculus : 𝓤₁ ̇ where
  field

    Ty : 𝓤₀ ̇

    Tm : Ty → 𝓤₀ ̇

    ι : Ty
    _⇒_ : Ty → Ty → Ty

    _·_ : {A B : Ty} → Tm (A ⇒ B) → Tm A → Tm B

    K : {A B : Ty} → Tm (A ⇒ B ⇒ A)
    S : {A B C : Ty} → Tm ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C)

    Kβ : {A B : Ty} {u : Tm A} {f : Tm B} → K · u · f ＝ u
    Sβ : {A B C : Ty}
      {f : Tm (A ⇒ B ⇒ C)}
      {g : Tm (A ⇒ B)}
      {u : Tm A}
      → S · f · g · u ＝ f · u · (g · u)

  infixl  _·_
  infixr  _⇒_

module ag-0005 where

open import MLTT.Spartan

record lambda-calculus : 𝓤₁ ̇ where
  field
    Tm : 𝓤₀ ̇

    lam : (Tm → Tm) → Tm
    _·_ : Tm → Tm → Tm

    β : {f : Tm → Tm} {u : Tm} → lam f · u ＝ f u

  infixl  _·_

  Y : Tm
  Y = lam (λ f → (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x))))

  Y-is-fixed-point : {f : Tm} → Y · f ＝ f · (Y · f)
  Y-is-fixed-point {f} =
    Y · f                                                                 ＝⟨by-definition⟩
    lam (λ f → (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))) · f ＝⟨ β ⟩
    (λ f → (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))) f       ＝⟨ refl ⟩
    (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))                 ＝⟨ β ⟩
    f · ((lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x))))           ＝⟨ refl ⟩
    f · ((λ f → (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))) f) ＝⟨ ap (f ·_) (β ⁻¹) ⟩
    f · (Y · f) ∎

module ag-0006 where

open import MLTT.Spartan hiding (_∘_; id)

record first-order-lambda-calculus : 𝓤₁ ̇  where
  field
    Con : 𝓤₀ ̇
    Sub : Con → Con → 𝓤₀ ̇

    _∘_ : {Δ Γ Θ : Con} → Sub Δ Γ → Sub Θ Δ → Sub Θ Γ
    assoc : {A B C D : Con} {γ : Sub C D} {δ : Sub B C} {θ : Sub A B}
      → (γ ∘ δ) ∘ θ ＝ γ ∘ (δ ∘ θ)
    id : {Γ : Con} → Sub Γ Γ
    id-left : {A B : Con} {γ : Sub A B} → id ∘ γ ＝ γ
    id-right : {A B : Con} {γ : Sub A B} → γ ∘ id ＝ γ
    -- empty context: zero
    ◇ : Con
    ε : {Γ : Con} → Sub Γ ◇
    -- terminal
    ◇η : {Γ : Con} → (σ : Sub Γ ◇) → σ ＝ ε

    Tm : Con → 𝓤₀ ̇
    _[_] : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ
    [id] : {Γ : Con} {t : Tm Γ} → t [ id ] ＝ t
    [∘] : {Θ Γ Δ : Con} {t : Tm Γ} {γ : Sub Δ Γ} {δ : Sub Θ Δ} → t [ γ ∘ δ ] ＝ t [ γ ] [ δ ]

    _▹ : Con → Con

    _,,_ : {Δ Γ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹)

    p : {Γ : Con} → Sub (Γ ▹) Γ
    q : {Γ : Con} → Tm (Γ ▹)

    ▹β₁ : {Δ Γ : Con} {γ : Sub Δ Γ} {t : Tm Δ}
      → p ∘ (γ ,, t) ＝ γ
    ▹β₂ : {Δ Γ : Con} {γ : Sub Δ Γ} {t : Tm Δ}
      → q [ γ ,, t ] ＝ t
    ▹η : {Δ Γ : Con} {σ : Sub Δ (Γ ▹)} → σ ＝ (p ∘ σ ,, q [ σ ])

    lam : {Γ : Con} → Tm (Γ ▹) → Tm Γ
    lam[] : {Δ Γ : Con} {γ : Sub Δ Γ} {t : Tm (Γ ▹)} → (lam t)[ γ ] ＝ lam (t [ γ ∘ p ,, q ])

    _·_ : {Γ : Con} → Tm Γ → Tm Γ → Tm Γ
    ·[] : {Δ Γ : Con} {γ : Sub Δ Γ} {t u : Tm Γ} → (t · u)[ γ ] ＝ t [ γ ] · (u [ γ ])

    β : {Δ Γ : Con} {γ : Sub Δ Γ} {t : Tm (Γ ▹)} {u : Tm Γ}
      → lam t · u ＝ t [ id ,, u ]

  infixl  _∘_
  infixl  _,,_
  infixl  _·_
  infixl  _[_]

module ag-0007 where

open import MLTT.Spartan
open import UF.Equiv

record simply-typed-lambda-calculus : 𝓤₁ ̇  where
  field
    Ty : 𝓤₀ ̇
    _⇒_ : Ty → Ty → Ty

    Tm : Ty → 𝓤₀ ̇

    lam : {A B : Ty} → (Tm A → Tm B) → Tm (A ⇒ B)
    _·_ : {A B : Ty} → Tm (A ⇒ B) → (Tm A → Tm B)

    stlc-cong : {A B : Ty} → Tm (A ⇒ B) ≃ (Tm A → Tm B)

module ag-0008 where

open import MLTT.Spartan
open import UF.Subsingletons

record minimal-intuitionistic-first-order-logic : 𝓤₁ ̇  where
  field
    For : 𝓤₀ ̇
    Tm : 𝓤₀ ̇
    _⊃_ : For → For → For
    All : (Tm → For) → For
    Eq : Tm → Tm → For

    Pf : For → 𝓤₀ ̇
    Pf-is-prop : (A : For) → is-prop (Pf A)

    intro⊃ : {A B : For} → (Pf A → Pf B) → Pf (A ⊃ B)
    elim⊃ : {A B : For} → Pf (A ⊃ B) → (Pf A → Pf B)

    intro∀ : {A : Tm → For} → ((𝑡 : Tm) → Pf (A 𝑡)) → Pf (All A)
    elim∀ : {A : Tm → For} → Pf (All A) → ((𝑡 : Tm) → Pf (A 𝑡))

    introEq : {t : Tm} → Pf (Eq t t)
    elimEq : {t t' : Tm} → (A : Tm → For) → Pf (Eq t t') → Pf (A t) → Pf (A t')

module ag-0009 where

open import MLTT.Spartan

record polymorphic-lambda-calculus : 𝓤₁ ̇  where
  field
    Ty : 𝓤₀ ̇
    Tm : Ty → 𝓤₀ ̇
    _⇒_ : Ty → Ty → Ty
    lam : {𝐴 𝐵 : Ty} → (Tm 𝐴 → Tm 𝐵) → Tm (𝐴 ⇒ 𝐵)
    _·_ : {𝐴 𝐵 : Ty} → Tm (𝐴 ⇒ 𝐵) → (Tm 𝐴 → Tm 𝐵)
    All : (Ty → Ty) → Ty
    Lam : {𝐴 : Ty → Ty} → ((𝑋 : Ty) → Tm (𝐴 𝑋)) → Tm (All 𝐴)
    _•_ : {𝐴 : Ty → Ty} → Tm (All 𝐴) → ((𝑋 : Ty) → Tm (𝐴 𝑋))

module ag-000A where

open import MLTT.Spartan

record system-F-ω : 𝓤₁ ̇  where
  field
    □ : 𝓤₀ ̇
    Ty : □ → 𝓤₀ ̇

    _⇛_ : □ → □ → □
    LAM : {K L : □} → (Ty K → Ty L) → Ty (K ⇛ L)
    _●_ : {K L : □} → Ty (K ⇛ L) → (Ty K → Ty L)

    ∗ : □
    Tm : Ty ∗ → 𝓤₀ ̇

    All : {K : □} → (Ty K → Ty ∗) → Ty ∗
    Lam : {K : □}{A : Ty K → Ty ∗} → ((X : Ty K) → Tm (A X)) → Tm (All A)
    _•_ : {K : □}{A : Ty K → Ty ∗} → Tm (All A) → ((X : Ty K) → Tm (A X))

    _⇒_ : Ty ∗ → Ty ∗ → Ty ∗
    lam : {A B : Ty ∗} → (Tm A → Tm B) → Tm (A ⇒ B)
    _·_ : {A B : Ty ∗} → Tm (A ⇒ B) → (Tm A → Tm B)

module ag-000B where

open import MLTT.Spartan
open import MLTT.NaturalNumbers

variable
  𝑖 : ℕ

record minimal-martin-lof-type-theory : 𝓤₁ ̇  where
  field
    Ty : ℕ → 𝓤₀ ̇
    U : (𝑖 : ℕ) → Ty (succ 𝑖)
    Tm : Ty 𝑖 → 𝓤₀ ̇

    c : Ty 𝑖 → Tm (U 𝑖)
    El : Tm (U 𝑖) → Ty 𝑖

    PI : (A : Ty 𝑖) → (Tm A → Ty 𝑖) → Ty 𝑖
    Lift : Ty 𝑖 → Ty (succ 𝑖)

    lam : {𝐴 : Ty 𝑖}{𝐵 : Tm 𝐴 → Ty 𝑖} → ((𝑎 : Tm 𝐴) → Tm (𝐵 𝑎)) → Tm (PI 𝐴 𝐵)
    _·_ : {𝐴 : Ty 𝑖}{𝐵 : Tm 𝐴 → Ty 𝑖} → Tm (PI 𝐴 𝐵) → ((𝑎 : Tm 𝐴) → Tm (𝐵 𝑎))

    mk : {𝐴 : Ty 𝑖} → Tm 𝐴 → Tm (Lift 𝐴)
    un : {𝐴 : Ty 𝑖} → Tm (Lift 𝐴) → Tm 𝐴