---
layout: default
title : "Setoid.Varieties.Closure module (The Agda Universal Algebra Library)"
date : "2021-01-14"
author: "agda-algebras development team"
---

#### Closure Operators for Setoid Algebras

Fix a signature 𝑆, let 𝒦 be a class of 𝑆-algebras, and define

+  `H 𝒦` = algebras isomorphic to a homomorphic image of a member of `𝒦`;
+  `S 𝒦` = algebras isomorphic to a subalgebra of a member of `𝒦`;
+  `P 𝒦` = algebras isomorphic to a product of members of `𝒦`.

<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

open import Overture using (π“ž ; π“₯ ; Signature)

module Setoid.Varieties.Closure {𝑆 : Signature π“ž π“₯} where

open import Agda.Primitive using () renaming ( Set to Type )

-- imports from the Agda Standard Library ----------------------------------------
open import Data.Product           using ( _,_ ; Ξ£-syntax )
                                   renaming ( _Γ—_ to _∧_ )
open import Data.Unit.Polymorphic  using ( ⊀ ; tt )
open import Function               using () renaming ( Func to _⟢_ )
open import Level                  using ( Level ;  _βŠ”_ )
open import Relation.Binary        using ( Setoid )
open import Relation.Unary         using ( Pred ; _∈_ ; _βŠ†_ )

-- Imports from the Agda Universal Algebra Library -------------------------------
open import Setoid.Algebras {𝑆 = 𝑆} using ( Algebra ; ov ; Lift-Alg ; β¨… )
open import Setoid.Homomorphisms {𝑆 = 𝑆}
open import Setoid.Subalgebras {𝑆 = 𝑆}
open _⟢_ renaming ( to to _⟨$⟩_ )
```
-->

```agda
module _ {Ξ± ρᡃ Ξ² ρᡇ : Level} where

  private
    a b : Level
    a = Ξ± βŠ” ρᡃ ; b = Ξ² βŠ” ρᡇ

  Level-closure : βˆ€ β„“ β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov β„“) β†’ Pred(Algebra Ξ² ρᡇ) (b βŠ” ov(a βŠ” β„“))
  Level-closure β„“ 𝒦 𝑩 = Ξ£[ 𝑨 ∈ Algebra Ξ± ρᡃ ] 𝑨 ∈ 𝒦 ∧ 𝑨 β‰… 𝑩

module _ {Ξ± ρᡃ Ξ² ρᡇ : Level} where

  Lift-closed : βˆ€ β„“ β†’ {𝒦 : Pred(Algebra Ξ± ρᡃ) _}{𝑨 : Algebra Ξ± ρᡃ}
    β†’ 𝑨 ∈ 𝒦 β†’ Lift-Alg 𝑨 Ξ² ρᡇ ∈ (Level-closure β„“ 𝒦)
  Lift-closed _ {𝑨 = 𝑨} kA = 𝑨 , (kA , Lift-β‰…)

  private
    a b : Level
    a = Ξ± βŠ” ρᡃ ; b = Ξ² βŠ” ρᡇ

  H S : βˆ€ β„“ β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov β„“) β†’ Pred(Algebra Ξ² ρᡇ) (b βŠ” ov(a βŠ” β„“))
  H _ 𝒦 𝑩 = Ξ£[ 𝑨 ∈ Algebra Ξ± ρᡃ ] 𝑨 ∈ 𝒦 ∧ 𝑩 IsHomImageOf 𝑨
  S _ 𝒦 𝑩 = Ξ£[ 𝑨 ∈ Algebra Ξ± ρᡃ ] 𝑨 ∈ 𝒦 ∧ 𝑩 ≀ 𝑨

  P : βˆ€ β„“ ΞΉ β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov β„“) β†’ Pred(Algebra Ξ² ρᡇ) (b βŠ” ov(a βŠ” β„“ βŠ” ΞΉ))
  P β„“ ΞΉ 𝒦 𝑩 = Ξ£[ I ∈ Type ΞΉ ] Ξ£[ π’œ ∈ (I β†’ Algebra Ξ± ρᡃ) ] (βˆ€ i β†’ π’œ i ∈ 𝒦) ∧ 𝑩 β‰… β¨… π’œ

