--------------------------------------------------------------------------------
title:          Transporting a distributive lattice along an equivalence
author:         Ayberk Tosun
date-started:   2024-04-22
date-completed: 2024-04-30
--------------------------------------------------------------------------------

Given a distributive lattice `L : 𝓤` and an equivalence of the carrier set

    `e : ⟨ L ⟩ ≃ Aᶜ`

to some type `Aᶜ : 𝓥`, we can transport the distributive lattice `L` to
live in universe `𝓥` by copying over the distributive lattice structure from
`L` onto `Aᶜ`.

In this module, we prove this fact, and define some machinery for working with
such copies.

The superscript `(-)ᶜ` is intended to be mnemonic for "copy". We use this
convention to distinguish all distributive lattice operations from their copies
on `Aᶜ`.

\begin{code}

{-# OPTIONS --safe --without-K --lossy-unification #-}

open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Size
open import UF.SubtypeClassifier
open import UF.UA-FunExt
open import UF.Univalence

module Locales.DistributiveLattice.Resizing
        (ua : Univalence)
        (pt : propositional-truncations-exist)
        (sr : Set-Replacement pt)
       where

private
 fe : Fun-Ext
 fe {𝓤} {𝓥} = univalence-gives-funext' 𝓤 𝓥 (ua 𝓤) (ua (𝓤 ⊔ 𝓥))

open import Locales.Compactness.Definition pt fe
open import Locales.DistributiveLattice.Definition fe pt
open import Locales.DistributiveLattice.Homomorphism fe pt
open import Locales.DistributiveLattice.Isomorphism fe pt
open import Locales.Frame pt fe
open import UF.Equiv
open import UF.Logic
open import UF.Sets-Properties

open AllCombinators pt fe hiding (_∧_; _∨_)
open Locale
open PropositionalTruncation pt hiding (_∨_)

\end{code}

We work in an anonymous module parameterized by a distributive lattice `L : 𝓤`,
a type `A : 𝓥`, and an equivalence `e : ⟨ L ⟩ ≃ A`.

\begin{code}

module DistributiveLatticeResizing (L  : DistributiveLattice 𝓤)
                                   (Aᶜ : 𝓥  ̇)
                                   (e  : ∣ L ∣ᵈ ≃ Aᶜ) where

 open DistributiveLattice L renaming (𝟏 to 𝟏L; 𝟎 to 𝟎L)

 s : ∣ L ∣ᵈ → Aᶜ
 s = ⌜ e ⌝

 r : Aᶜ → ∣ L ∣ᵈ
 r = inverse ⌜ e ⌝ (⌜⌝-is-equiv e)

\end{code}

The copy of the meet operation on type `A` is denoted `_∧ᶜ_` and is defined as:

\begin{code}

 _∧ᶜ_ : Aᶜ → Aᶜ → Aᶜ
 _∧ᶜ_ = λ x y → s (r x ∧ r y)

\end{code}

We can now prove that `s` and `r` map the two meet operations onto each other.

\begin{code}

 r-preserves-∧ : (x y : Aᶜ) → r (x ∧ᶜ y) ＝ r x ∧ r y
 r-preserves-∧ x y = inverses-are-retractions' e (r x ∧ r y)

 s-preserves-∧ : (x y : X) → s (x ∧ y) ＝ s x ∧ᶜ s y
 s-preserves-∧ x y = s (x ∧ y)             ＝⟨ Ⅰ ⟩
                     s (x ∧ r (s y))       ＝⟨ Ⅱ ⟩
                     s (r (s x) ∧ r (s y)) ∎
                      where
                       Ⅰ = ap (λ - → s (x ∧ -)) (inverses-are-retractions' e y) ⁻¹
                       Ⅱ = ap (λ - → s (- ∧ r (s y))) (inverses-are-retractions' e x ⁻¹)

\end{code}

Now, we do exactly the same thing for the join operation.

\begin{code}

 _∨ᶜ_ : Aᶜ → Aᶜ → Aᶜ
 _∨ᶜ_ = λ x y → s (r x ∨ r y)

 r-preserves-∨ : (x y : Aᶜ) → r (x ∨ᶜ y) ＝ r x ∨ r y
 r-preserves-∨ x y = inverses-are-retractions' e (r x ∨ r y)

 s-preserves-∨ : (x y : X) → s (x ∨ y) ＝ s x ∨ᶜ s y
 s-preserves-∨ x y =
  s (x ∨ y)                ＝⟨ Ⅰ    ⟩
  s (x ∨ r (s y))          ＝⟨ Ⅱ    ⟩
  s (r (s x) ∨ r (s y))    ＝⟨ refl ⟩
  s x ∨ᶜ s y               ∎
   where
    Ⅰ = ap (λ - → s (x ∨ -)) (inverses-are-retractions' e y ⁻¹)
    Ⅱ = ap (λ - → s (- ∨ r (s y))) (inverses-are-retractions' e x ⁻¹)

\end{code}

The bottom element of the new lattice is just `s 𝟎`

\begin{code}

 𝟎ᶜ : Aᶜ
 𝟎ᶜ = s 𝟎L

\end{code}

The top element is `s 𝟏`.

\begin{code}

 𝟏ᶜ : Aᶜ
 𝟏ᶜ = s 𝟏L

\end{code}

We now proceed to prove that `(Aᶜ , 𝟎ᶜ , 𝟏ᶜ , _∧ᶜ_ , _∨ᶜ_)` forms a
distributive lattice. We refer to this as the _𝓥-small copy_ of `L`.

We start with the unit laws.

\begin{code}

 ∧ᶜ-unit : (x : Aᶜ) → x ∧ᶜ 𝟏ᶜ ＝ x
 ∧ᶜ-unit x =
  s (r x ∧ r (s 𝟏L)) ＝⟨ Ⅰ ⟩
  s (r x ∧ 𝟏L)       ＝⟨ Ⅱ ⟩
  s (r x)            ＝⟨ Ⅲ ⟩
  x                  ∎
   where
    Ⅰ = ap (λ - → s (r x ∧ -)) (inverses-are-retractions' e 𝟏L)
    Ⅱ = ap s (∧-unit (r x))
    Ⅲ = inverses-are-sections' e x


 ∨ᶜ-unit : (x : Aᶜ) → x ∨ᶜ 𝟎ᶜ ＝ x
 ∨ᶜ-unit x =
  s (r x ∨ r (s 𝟎L)) ＝⟨ Ⅰ ⟩
  s (r x ∨ 𝟎L)       ＝⟨ Ⅱ ⟩
  s (r x)            ＝⟨ Ⅲ ⟩
  x                  ∎
   where
    Ⅰ = ap (λ - → s (r x ∨ -)) (inverses-are-retractions' e 𝟎L)
    Ⅱ = ap s (∨-unit (r x))
    Ⅲ = inverses-are-sections' e x

\end{code}

Associativity laws.

\begin{code}

 ∧ᶜ-is-associative : (x y z : Aᶜ) → x ∧ᶜ (y ∧ᶜ z) ＝ (x ∧ᶜ y) ∧ᶜ z
 ∧ᶜ-is-associative x y z =
  x ∧ᶜ (y ∧ᶜ z)                ＝⟨ refl ⟩
  s (r x ∧ r (s (r y ∧ r z)))  ＝⟨ Ⅰ    ⟩
  s (r x ∧ (r y ∧ r z))        ＝⟨ Ⅱ    ⟩
  s ((r x ∧ r y) ∧ r z)        ＝⟨ Ⅲ    ⟩
  s (r (s (r x ∧ r y)) ∧ r z)  ＝⟨ refl ⟩
  s (r (s (r x ∧ r y)) ∧ r z)  ＝⟨ refl ⟩
  (x ∧ᶜ y) ∧ᶜ z                ∎
   where
    Ⅰ = ap (λ - → s (r x ∧ -)) (inverses-are-retractions' e (r y ∧ r z))
    Ⅱ = ap s (∧-associative (r x) (r y) (r z))
    Ⅲ = ap (λ - → s (- ∧ r z)) (inverses-are-retractions' e (r x ∧ r y) ⁻¹)

 ∨ᶜ-associative : (x y z : Aᶜ) → x ∨ᶜ (y ∨ᶜ z) ＝ (x ∨ᶜ y) ∨ᶜ z
 ∨ᶜ-associative x y z =
  x ∨ᶜ (y ∨ᶜ z)                ＝⟨ refl ⟩
  s (r x ∨ r (s (r y ∨ r z)))  ＝⟨ Ⅰ    ⟩
  s (r x ∨ (r y ∨ r z))        ＝⟨ Ⅱ    ⟩
  s ((r x ∨ r y) ∨ r z)        ＝⟨ Ⅲ    ⟩
  s (r (s (r x ∨ r y)) ∨ r z)  ＝⟨ refl ⟩
  s (r (s (r x ∨ r y)) ∨ r z)  ＝⟨ refl ⟩
  (x ∨ᶜ y) ∨ᶜ z                ∎
   where
    Ⅰ = ap (λ - → s (r x ∨ -)) (inverses-are-retractions' e (r y ∨ r z))
    Ⅱ = ap s (∨-associative (r x) (r y) (r z))
    Ⅲ = ap (λ - → s (- ∨ r z)) (inverses-are-retractions' e (r x ∨ r y) ⁻¹)

\end{code}

Commutativity laws.

\begin{code}

 ∧ᶜ-is-commutative : (x y : Aᶜ) → x ∧ᶜ y ＝ y ∧ᶜ x
 ∧ᶜ-is-commutative x y = ap s (∧-commutative (r x) (r y))

 ∨ᶜ-commutative : (x y : Aᶜ) → x ∨ᶜ y ＝ y ∨ᶜ x
 ∨ᶜ-commutative x y = ap s (∨-commutative (r x) (r y))

\end{code}

Idempotency laws.

\begin{code}

 ∧ᶜ-idempotent : (x : Aᶜ) → x ∧ᶜ x ＝ x
 ∧ᶜ-idempotent x =
  s (r x ∧ r x) ＝⟨ Ⅰ ⟩
  s (r x)       ＝⟨ Ⅱ ⟩
  x             ∎
   where
    Ⅰ = ap s (∧-idempotent (r x))
    Ⅱ = inverses-are-sections' e x

 ∨ᶜ-idempotent : (x : Aᶜ) → x ∨ᶜ x ＝ x
 ∨ᶜ-idempotent x =
   s (r x ∨ r x) ＝⟨ Ⅰ ⟩
   s (r x)       ＝⟨ Ⅱ ⟩
   x             ∎
    where
     Ⅰ = ap s (∨-idempotent (r x))
     Ⅱ = inverses-are-sections' e x

\end{code}

Absorption laws.

\begin{code}

 ∧ᶜ-absorptive : (x y : Aᶜ) → x ∧ᶜ (x ∨ᶜ y) ＝ x
 ∧ᶜ-absorptive x y =
  s (r x ∧ r (s (r x ∨ r y)))   ＝⟨ Ⅰ ⟩
  s (r x ∧ (r x ∨ r y))         ＝⟨ Ⅱ ⟩
  s (r x)                       ＝⟨ Ⅲ ⟩
  x                             ∎
   where
    Ⅰ = ap (λ - → s (r x ∧ -)) (inverses-are-retractions' e (r x ∨ r y))
    Ⅱ = ap s (∧-absorptive (r x) (r y))
    Ⅲ = inverses-are-sections' e x

 ∨ᶜ-absorptive : (x y : Aᶜ) → x ∨ᶜ (x ∧ᶜ y) ＝ x
 ∨ᶜ-absorptive x y =
  x ∨ᶜ (x ∧ᶜ y)                 ＝⟨ refl ⟩
  s (r x ∨ r (s (r x ∧ r y)))   ＝⟨ Ⅰ    ⟩
  s (r x ∨ (r x ∧ r y))         ＝⟨ Ⅱ    ⟩
  s (r x)                       ＝⟨ Ⅲ    ⟩
  x                             ∎
   where
    Ⅰ = ap (λ - → s (r x ∨ -)) (inverses-are-retractions' e (r x ∧ r y))
    Ⅱ = ap s (∨-absorptive (r x) (r y))
    Ⅲ = inverses-are-sections' e x

\end{code}

Finally, the distributivity law.

\begin{code}

 distributivityᶜ : (x y z : Aᶜ) → x ∧ᶜ (y ∨ᶜ z) ＝ (x ∧ᶜ y) ∨ᶜ (x ∧ᶜ z)
 distributivityᶜ x y z =
  x ∧ᶜ (y ∨ᶜ z)                             ＝⟨ refl ⟩
  s (r x ∧ r (s (r y ∨ r z)))               ＝⟨ Ⅰ    ⟩
  s (r x ∧ (r y ∨ r z))                     ＝⟨ Ⅱ    ⟩
  s ((r x ∧ r y) ∨ (r x ∧ r z))             ＝⟨ Ⅲ    ⟩
  s ((r x ∧ r y) ∨ r (s (r x ∧ r z)))       ＝⟨ Ⅳ    ⟩
  s (r (s (r x ∧ r y)) ∨ r (s (r x ∧ r z))) ＝⟨ refl ⟩
  s (r (x ∧ᶜ y) ∨ r (x ∧ᶜ z))               ＝⟨ refl ⟩
  (x ∧ᶜ y) ∨ᶜ (x ∧ᶜ z)                      ∎
   where
    Ⅰ = ap (λ - → s (r x ∧ -)) (inverses-are-retractions' e (r y ∨ r z))
    Ⅱ = ap s (distributivityᵈ (r x) (r y) (r z))
    Ⅲ = ap (λ - → s ((r x ∧ r y) ∨ -)) (inverses-are-retractions' e (r x ∧ r z) ⁻¹)
    Ⅳ = ap (λ - → s (- ∨ r (s (r x ∧ r z)))) (inverses-are-retractions' e (r x ∧ r y) ⁻¹)

\end{code}

We package everything up into `copyᵈ` below.

\begin{code}

 Lᶜ : DistributiveLattice 𝓥
 Lᶜ = record
       { X               = Aᶜ
       ; 𝟏               = 𝟏ᶜ
       ; 𝟎               = 𝟎ᶜ
       ; _∧_             = _∧ᶜ_
       ; _∨_             = _∨ᶜ_
       ; X-is-set        = equiv-to-set
                            (≃-sym e)
                            carrier-of-[ poset-ofᵈ L ]-is-set
       ; ∧-associative   = ∧ᶜ-is-associative
       ; ∧-commutative   = ∧ᶜ-is-commutative
       ; ∧-unit          = ∧ᶜ-unit
       ; ∧-idempotent    = ∧ᶜ-idempotent
       ; ∧-absorptive    = ∧ᶜ-absorptive
       ; ∨-associative   = ∨ᶜ-associative
       ; ∨-commutative   = ∨ᶜ-commutative
       ; ∨-unit          = ∨ᶜ-unit
       ; ∨-idempotent    = ∨ᶜ-idempotent
       ; ∨-absorptive    = ∨ᶜ-absorptive
       ; distributivityᵈ = distributivityᶜ
       }

 ⦅_⦆ᶜ : DistributiveLattice 𝓥
 ⦅_⦆ᶜ = Lᶜ

 s-preserves-𝟏 : preserves-𝟏 L Lᶜ s holds
 s-preserves-𝟏 = refl

 s-preserves-𝟎 : preserves-𝟎 L Lᶜ s holds
 s-preserves-𝟎 = refl

\end{code}

We package `s` up with the proof that it is a homomorphism, and call it
`sₕ`.

\begin{code}

 sₕ : L ─d→ Lᶜ
 sₕ =
  record
   { h                 = s
   ; h-is-homomorphism = α , β , γ , δ
   }
    where
     α : preserves-𝟏 L Lᶜ s holds
     α = refl

     β : preserves-∧ L Lᶜ s holds
     β = s-preserves-∧

     γ : preserves-𝟎 L Lᶜ s holds
     γ = s-preserves-𝟎

     δ : preserves-∨ L Lᶜ s holds
     δ = s-preserves-∨

\end{code}

Now, we we do the same thing for `r`

\begin{code}

 rₕ : Lᶜ ─d→ L
 rₕ =
  record
   { h                 = r
   ; h-is-homomorphism = α , β , γ , δ
   }
    where
     α : preserves-𝟏 Lᶜ L r holds
     α = inverses-are-retractions' e 𝟏L

     β : preserves-∧ Lᶜ L r holds
     β = r-preserves-∧

     γ : preserves-𝟎 Lᶜ L r holds
     γ = inverses-are-retractions' e 𝟎L

     δ : preserves-∨ Lᶜ L r holds
     δ = r-preserves-∨

 s-is-homomorphism : is-homomorphismᵈ L Lᶜ s holds
 s-is-homomorphism = Homomorphismᵈᵣ.h-is-homomorphism sₕ

 r-is-homomorphism : is-homomorphismᵈ Lᶜ L r holds
 r-is-homomorphism = Homomorphismᵈᵣ.h-is-homomorphism rₕ

\end{code}

Combining the fact that `s` and `r` are parts of an equivalence with the rather
trivial proof that they are homomorphisms with respect to `Lᶜ`, we obtain
the fact that `L` is isomorphic to its 𝓥-small copy.

\begin{code}

 open DistributiveLatticeIsomorphisms

 copy-isomorphic-to-original : L ≅d≅ Lᶜ
 copy-isomorphic-to-original =
  record
   { 𝓈           = sₕ
   ; 𝓇           = rₕ
   ; r-cancels-s = inverses-are-retractions' e
   ; s-cancels-r = inverses-are-sections' e
   }

\end{code}