{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Size
open import UF.Logic

module ag-V7YV
  (pt : propositional-truncations-exist)
  (fe : Fun-Ext)
  (pe : propext 𝓤)
  (ρ  : propositional-resizing (𝓤 ⁺) 𝓤)
  where

open Conjunction
open Universal   fe
open Implication fe

open import ag-UAEO pt fe pe ρ
open import ag-GY8B pt fe pe ρ

(⇐) 方向：由 L f p 與 L g p 可以得出 L (f ∧ g) p。

L-preserves-∧-⇐ : (f g : Ω 𝓤 → Ω 𝓤) (p : Ω 𝓤)
               → (L f p holds × L g p holds)
               → L (λ x → f x ∧ g x) p holds
L-preserves-∧-⇐ f g p (Lfp , Lgp) = ηL (λ x → f x ∧ g x) p I
  where
  Lf = εL f p Lfp
  Lg = εL g p Lgp

  I : (L⁺ (λ x → f x ∧ g x) p) holds
  I s (p⇒s , fs∧gs⇒s) = Lf s (p⇒s , fs⇒s)
    where
    fs⇒s : f s holds → s holds
    fs⇒s fs = Lg s (p⇒s , gs⇒s)
      where
      gs⇒s : g s holds → s holds
      gs⇒s gs = fs∧gs⇒s (fs , gs)

(⇒) 方向由 L-operator-mono（一個輔助證明：f ≼ g 蘊涵 L f ≼ L g）配上 f ∧ g ≼ f、f ∧ g ≼ g 得到。

L-operator-mono : (f g : Ω 𝓤 → Ω 𝓤)
                → (f ≼ g) holds
                → (L f ≼ L g) holds
L-operator-mono f g f≼g p lfp = ηL g p I
  where
  I : (L⁺ g p) holds
  I q (p⇒q , gq⇒q) = εL f p lfp q (p⇒q , fq⇒q)
    where
    fq⇒q : (f q ⇒ q) holds
    fq⇒q x = gq⇒q (f≼g q x)

L-preserves-∧-⇒ : (f g : Ω 𝓤 → Ω 𝓤) (p : Ω 𝓤)
               → L (λ x → f x ∧ g x) p holds
               → (L f p holds × L g p holds)
L-preserves-∧-⇒ f g p lfgp = to-f , to-g
  where
  to-f : L f p holds
  to-f = L-operator-mono (λ x → f x ∧ g x) f (λ q → pr₁) p lfgp

  to-g : L g p holds
  to-g = L-operator-mono (λ x → f x ∧ g x) g (λ q → pr₂) p lfgp

兩個方向合併就得到逐點的等式 L (f ∧ g) p ＝ L f p ∧ L g p

L-preserves-∧ : (f g : Ω 𝓤 → Ω 𝓤) (p : Ω 𝓤)
             → L (λ x → f x ∧ g x) p ＝ L f p ∧ L g p
L-preserves-∧ f g p = Ω-extensionality pe fe (L-preserves-∧-⇒ f g p)
                                             (L-preserves-∧-⇐ f g p)