module _ {Ξ± ρᡃ Ξ² ρᡇ : Level} where
  private
    a b : Level
    a = Ξ± βŠ” ρᡃ ; b = Ξ² βŠ” ρᡇ

  SP : βˆ€ β„“ ΞΉ β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov β„“) β†’ Pred(Algebra Ξ² ρᡇ) (b βŠ” ov(a βŠ” β„“ βŠ” ΞΉ))
  SP β„“ ΞΉ 𝒦 = S{Ξ±}{ρᡃ} (a βŠ” β„“ βŠ” ΞΉ) (P β„“ ΞΉ 𝒦)

  module _ {γ ρᢜ δ ρᡈ : Level} where

    private
      c d : Level
      c = Ξ³ βŠ” ρᢜ ; d = Ξ΄ βŠ” ρᡈ

    V : βˆ€ β„“ ΞΉ
      β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov β„“) β†’  Pred(Algebra Ξ΄ ρᡈ) (d βŠ” ov(a βŠ” b βŠ” c βŠ” β„“ βŠ” ΞΉ))
    V β„“ ΞΉ 𝒦 = H{Ξ³}{ρᢜ} (a βŠ” b βŠ” β„“ βŠ” ΞΉ) (S{Ξ²}{ρᡇ} (a βŠ” β„“ βŠ” ΞΉ) (P β„“ ΞΉ 𝒦))
```

Thus, if 𝒦 is a class of 𝑆-algebras, then the *variety generated by* 𝒦 is denoted by
`V 𝒦` and defined to be the smallest class that contains 𝒦 and is closed under `H`,
`S`, and `P`.

#### A common-case level specialization of `V`

The operator `V`{.AgdaFunction} carries *eight* independent universe levels.
The input class lives at `(Ξ±, ρᡃ)` and the output algebra at `(Ξ΄, ρᡈ)`, but the
intermediate pairs `(Ξ², ρᡇ)` and `(Ξ³, ρᢜ)` are the levels of the algebras threaded
through the `H ∘ S ∘ P` composition: they are determined by neither the input nor the
output, so they stay free metavariables whenever `V`{.AgdaFunction} is applied without
a goal that already pins them.  That generality is essential for the HSP theorem, but
is unnecessary friction for the everyday request "the variety generated by a fixed algebra".

`Vβ€²`{.AgdaFunction} is the specialization of `V`{.AgdaFunction} to the overwhelmingly
common case in which the generated variety is considered at the *same* levels as the
class that generates it.  It collapses all four algebra positions to the input levels
`(Ξ±, ρᡃ)` β€” exactly the pinning `is-variety`{.AgdaFunction} already performs above
(`Ξ² = Ξ³ = Ξ΄ = Ξ±` and `ρᡇ = ρᢜ = ρᡈ = ρᡃ`), under which the output level
`d βŠ” ov(a βŠ” b βŠ” c βŠ” β„“ βŠ” ΞΉ)` of `V`{.AgdaFunction} collapses to `a βŠ” ov(a βŠ” β„“ βŠ” ΞΉ)`.
This is a documented narrowing of the canonical operator, not a synonym:
`V`{.AgdaFunction} remains the level-polymorphic form, while `Vβ€²`{.AgdaFunction} is the
fixed-level entry point that downstream examples and tests should prefer.

```agda
module _ {Ξ± ρᡃ : Level} where
  private
    a : Level
    a = Ξ± βŠ” ρᡃ

  Vβ€² : βˆ€ β„“ ΞΉ β†’ Pred(Algebra Ξ± ρᡃ)(a βŠ” ov β„“) β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov(a βŠ” β„“ βŠ” ΞΉ))
  Vβ€² β„“ ΞΉ 𝒦 = V {Ξ±}{ρᡃ}{Ξ±}{ρᡃ}{Ξ±}{ρᡃ} β„“ ΞΉ 𝒦
