refactor: post-lemma-3.9 clean-ups

src/Mugen/Cat/Endomorphisms.agda

@@ -1,6 +1,6 @@
 open import Cat.Prelude
 
-module Mugen.Cat.Endomorphisms {o ℓ} (𝒞 : Precategory o ℓ) (X : 𝒞 .Precategory.Ob) where
+module Mugen.Cat.Endomorphisms {o ℓ} where
 
 --------------------------------------------------------------------------------
 -- The category of endomorphisms on an object.
@@ -10,5 +10,8 @@ module Mugen.Cat.Endomorphisms {o ℓ} (𝒞 : Precategory o ℓ) (X : 𝒞 .Pre
 
 open import Mugen.Cat.Indexed
 
-Endos = Indexed 𝒞 {I = ⊤} λ _ → X
-Endos-include = Indexed-include 𝒞 {I = ⊤} λ _ → X
+Endos : (𝒞 : Precategory o ℓ) (X : 𝒞 .Precategory.Ob) → Precategory lzero ℓ
+Endos 𝒞 X = Indexed {I = ⊤} 𝒞 λ _ → X
+
+Endos-include : {𝒞 : Precategory o ℓ} {X : 𝒞 .Precategory.Ob} → Functor (Endos 𝒞 X) 𝒞
+Endos-include = Indexed-include

src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda

@@ -39,7 +39,7 @@ import Mugen.Order.Reasoning as Reasoning
 -- Naturality is in a different file
 
 module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
-  {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ lsuc r)) where
+  {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc (o ⊔ r))) where
 
   --------------------------------------------------------------------------------
   -- Notation
@@ -84,11 +84,14 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
     SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (McBride H⟨Δ⁺⟩→)
     module SOrdᴹᴰ = Cat SOrdᴹᴰ
 
+    Fᴴ : Functor SOrd SOrdᴴ
+    Fᴴ = Free SOrd H
+
     Fᴴ₀ : Poset o r → Algebra SOrd H
-    Fᴴ₀ = Functor.F₀ (Free SOrd H)
+    Fᴴ₀ = Fᴴ .Functor.F₀
 
     Fᴴ₁ : {X Y : Poset o r} → Hom X Y → SOrdᴴ.Hom (Fᴴ₀ X) (Fᴴ₀ Y)
-    Fᴴ₁ = Functor.F₁ (Free SOrd H)
+    Fᴴ₁ = Fᴴ .Functor.F₁
 
     Endoᴴ⟨Δ⟩ : Type (o ⊔ r)
     Endoᴴ⟨Δ⟩ = Hom (H.M₀ Δ) (H.M₀ Δ)

src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda

@@ -41,7 +41,7 @@ import Mugen.Order.Reasoning as Reasoning
 -- This file covers the naturality
 
 module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality
-  {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ lsuc r)) where
+  {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc (o ⊔ r))) where
 
   open import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding H Δ Ψ
 
@@ -92,38 +92,28 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality
     SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (McBride H⟨Δ⁺⟩→)
     module SOrdᴹᴰ = Cat SOrdᴹᴰ
 
+    Uᴴ : Functor SOrdᴴ SOrd
+    Uᴴ = Forget SOrd H
+
+    Fᴴ : Functor SOrd SOrdᴴ
+    Fᴴ = Free SOrd H
+
     Fᴴ₀ : Poset o r → Algebra SOrd H
-    Fᴴ₀ = Functor.F₀ (Free SOrd H)
+    Fᴴ₀ = Fᴴ .Functor.F₀
 
     Fᴴ₁ : {X Y : Poset o r} → Hom X Y → SOrdᴴ.Hom (Fᴴ₀ X) (Fᴴ₀ Y)
-    Fᴴ₁ = Functor.F₁ (Free SOrd H)
+    Fᴴ₁ = Fᴴ .Functor.F₁
 
