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

  module ag-NN5N
    (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; encode; PER-symm; PER-trans)

首先我們需要針對程式的projection 1跟projection 2

Fst Snd : 𝓟 ℕ → 𝓟 ℕ
Fst X n = X (encode (0 , n))
Snd X n = X (encode (1 , n))

Definition Product [local-1]

我們把product定義成

程式的第一部分有類型 $A$ : Fst X [ A ] Fst Y
且程式的第二部分有類型 $B$ : Snd X [ B ] Snd Y

時，X [ A ×ᵣ B ] Y

  _×ᵣ_ : Rel → Rel → Rel
  (A ×ᵣ B) X Y = (Fst X [ A ] Fst Y) × (Snd X [ B ] Snd Y)
  infixr 55 _×ᵣ_

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

證明 A ×ᵣ B 依然是一個PER，不難看出證明就是per component而已

  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 (XA , XB) =
      PER-symm per-A (Fst X) (Fst Y) XA ,
      PER-symm per-B (Snd X) (Snd Y) XB
    II : transitive (A ×ᵣ B)
    II X Y Z (XA , XB) (YA , YB) =
      PER-trans per-A (Fst X) (Fst Y) (Fst Z) XA YA ,
      PER-trans per-B (Snd X) (Snd Y) (Snd Z) XB YB

PER as types: product [ag-NN5N]

Details [local-0]

Definition Product [local-1]

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