```

With the closure operator V representing closure under HSP, we represent formally
what it means to be a variety of algebras as follows.

```agda
module _ {Ξ± ρᡃ β„“ ΞΉ : Level} where

  is-variety : Pred (Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“) β†’ Type (ov (Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ))
  is-variety 𝒱 = Vβ€² β„“ ΞΉ 𝒱 βŠ† 𝒱

  variety : Type (ov (Ξ± βŠ” ρᡃ βŠ” ov β„“ βŠ” ΞΉ))
  variety = Ξ£[ 𝒱 ∈ Pred (Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“) ] is-variety 𝒱
```

#### Closure properties of S

`S` is a closure operator.  The fact that `S` is expansive won't be needed, so we
omit the proof, but we will make use of monotonicity and idempotence of `S`.

```agda
module _ {Ξ± ρᡃ : Level} where

  private a = Ξ± βŠ” ρᡃ

  S-mono : βˆ€{β„“} β†’ {𝒦 𝒦' : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)}
    β†’ 𝒦 βŠ† 𝒦' β†’ S{Ξ² = Ξ±}{ρᡃ} β„“ 𝒦 βŠ† S β„“ 𝒦'
  S-mono kk {𝑩} (𝑨 , (kA , B≀A)) = 𝑨 , ((kk kA) , B≀A)
```


We say `S` is *idempotent* provided `S`{.AgdaFunction} (`S`{.AgdaFunction} `𝒦`{.AgdaBound}) `=`{.AgdaSymbol} `S`{.AgdaFunction} `𝒦`{.AgdaBound}.
Of course, this is proved by establishing two inclusions, but one of them is trivial, so only the other need be formalized, which we do as follows.


```agda
  S-idem :  βˆ€{Ξ² ρᡇ Ξ³ ρᢜ β„“} β†’ {𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)}
    β†’ S{Ξ² = Ξ³}{ρᢜ} (a βŠ” β„“) (S{Ξ² = Ξ²}{ρᡇ} β„“ 𝒦) βŠ† S{Ξ² = Ξ³}{ρᢜ} β„“ 𝒦
  S-idem (𝑨 , (𝑩 , sB , A≀B) , x≀A) = 𝑩 , (sB , ≀-trans x≀A A≀B)
