Details [local-0]

  {-# OPTIONS --safe --without-K #-}
  open import MLTT.Spartan
  open import UF.Powerset
  open import UF.PropTrunc
  open import UF.FunExt
  open import UF.Subsingletons
  open import UF.DiscreteAndSeparated using (ℕ-is-set)
  open import Naturals.Properties using (positive-not-zero)

  module ag-MM24
    (pt : propositional-truncations-exist)
    (fe : Fun-Ext)
    (pe : propext 𝓤₀)
    where

  open import ag-U75Z using (_[_]_; is-PER)
  open import ag-KA1U pt fe pe using (Rel; PER-symm; PER-trans)
  open import ag-NN5N pt fe pe using (Fst; Snd)

tag 取成 singleton：｛ m ｝ 就是只含 m 的集合

｛_｝ : ℕ → 𝓟 ℕ
｛ m ｝ n = (m ＝ n) , ℕ-is-set

X = (｛0｝ , X0) 可以表示成 Fst X ＝｛ 0 ｝ 且 Snd X = X0，inr同理

is-inl is-inr : 𝓟 ℕ → 𝓤₁ ̇
is-inl X = Fst X ＝ ｛ 0 ｝
is-inr X = Fst X ＝ ｛ 1 ｝

輔助引理證明不可能既是inl又是inr

inl-and-inr-is-impossible : (X : 𝓟 ℕ) → is-inl X → is-inr X → 𝟘
inl-and-inr-is-impossible X p q =
  positive-not-zero 0 (transport (0 ∈_) (p ⁻¹ ∙ q) refl)

Definition Sum [local-1]

我們把sum定義成

要嘛兩邊都是inl、且 Snd X [ A ] Snd Y
不然就是兩邊都是inr、且 Snd X [ B ] Snd Y

  _+ᵣ_ : Rel → Rel → Rel
  (A +ᵣ B) X Y = (is-inl X × is-inl Y × (Snd X [ A ] Snd Y))
               + (is-inr X × is-inr Y × (Snd X [ B ] Snd Y))
  infixr 54 _+ᵣ_

Sum of PER依然是PER [local-2]

A +ᵣ B 依然是PER。symmetric跟transitivity的同向情況都是per component；混合情況用 inl-and-inr-is-impossible 推出矛盾排除

  A+B-is-PER : {A B : Rel}
       → is-PER A
       → is-PER B
       → is-PER (A +ᵣ B)
  A+B-is-PER {A}{B} per-A per-B = I , II
    where
    I : symmetric (A +ᵣ B)
    I X Y (inl (lX , lY , XA)) =
      inl (lY , lX , PER-symm per-A (Snd X) (Snd Y) XA)
    I X Y (inr (rX , rY , XB)) =
      inr (rY , rX , PER-symm per-B (Snd X) (Snd Y) XB)
    II : transitive (A +ᵣ B)
    II X Y Z (inl (lX , _ , XA)) (inl (_ , lZ , YA)) =
      inl (lX , lZ , PER-trans per-A (Snd X) (Snd Y) (Snd Z) XA YA)
    II X Y Z (inr (rX , _ , XB)) (inr (_ , rZ , YB)) =
      inr (rX , rZ , PER-trans per-B (Snd X) (Snd Y) (Snd Z) XB YB)
    II X Y Z (inl (_ , lY , _)) (inr (rY , _ , _)) =
      𝟘-elim (inl-and-inr-is-impossible Y lY rY)
    II X Y Z (inr (_ , rY , _)) (inl (lY , _ , _)) =
      𝟘-elim (inl-and-inr-is-impossible Y lY rY)

PER as types: sum [ag-MM24]

Details [local-0]

Definition Sum [local-1]

Sum of PER依然是PER [local-2]