-  --------------------------------------------------------------------------------
-  -- NOTE: Forgetful Functors + Levels
-  --
-  -- To avoid dealing with an annoying level shifting functor, we bake in the
-  -- required lifts into Uᴴ instead.
-
-  Uᴴ : ∀ {X} → Functor (Endos SOrdᴴ X) SOrd↑
-  Uᴴ {X} .Functor.F₀ _ = Lift≤ _ _ (X .fst)
-  Uᴴ .Functor.F₁ σ .hom (lift α) = lift (σ # α)
-  Uᴴ .Functor.F₁ σ .pres-≤[]-equal (lift α≤β) =
-    let σα≤σβ , inj = σ .morphism .pres-≤[]-equal α≤β in
-    lift σα≤σβ , λ p → ap lift $ inj $ lift-inj p
-  Uᴴ .Functor.F-id = ext λ _ → refl
-  Uᴴ .Functor.F-∘ _ _ = ext λ _ → refl
-
-  Uᴹᴰ : ∀ {X} → Functor (Endos SOrdᴹᴰ X) SOrd↑
-  Uᴹᴰ {X} .Functor.F₀ _ = X .fst
-  Uᴹᴰ .Functor.F₁ σ = σ .morphism
-  Uᴹᴰ .Functor.F-id = refl
-  Uᴹᴰ .Functor.F-∘ _ _ = refl
+    Uᴹᴰ : Functor SOrdᴹᴰ SOrd↑
+    Uᴹᴰ = Forget SOrd↑ (McBride H⟨Δ⁺⟩→)
 
   --------------------------------------------------------------------------------
   -- Constructing the natural transformation ν
   -- Section 3.4, Lemma 3.8
 
-  ν : (pt : ∣ Ψ ∣) → Uᴴ => Uᴹᴰ F∘ T
+  ν : (pt : ∣ Ψ ∣)
+    →  liftᶠ-strict-orders F∘ Uᴴ F∘ Endos-include
+    => Uᴹᴰ F∘ Endos-include F∘ T
   ν pt = nt
     where
       ℓ̅ : ⌞ H.M₀ Δ ⌟ → Hom Δ⁺ (H.M₀ Δ⁺)
@@ -183,7 +173,8 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality
             H.η _ # ι₂ α                          ≡˘⟨ μ-η H (σ̅ σ) #ₚ _ ⟩
             H.μ _ # (H.M₁ (σ̅ σ) # (H.η _ # ι₂ α)) ∎
 
-      nt : Uᴴ => Uᴹᴰ F∘ T
+      nt : liftᶠ-strict-orders F∘ Uᴴ F∘ Endos-include
+        => Uᴹᴰ F∘ Endos-include F∘ T
       nt ._=>_.η _ .hom (lift ℓ) = pt , ν′ ℓ
       nt ._=>_.η _ .pres-≤[]-equal (lift ℓ≤ℓ′) =
         inc (biased refl (ν′-mono ℓ≤ℓ′)) , λ p → ap lift $ ν′-injective-on-related ℓ≤ℓ′ (ap snd p)

src/Mugen/Cat/HierarchyTheory/Universality/HeterogeneousEmbedding.agda → src/Mugen/Cat/HierarchyTheory/Universality/SubcategoryEmbedding.agda

@@ -12,33 +12,25 @@ import Cat.Reasoning as Cat
 
 open import Mugen.Prelude
 
-open import Mugen.Algebra.Displacement
-open import Mugen.Algebra.Displacement.Instances.Endomorphism
-
 open import Mugen.Cat.Endomorphisms
 open import Mugen.Cat.Indexed
 open import Mugen.Cat.StrictOrders
 open import Mugen.Cat.Monad
 open import Mugen.Cat.HierarchyTheory
-open import Mugen.Cat.HierarchyTheory.McBride
 
 open import Mugen.Order.StrictOrder
 open import Mugen.Order.Instances.Copower
-open import Mugen.Order.Instances.Lift
 open import Mugen.Order.Instances.Singleton
 
 import Mugen.Order.Reasoning as Reasoning
 
 --------------------------------------------------------------------------------
 -- The Universal Embedding Theorem
 -- Section 3.4, Lemma 3.9
---
--- Naturality is in a different file
 
-module Mugen.Cat.HierarchyTheory.Universality.HeterogeneousEmbedding
-  {o} (H : Hierarchy-theory o o) {I : Type o}
-  ⦃ Discrete-I : Discrete I ⦄
-  (Δ₋ : ⌞ I ⌟ → Poset o o) where
+module Mugen.Cat.HierarchyTheory.Universality.SubcategoryEmbedding {o o' r}
+  (H : Hierarchy-theory (o ⊔ o') (r ⊔ o')) {I : Type o'} ⦃ Discrete-I : Discrete I ⦄
+  (Δ₋ : ⌞ I ⌟ → Poset (o ⊔ o') (r ⊔ o')) where
 
   --------------------------------------------------------------------------------
   -- Notation
@@ -48,34 +40,32 @@ module Mugen.Cat.HierarchyTheory.Universality.HeterogeneousEmbedding
   private
     open Strictly-monotone
     open Algebra-hom
-    open Cat (Strict-orders o o)
+    open Cat (Strict-orders (o ⊔ o') (r ⊔ o'))
     module Δ₋ i = Poset (Δ₋ i)
     module H = Monad H
 
-    ⌞Δ₋⌟ : I → Type o
+    ⌞Δ₋⌟ : I → Type (o ⊔ o')
     ⌞Δ₋⌟ i = ⌞ Δ₋ i ⌟
 
     abstract instance 
       H-Level-I : H-Level I 2
       H-Level-I = hlevel-instance $ Discrete→is-set Discrete-I
 
-    Δ' : Poset o o
-    Δ' = Disjoint (el! I) Δ₋
-    module Δ' = Poset Δ'
-
-    Δ : Poset o o
-    Δ = Copower (el! Nat) Δ'
-    module Δ = Poset Δ
+  -- Δ is made public for proving the main theorem
+  Δ : Poset (o ⊔ o') (r ⊔ o')
+  Δ = Copower (el! Nat) (Disjoint (el! I) Δ₋)
+  module Δ = Poset Δ
 
-    H⟨Δ⟩ : Poset o o
+  private
+    H⟨Δ⟩ : Poset (o ⊔ o') (r ⊔ o')
     H⟨Δ⟩ = H.M₀ Δ
     module H⟨Δ⟩ = Reasoning H⟨Δ⟩
 
-    SOrd : Precategory (lsuc o) o
-    SOrd = Strict-orders o o
+    SOrd : Precategory (lsuc (o ⊔ r ⊔ o')) (o ⊔ r ⊔ o')
+    SOrd = Strict-orders (o ⊔ o') (r ⊔ o')
     module SOrd = Cat SOrd
 
-    SOrdᴴ : Precategory (lsuc o) (lsuc o)
+    SOrdᴴ : Precategory (lsuc (o ⊔ r ⊔ o')) (lsuc (o ⊔ r ⊔ o'))
     SOrdᴴ = Eilenberg-Moore SOrd H
     module SOrdᴴ = Cat SOrdᴴ
 
@@ -85,10 +75,10 @@ module Mugen.Cat.HierarchyTheory.Universality.HeterogeneousEmbedding
     Fᴴ : Functor SOrd SOrdᴴ
     Fᴴ = Free SOrd H
 
-    Fᴴ₀ : Poset o o → Algebra SOrd H
+    Fᴴ₀ : Poset (o ⊔ o') (r ⊔ o') → Algebra SOrd H
     Fᴴ₀ = Fᴴ .Functor.F₀
 
-    Fᴴ₁ : {X Y : Poset o o} → Hom X Y → SOrdᴴ.Hom (Fᴴ₀ X) (Fᴴ₀ Y)
+    Fᴴ₁ : {X Y : Poset (o ⊔ o') (r ⊔ o')} → Hom X Y → SOrdᴴ.Hom (Fᴴ₀ X) (Fᴴ₀ Y)
     Fᴴ₁ = Fᴴ .Functor.F₁
 
     FᴴΔ₋ : I → Algebra SOrd H
@@ -128,19 +118,18 @@ module Mugen.Cat.HierarchyTheory.Universality.HeterogeneousEmbedding
   ... | no _      | n     | yes _ = H⟨Δ⟩.≤[]-map (ap (ι n k)) $ (H.η Δ ∘ ι-hom (suc n) k) .pres-≤[]-equal α≤β
   ... | no _      | n     | no _  = H.η Δ .pres-≤[]-equal (reflᵢ , reflᵢ , α≤β)
 
-  -- all raw β rules
+  -- Raw β rules of σ̅ σ matching its five cases
   module _ where
     abstract
       σ̅-ι-k0j-ext : ∀ {i j k : I} (σ : SOrdᴴ.Hom (FᴴΔ₋ i) (FᴴΔ₋ j))
         → (p : k ≡ᵢ i)
         → (α : ⌞ Δ₋ k ⌟)
         → σ̅ σ # ι 0 k α ≡ H.M₁ (ι-hom 0 j) # (σ # (H.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ p α))
       σ̅-ι-k0j-ext {i = i} {j} {k} σ p α with k ≡ᵢ? i
-      ... | no  k≠ᵢi = absurd (k≠ᵢi p)
-      ... | yes k=ᵢi =
-        H.M₁ (ι-hom 0 j) # (σ # (H.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ k=ᵢi α))
-         ≡⟨ ap# (H.M₁ (ι-hom 0 j) ∘ σ .morphism ∘ H.η (Δ₋ i))
-              (λ l → substᵢ ⌞Δ₋⌟ (hlevel 1 k=ᵢi p l) α) ⟩
+      ... | no  k≠ᵢi  = absurd (k≠ᵢi p)
+      ... | yes reflᵢ =
+        H.M₁ (ι-hom 0 j) # (σ # (H.η (Δ₋ i) # α))
+         ≡⟨ ap# (H.M₁ (ι-hom 0 j) ∘ σ .morphism ∘ H.η (Δ₋ i)) $ substᵢ-filler-set ⌞Δ₋⌟ (hlevel 2) p α ⟩
         H.M₁ (ι-hom 0 j) # (σ # (H.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ p α))
           ∎
 
@@ -184,7 +173,7 @@ module Mugen.Cat.HierarchyTheory.Universality.HeterogeneousEmbedding
       ... | no  _    | yes k=ᵢj = absurd (k≠ᵢj k=ᵢj)
       ... | no  _    | no  _    = refl
 
-  -- all wrapped β rules
+  -- Wrapped β rules of H.M₁ (σ̅ σ)
   module _ where
     abstract
       H-σ̅-ι-k0j : ∀ {k j : I} (σ : SOrdᴴ.Hom (FᴴΔ₋ k) (FᴴΔ₋ j)) (α : ⌞ H.M₀ (Δ₋ k) ⌟)
@@ -273,6 +262,7 @@ module Mugen.Cat.HierarchyTheory.Universality.HeterogeneousEmbedding
       ≡ (H.μ Δ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ) # ι n l α
     σ̅-∘ {i = i} {j} {k} σ δ n l α with l ≡ᵢ? i | n | l ≡ᵢ? j | l ≡ᵢ? k
     ... | yes reflᵢ | 0     | _         | _         = sym $ H-σ̅-ι-k0j σ (δ # (H.η (Δ₋ i) # α))
+    -- Note: the following eight cases correspond to the table in the paper with eight rows.
     ... | yes reflᵢ | suc n | yes reflᵢ | yes reflᵢ = sym $ H-σ̅-η-ι-k1k n σ α
     ... | yes reflᵢ | suc n | yes reflᵢ | no  l≠k   = sym $ H-σ̅-η-ι-k1j n σ l≠k α
     ... | yes reflᵢ | suc n | no  l≠j   | yes reflᵢ = sym $ H-σ̅-η-ι-ik n σ l≠j α
@@ -303,7 +293,7 @@ module Mugen.Cat.HierarchyTheory.Universality.HeterogeneousEmbedding
   -- Constructing the natural transformation ν
   -- Section 3.4, Lemma 3.8
 
-  ν : Uᴴ F∘ Indexed-include SOrdᴴ FᴴΔ₋ => Uᴴ F∘ Endos-include SOrdᴴ (Fᴴ₀ Δ) F∘ T
+  ν : Uᴴ F∘ Indexed-include => Uᴴ F∘ Endos-include F∘ T
   ν ._=>_.η i = H.M₁ (ι-hom 0 i)
   ν ._=>_.is-natural i j σ = sym $ ext $ H-σ̅-ι-k0j σ
 

src/Mugen/Cat/Indexed.agda

@@ -1,23 +1,24 @@
 open import Cat.Prelude
 
-module Mugen.Cat.Indexed {o o' ℓ} (𝒞 : Precategory o ℓ) {I : Type o'} (F : I → 𝒞 .Precategory.Ob) where
+module Mugen.Cat.Indexed {o o' ℓ} {I : Type o'} where
 
 import Cat.Reasoning as Cat
 
-open Cat 𝒞
+Indexed : (𝒞 : Precategory o ℓ) (F : I → 𝒞 .Precategory.Ob) → Precategory o' ℓ
+Indexed 𝒞 F = C where
+  open Cat 𝒞
+  C : Precategory o' ℓ
+  C .Precategory.Ob          = I
+  C .Precategory.Hom i j     = Hom (F i) (F j)
+  C .Precategory.Hom-set _ _ = Hom-set _ _
+  C .Precategory.id          = id
+  C .Precategory._∘_         = _∘_
+  C .Precategory.idr         = idr
+  C .Precategory.idl         = idl
+  C .Precategory.assoc       = assoc
 
-Indexed : Precategory o' ℓ
-Indexed .Precategory.Ob          = I
-Indexed .Precategory.Hom i j     = Hom (F i) (F j)
-Indexed .Precategory.Hom-set _ _ = Hom-set _ _
-Indexed .Precategory.id          = id
-Indexed .Precategory._∘_         = _∘_
-Indexed .Precategory.idr         = idr
-Indexed .Precategory.idl         = idl
-Indexed .Precategory.assoc       = assoc
-
-Indexed-include : Functor Indexed 𝒞
-Indexed-include .Functor.F₀ = F
+Indexed-include : ∀ {𝒞} {F : I → 𝒞 .Precategory.Ob} → Functor (Indexed 𝒞 F) 𝒞
+Indexed-include {F = F} .Functor.F₀ = F
 Indexed-include .Functor.F₁ σ = σ
 Indexed-include .Functor.F-id = refl
 Indexed-include .Functor.F-∘ _ _ = refl

src/Mugen/Cat/StrictOrders.agda

@@ -2,10 +2,7 @@ module Mugen.Cat.StrictOrders where
 
 open import Mugen.Prelude
 open import Mugen.Order.StrictOrder
-
-private variable
-  o r : Level
-  X Y Z : Poset o r
+open import Mugen.Order.Instances.Lift
 
 --------------------------------------------------------------------------------
 -- The Category of Strict Orders
@@ -21,3 +18,9 @@ Strict-orders o r ._∘_ = strictly-monotone-∘
 Strict-orders o r .idr f = ext λ _ → refl
 Strict-orders o r .idl f = ext λ _ → refl
 Strict-orders o r .assoc f g h = ext λ _ → refl
+
+liftᶠ-strict-orders : ∀ {o r o' r' : Level} → Functor (Strict-orders o r) (Strict-orders (o ⊔ o') (r ⊔ r'))
+liftᶠ-strict-orders {o' = o'} {r'} .Functor.F₀ X    = Liftᵖ o' r' X
+liftᶠ-strict-orders .Functor.F₁ f    = strictly-monotone-∘ (strictly-monotone-∘ lift-strictly-monotone f) lower-strictly-monotone
+liftᶠ-strict-orders .Functor.F-id    = ext λ _ → refl
+liftᶠ-strict-orders .Functor.F-∘ _ _ = ext λ _ → refl

src/Mugen/Everything.agda

@@ -25,7 +25,7 @@ import Mugen.Cat.HierarchyTheory
 import Mugen.Cat.HierarchyTheory.McBride
 import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
 import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality
-import Mugen.Cat.HierarchyTheory.Universality.HeterogeneousEmbedding
+import Mugen.Cat.HierarchyTheory.Universality.SubcategoryEmbedding
 import Mugen.Cat.Indexed
 import Mugen.Cat.Monad
 import Mugen.Cat.StrictOrders

src/Mugen/Order/Instances/Lift.agda

@@ -1,18 +1,33 @@
+open import Order.Base
+
 open import Mugen.Prelude
+open import Mugen.Order.StrictOrder
+import Mugen.Order.Reasoning as Reasoning
 
 module Mugen.Order.Instances.Lift where
 
-private variable
-  o r : Level
+Liftᵖ : ∀ {o r} o′ r′ → Poset o r → Poset (o ⊔ o′) (r ⊔ r′)
+Liftᵖ o' r' X .Poset.Ob      = Lift o' ⌞ X ⌟
+Liftᵖ o' r' X .Poset._≤_ x y = Lift r' $ (X .Poset._≤_) (Lift.lower x) (Lift.lower y)
+Liftᵖ o' r' X .Poset.≤-thin  = Lift-is-hlevel 1 $ X .Poset.≤-thin
+Liftᵖ o' r' X .Poset.≤-refl  = lift $ X .Poset.≤-refl
+Liftᵖ o' r' X .Poset.≤-trans (lift p) (lift q)   = lift (X .Poset.≤-trans p q)
+Liftᵖ o' r' X .Poset.≤-antisym (lift p) (lift q) = ap lift (X .Poset.≤-antisym p q)
+
+lift-strictly-monotone
+  : ∀ {bo br o r} {X : Poset o r}
+  → Strictly-monotone X (Liftᵖ bo br X)
+lift-strictly-monotone = F where
+  open Strictly-monotone
+  F : Strictly-monotone _ _
+  F .hom              = lift
+  F .pres-≤[]-equal α = lift α , ap Lift.lower
 
-Lift≤
-  : ∀ {o r}
-  → (o′ r′ : Level)
-  → Poset o r
-  → Poset (o ⊔ o′) (r ⊔ r′)
-Lift≤ o' r' X .Poset.Ob = Lift o' ⌞ X ⌟
-Lift≤ o' r' X .Poset._≤_ x y = Lift r' $ (X .Poset._≤_) (Lift.lower x) (Lift.lower y)
-Lift≤ o' r' X .Poset.≤-thin = Lift-is-hlevel 1 $ X .Poset.≤-thin
-Lift≤ o' r' X .Poset.≤-refl = lift $ X .Poset.≤-refl
-Lift≤ o' r' X .Poset.≤-trans (lift p) (lift q) = lift (X .Poset.≤-trans p q)
-Lift≤ o' r' X .Poset.≤-antisym (lift p) (lift q) = ap lift (X .Poset.≤-antisym p q)
+lower-strictly-monotone
+  : ∀ {bo br o r} {X : Poset o r}
+  → Strictly-monotone (Liftᵖ bo br X) X
+lower-strictly-monotone = F where
+  open Strictly-monotone
+  F : Strictly-monotone _ _
+  F .hom                     = Lift.lower
+  F .pres-≤[]-equal (lift α) = α , ap lift

src/Mugen/Order/Reasoning.agda

@@ -30,10 +30,10 @@ module Mugen.Order.Reasoning {o r} (A : Poset o r) where
     ≤-antisym'-r : ∀ {x y z} → x ≤ y → y ≤ z → x ≡ z → y ≡ z
     ≤-antisym'-r {y = y} x≤y y≤z x=z = ≤-antisym y≤z $ subst (_≤ y) x=z x≤y
 
-  RelativeInequality : ∀ {r'} (x y : Ob) (K : Type r') → Type (o ⊔ r ⊔ r')
-  RelativeInequality x y K = (x ≤ y) × (x ≡ y → K)
+  ParametrizedInequality : ∀ {r'} (x y : Ob) (K : Type r') → Type (o ⊔ r ⊔ r')
+  ParametrizedInequality x y K = (x ≤ y) × (x ≡ y → K)
 
-  syntax RelativeInequality x y K = x ≤[ K ] y
+  syntax ParametrizedInequality x y K = x ≤[ K ] y
 
   abstract
     ≤[]-is-hlevel : ∀ {x y : Ob} {K : Type r'}