```



#### Closure properties of P

`P` is a closure operator.  This is proved by checking that `P` is *monotone*, *expansive*, and *idempotent*. The meaning of these terms will be clear from the definitions of the types that follow.


```agda
  H-expa : βˆ€{β„“} β†’ {𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)} β†’ 𝒦 βŠ† H β„“ 𝒦
  H-expa {β„“} {𝒦}{𝑨} kA = 𝑨 , kA , IdHomImage

  S-expa : βˆ€{β„“} β†’ {𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)} β†’ 𝒦 βŠ† S β„“ 𝒦
  S-expa {β„“}{𝒦}{𝑨} kA = 𝑨 , (kA , ≀-reflexive)

  P-mono : βˆ€{β„“ ΞΉ} β†’ {𝒦 𝒦' : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)}
    β†’ 𝒦 βŠ† 𝒦' β†’ P{Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦 βŠ† P β„“ ΞΉ 𝒦'

  P-mono {β„“}{ΞΉ}{𝒦}{𝒦'} kk {𝑩} (I , π’œ , (kA , Bβ‰…β¨…A)) = I , (π’œ , ((Ξ» i β†’ kk (kA i)) , Bβ‰…β¨…A))

  open _β‰…_
  open IsHom

  P-expa : βˆ€{β„“ ΞΉ} β†’ {𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)} β†’ 𝒦 βŠ† P β„“ ΞΉ 𝒦
  P-expa {β„“}{ΞΉ}{𝒦}{𝑨} kA = ⊀ , (Ξ» x β†’ 𝑨) , ((Ξ» i β†’ kA) , Goal)
    where
    open Algebra 𝑨 using () renaming (Domain to A)
    open Algebra (β¨… (Ξ» _ β†’ 𝑨)) using () renaming (Domain to β¨…A)
    open Setoid A using ( refl )
    open Setoid ⨅A using () renaming ( refl to refl⨅ )

    toβ¨… : A ⟢ β¨…A
    (toβ¨… ⟨$⟩ x) = Ξ» _ β†’ x
    cong to⨅ xy = λ _ → xy
    toβ¨…IsHom : IsHom 𝑨 (β¨… (Ξ» _ β†’ 𝑨)) toβ¨…
    compatible to⨅IsHom =  refl⨅

    fromβ¨… : β¨…A ⟢ A
    (fromβ¨… ⟨$⟩ x) = x tt
    cong from⨅ xy = xy tt
    fromβ¨…IsHom : IsHom (β¨… (Ξ» _ β†’ 𝑨)) 𝑨 fromβ¨…
    compatible from⨅IsHom = refl

    Goal : 𝑨 β‰… β¨… (Ξ» x β†’ 𝑨)
    to Goal = to⨅ , to⨅IsHom
    from Goal = from⨅ , from⨅IsHom
    to∼from Goal = Ξ» _ _ β†’ refl
    from∼to Goal = Ξ» _ β†’ refl


  V-expa : βˆ€ β„“ ΞΉ β†’ {𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)} β†’ 𝒦 βŠ† V β„“ ΞΉ 𝒦
  V-expa β„“ ΞΉ {𝒦} {𝑨} x = H-expa {a βŠ” β„“ βŠ” ΞΉ} (S-expa {a βŠ” β„“ βŠ” ΞΉ} (P-expa {β„“}{ΞΉ} x) )
```


The expansiveness lemmas above are stated with `_βŠ†_`, i.e. `𝒦 βŠ† βŠ™ β„“ … 𝒦`, which
unfolds to `βˆ€ {𝑨} β†’ 𝑨 ∈ 𝒦 β†’ 𝑨 ∈ βŠ™ β„“ … 𝒦` with both the class `𝒦`{.AgdaBound} and the
element `𝑨`{.AgdaBound} implicit.  Recovering them from a single membership proof is a
higher-order unification problem (`_𝒦 _𝑨 β‰Ÿ (𝑨 ∈ 𝒦)`) that Agda cannot solve once the
class predicate reduces.  The variants below take the class `𝒦`{.AgdaBound}
*explicitly*, so a membership in a closure operator follows directly from a membership
in the class with nothing to infer.  The `_βŠ†_` forms above remain the abstract
statements; these are the ergonomic entry points (`V-expaβ€²`{.AgdaFunction} is the one
exercised by `Examples.Setoid.HSPCommutativeMonoid`{.AgdaModule}).

```agda
  H-expaβ€² : βˆ€ β„“ (𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)) {𝑨} β†’ 𝑨 ∈ 𝒦 β†’ 𝑨 ∈ H β„“ 𝒦
  H-expaβ€² β„“ 𝒦 = H-expa {β„“}{𝒦}

  S-expaβ€² : βˆ€ β„“ (𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)) {𝑨} β†’ 𝑨 ∈ 𝒦 β†’ 𝑨 ∈ S β„“ 𝒦
  S-expaβ€² β„“ 𝒦 = S-expa {β„“}{𝒦}

  P-expaβ€² : βˆ€ β„“ ΞΉ (𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)) {𝑨} β†’ 𝑨 ∈ 𝒦 β†’ 𝑨 ∈ P β„“ ΞΉ 𝒦
  P-expaβ€² β„“ ΞΉ 𝒦 = P-expa {β„“}{ΞΉ}{𝒦}

  V-expaβ€² : βˆ€ β„“ ΞΉ (𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)) {𝑨} β†’ 𝑨 ∈ 𝒦 β†’ 𝑨 ∈ V β„“ ΞΉ 𝒦
  V-expaβ€² β„“ ΞΉ 𝒦 = V-expa β„“ ΞΉ {𝒦}
