{-# 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-BQXB
    (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; _×ᵣ_)

Per component提出證明，依賴的部分要靠 B U ＝ B V 把證明在 B (Fst X) 與 B (Fst Y) 之間搬移

  Σ-is-PER : {A : Rel} {B : 𝓟 ℕ → Rel}
       → is-PER A
       → ((U : 𝓟 ℕ) → is-PER (B U))
       → ({U V : 𝓟 ℕ} → U [ A ] V → B U ＝ B V)
       → is-PER (Σᵣ A B)
  Σ-is-PER {A}{B} per-A per-B resp = I , II
    where
    I : symmetric (Σᵣ A B)
    I X Y (p , q) =
      PER-symm per-A (Fst X) (Fst Y) p ,
      PER-symm (per-B (Fst Y)) (Snd X) (Snd Y)
        (transport (λ R → Snd X [ R ] Snd Y) (resp p) q)
    II : transitive (Σᵣ A B)
    II X Y Z (p₁ , q₁) (p₂ , q₂) =
      PER-trans per-A (Fst X) (Fst Y) (Fst Z) p₁ p₂ ,
      PER-trans (per-B (Fst X)) (Snd X) (Snd Y) (Snd Z) q₁
        (transport (λ R → Snd Y [ R ] Snd Z) (resp p₁ ⁻¹) q₂)

結構與 _=>_ 相同，只是每次套用後都要把型別 B Y 搬回 B X

  Π-is-PER : {A : Rel} {B : 𝓟 ℕ → Rel}
       → is-PER A
       → ((U : 𝓟 ℕ) → is-PER (B U))
       → ({U V : 𝓟 ℕ} → U [ A ] V → B U ＝ B V)
       → is-PER (Πᵣ A B)
  Π-is-PER {A}{B} per-A per-B resp = I , II
    where
    I : symmetric (Πᵣ A B)
    I F G F[Π]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

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

      apply' : (F ⊙ Y) [ B X ] (G ⊙ X)
      apply' = transport (λ R → (F ⊙ Y) [ R ] (G ⊙ X)) (resp Y[A]X) apply

      goal : (G ⊙ X) [ B X ] (F ⊙ Y)
      goal = PER-symm (per-B X) (F ⊙ Y) (G ⊙ X) apply'
    II : transitive (Πᵣ A B)
    II F G H F[Π]G G[Π]H X Y X[A]Y = goal
      where
      apply₁ : (F ⊙ X) [ B X ] (G ⊙ Y)
      apply₁ = F[Π]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 Y ] (H ⊙ Y)
      apply₂ = G[Π]H Y Y Y[A]Y

      apply₂' : (G ⊙ Y) [ B X ] (H ⊙ Y)
      apply₂' = transport (λ R → (G ⊙ Y) [ R ] (H ⊙ Y)) (resp Y[A]X) apply₂

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

當 B 是常數族時，Σᵣ 就是 product，Πᵣ 就是 exponentiation

  Σ-generalizes-× : {A B : Rel} (X Y : 𝓟 ℕ)
    → Σᵣ A (λ _ → B) X Y ＝ (A ×ᵣ B) X Y
  Σ-generalizes-× X Y = refl

  Π-generalizes-=> : {A B : Rel} (F G : 𝓟 ℕ)
    → Πᵣ A (λ _ → B) F G ＝ (A => B) F G
  Π-generalizes-=> F G = refl