```

We sometimes want to go back and forth between our two representations of subalgebras
of algebras in a class. The tools `subalgebra→S` and `S→subalgebra` are made for that
purpose.

```agda
module _
  {Ξ± ρᡃ Ξ² ρᡇ β„“ ΞΉ : Level}
  {𝒦 : Pred (Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)}
  {𝑨 : Algebra Ξ± ρᡃ}
  {𝑩 : Algebra Ξ² ρᡇ}
  where

  S-β‰… : 𝑨 ∈ S β„“ 𝒦 β†’ 𝑨 β‰… 𝑩 β†’ 𝑩 ∈ S{Ξ± βŠ” Ξ²}{ρᡃ βŠ” ρᡇ}(Ξ± βŠ” ρᡃ βŠ” β„“) (Level-closure β„“ 𝒦)
  S-β‰… (𝑨' , kA' , A≀A') Aβ‰…B = lA' , (lklA' , B≀lA')
    where
    lA' : Algebra (Ξ± βŠ” Ξ²) (ρᡃ βŠ” ρᡇ)
    lA' = Lift-Alg 𝑨' Ξ² ρᡇ
    lklA' : lA' ∈ Level-closure β„“ 𝒦
    lklA' = Lift-closed β„“ kA'
    subgoal : 𝑨 ≀ lA'
    subgoal = ≀-trans-β‰… A≀A' Lift-β‰…
    B≀lA' : 𝑩 ≀ lA'
    B≀lA' = β‰…-trans-≀ (β‰…-sym Aβ‰…B) subgoal

  V-β‰… : 𝑨 ∈ V β„“ ΞΉ 𝒦 β†’ 𝑨 β‰… 𝑩 β†’ 𝑩 ∈ V{Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦
  V-β‰… (𝑨' , spA' , AimgA') Aβ‰…B = 𝑨' , spA' , HomImage-β‰… AimgA' Aβ‰…B

module _
  {Ξ± ρᡃ β„“ : Level}
  (𝒦 : Pred(Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“))
  (𝑨 : Algebra (Ξ± βŠ” ρᡃ βŠ” β„“) (Ξ± βŠ” ρᡃ βŠ” β„“))
  where
  private ΞΉ = ov(Ξ± βŠ” ρᡃ βŠ” β„“)

  V-β‰…-lc : Lift-Alg 𝑨 ΞΉ ΞΉ ∈ V{Ξ² = ΞΉ}{ΞΉ} β„“ ΞΉ 𝒦 β†’ 𝑨 ∈ V{Ξ³ = ΞΉ}{ΞΉ} β„“ ΞΉ 𝒦
  V-β‰…-lc (𝑨' , spA' , lAimgA') = 𝑨' , (spA' , AimgA')
    where
    AimgA' : 𝑨 IsHomImageOf 𝑨'
    AimgA' = Lift-HomImage-lemma lAimgA'
```

The remaining theorems in this file are as yet unused, but may be useful later and/or
for reference.

```agda
module _ {Ξ± ρᡃ β„“ ΞΉ : Level}{𝒦 : Pred (Algebra Ξ± ρᡃ)(Ξ± βŠ” ρᡃ βŠ” ov β„“)} where
  -- For reference, some useful type levels:
  classP : Pred (Algebra Ξ± ρᡃ) (ov(Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ))
  classP = P{Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦

  classSP : Pred (Algebra Ξ± ρᡃ) (ov(Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ))
  classSP = S{Ξ² = Ξ±}{ρᡃ} (Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ) (P{Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦)

  classHSP : Pred (Algebra Ξ± ρᡃ) (ov(Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ))
  classHSP = H{Ξ² = Ξ±}{ρᡃ}(Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ) (S{Ξ² = Ξ±}{ρᡃ}(Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ) (P{Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦))

  classS : βˆ€{Ξ² ρᡇ} β†’ Pred (Algebra Ξ² ρᡇ) (Ξ² βŠ” ρᡇ βŠ” ov(Ξ± βŠ” ρᡃ βŠ” β„“))
  classS = S β„“ 𝒦
  classK : βˆ€{Ξ² ρᡇ} β†’ Pred (Algebra Ξ² ρᡇ) (Ξ² βŠ” ρᡇ βŠ” ov(Ξ± βŠ” ρᡃ βŠ” β„“))
  classK = Level-closure{Ξ±}{ρᡃ} β„“ 𝒦

module _ {Ξ± ρᡃ Ξ² ρᡇ Ξ³ ρᢜ β„“ : Level}{𝒦 : Pred (Algebra Ξ± ρᡃ)(Ξ± βŠ” ρᡃ βŠ” ov β„“)} where
  private a = Ξ± βŠ” ρᡃ ; b = Ξ² βŠ” ρᡇ ; c = Ξ³ βŠ” ρᢜ

  LevelClosure-S : Pred (Algebra (Ξ± βŠ” Ξ³) (ρᡃ βŠ” ρᢜ)) (c βŠ” ov(a βŠ” b βŠ” β„“))
  LevelClosure-S = Level-closure{Ξ²}{ρᡇ} (a βŠ” β„“) (S β„“ 𝒦)

  S-LevelClosure : Pred (Algebra (Ξ± βŠ” Ξ³) (ρᡃ βŠ” ρᢜ)) (ov(a βŠ” c βŠ” β„“))
  S-LevelClosure = S{Ξ± βŠ” Ξ³}{ρᡃ βŠ” ρᢜ}(a βŠ” β„“) (Level-closure β„“ 𝒦)

  S-Lift-lemma : LevelClosure-S βŠ† S-LevelClosure
  S-Lift-lemma {π‘ͺ} (𝑩 , (𝑨 , (kA , B≀A)) , Bβ‰…C) =
    Lift-Alg 𝑨 Ξ³ ρᢜ , (Lift-closed{Ξ² = Ξ³}{ρᢜ} β„“ kA) , C≀lA
    where
    B≀lA : 𝑩 ≀ Lift-Alg 𝑨 Ξ³ ρᢜ
    B≀lA = ≀-Lift B≀A
    C≀lA : π‘ͺ ≀ Lift-Alg 𝑨 Ξ³ ρᢜ
    C≀lA = β‰…-trans-≀ (β‰…-sym Bβ‰…C) B≀lA

module _ {Ξ± ρᡃ : Level} where

  P-Lift-closed :  βˆ€ β„“ ΞΉ β†’ {𝒦 : Pred (Algebra Ξ± ρᡃ)(Ξ± βŠ” ρᡃ βŠ” ov β„“)}{𝑨 : Algebra Ξ± ρᡃ}
    β†’ 𝑨 ∈ P{Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦
    β†’ {Ξ³ ρᢜ : Level} β†’ Lift-Alg 𝑨 Ξ³ ρᢜ ∈ P (Ξ± βŠ” ρᡃ βŠ” β„“) ΞΉ (Level-closure β„“ 𝒦)
  P-Lift-closed β„“ ΞΉ {𝒦}{𝑨} (I , π’œ , kA , Aβ‰…β¨…π’œ) {Ξ³}{ρᢜ} =
    I , (Ξ» x β†’ Lift-Alg (π’œ x) Ξ³ ρᢜ) , goal1 , goal2
      where
      goal1 : (i : I) β†’ Lift-Alg (π’œ i) Ξ³ ρᢜ ∈ Level-closure β„“ 𝒦
      goal1 i = Lift-closed β„“ (kA i)
      goal2 : Lift-Alg 𝑨 Ξ³ ρᢜ β‰… β¨… (Ξ» x β†’ Lift-Alg (π’œ x) Ξ³ ρᢜ)
      goal2 = β‰…-trans (β‰…-sym Lift-β‰…) (β‰…-trans Aβ‰…β¨…π’œ (⨅≅⨅ℓρ{β„“ = Ξ³}{ρ = ρᢜ}))
```