From a4e2c07c0f6470351ffe5e74dbf4ffff1595a931 Mon Sep 17 00:00:00 2001
From: Rahul <rahul29112002@gmail.com>
Date: Fri, 15 Sep 2023 22:15:06 +0530
Subject: [PATCH 1/5] Update Powerset module

---
 Cubical/Foundations/Powerset.agda | 94 +++++++++++++++++++++++++++++++
 Cubical/Functions/Embedding.agda  |  2 +-
 2 files changed, 95 insertions(+), 1 deletion(-)

diff --git a/Cubical/Foundations/Powerset.agda b/Cubical/Foundations/Powerset.agda
index 043a0dfed8..50cd39f517 100644
--- a/Cubical/Foundations/Powerset.agda
+++ b/Cubical/Foundations/Powerset.agda
@@ -18,6 +18,12 @@ open import Cubical.Foundations.Function
 open import Cubical.Foundations.Univalence using (hPropExt)
 
 open import Cubical.Data.Sigma
+open import Cubical.Data.Unit
+open import Cubical.Data.Empty
+
+open import Cubical.HITs.PropositionalTruncation.Base
+
+open import Cubical.Relation.Nullary using (¬_)
 
 private
   variable
@@ -41,6 +47,26 @@ A ⊆ B = ∀ x → x ∈ A → x ∈ B
 ∈-isProp : (A : ℙ X) (x : X) → isProp (x ∈ A)
 ∈-isProp A = snd ∘ A
 
+infix 5 _∈ₚ_
+
+-- x ∈ₚ A differs from x ∈ A
+-- in the sense that it produces an hProp
+_∈ₚ_ : {X : Type ℓ} → X → ℙ X → hProp ℓ
+x ∈ₚ A = x ∈ A , ∈-isProp A x
+
+-- "not in" relations
+
+infix 5 _∉_
+_∉_ : {X : Type ℓ} → X → ℙ X → Type ℓ
+x ∉ A = ¬ x ∈ A
+
+∉-isProp : (A : ℙ X) (x : X) → isProp (x ∉ A)
+∉-isProp A x = isPropΠ λ _ → isProp⊥
+
+infix 5 _∉ₚ_
+_∉ₚ_ : {X : Type ℓ} → X → ℙ X → hProp ℓ
+x ∉ₚ A = x ∉ A , ∉-isProp A x
+
 ⊆-isProp : (A B : ℙ X) → isProp (A ⊆ B)
 ⊆-isProp A B = isPropΠ2 (λ x _ → ∈-isProp B x)
 
@@ -63,3 +89,71 @@ subst-∈ A = subst (_∈ A)
                                             (⊆-refl-consequence A B)
                                             (λ _ → isSetℙ A B _ _)
                                             (λ _ → isPropΣ (⊆-isProp A B) (λ _ → ⊆-isProp B A) _ _))
+
+-- Binary Intersections
+infix 6 _∩_
+
+-- Unfortunately, simply importing Cubical.Data.Sum, Cubical.HITs.PropositionalTruncation and
+-- Cubical.Functions.Logic indirectly imports Cubical.Functions.Embeddings which
+-- creates a circular dependency
+-- For now, we will have to repeat a few definitions
+-- We mark all these as private to ensure that no name clashes take place
+
+_∩_ : ℙ X → ℙ X → ℙ X
+A ∩ B = λ x → A x ⊓ B x where
+              -- Repeated from Cubical.Functions.Logic
+              _⊓_ : hProp ℓ → hProp ℓ → hProp ℓ
+              a ⊓ b = ⟨ a ⟩ × ⟨ b ⟩ , isOfHLevelΣ 1 (a .snd) λ _ → b .snd 
+
+-- Repeated from Cubical.Data.Sum
+private data _⊎_ (A B : Type ℓ) : Type ℓ where
+  inl : A → A ⊎ B
+  inr : B → A ⊎ B
+
+-- Repeated from Cubical.Functions.Logic
+∥_∥ₚ : (X : Type ℓ) → hProp ℓ
+∥ X ∥ₚ = ∥ X ∥₁ , squash₁
+
+-- Binary Unions
+infix 6 _∪_
+
+_∪_ : ℙ X → ℙ X → ℙ X
+A ∪ B = λ x → A x ⊔ B x where
+              -- Repeated from Cubical.Functions.Logic
+              _⊔_ : hProp ℓ → hProp ℓ → hProp ℓ
+              a ⊔ b = ∥ ⟨ a ⟩ ⊎  ⟨ b ⟩ ∥ₚ 
+
+-- When defining union and intersection over families
+-- we define an implicit argument X instead of using the module private metavariable
+-- since Agda is unable to infer that ℓ-max ℓ X.ℓ = ℓ
+
+-- Indexed Unions
+⋃ : {X I : Type ℓ} → (I → ℙ X) → ℙ X
+⋃ {I = I} family = λ x → ∥ Σ[ i ∈ I ] (x ∈ family i) ∥ₚ 
+
+-- Indexed Intersections
+⋂ : {X I : Type ℓ} → (I → ℙ X) → ℙ X
+⋂ {I = I} family = λ x → ∥ (∀ i → (x ∈ family i)) ∥ₚ 
+
+-- Empty subset
+∅ : ℙ X
+∅ x = ⊥* , isProp⊥*
+
+-- Total subset
+𝕋 : ℙ X
+𝕋 = λ x → ∥ Lift Unit ∥ₚ 
+
+infixl 7 ～_
+
+～_ : ℙ X → ℙ X
+～ A = λ x → x ∉ₚ A
+
+-- The type of inhabited subsets
+-- Inspired by the same definition in [martinescardo/TypeTopology](https://www.cs.bham.ac.uk/~mhe/TypeTopology/UF.Powerset.html#3251)
+
+-- A subset A is inhabited if there merely exists an x such that x ∈ A
+isInhabited : {X : Type ℓ} → ℙ X → hProp ℓ
+isInhabited {X = X} A = ∥ (Σ[ x ∈ X ] x ∈ A) ∥ₚ
+
+ℙ⁺ : Type ℓ → Type (ℓ-suc ℓ)
+ℙ⁺ X = Σ[ A ∈ ℙ X ] ⟨ isInhabited A ⟩
diff --git a/Cubical/Functions/Embedding.agda b/Cubical/Functions/Embedding.agda
index bf5c11648d..8068eb2043 100644
--- a/Cubical/Functions/Embedding.agda
+++ b/Cubical/Functions/Embedding.agda
@@ -9,7 +9,7 @@ open import Cubical.Foundations.Equiv.HalfAdjoint
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Path
-open import Cubical.Foundations.Powerset
+open import Cubical.Foundations.Powerset using (ℙ; _∈_; ∈-isProp)
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Transport
 open import Cubical.Foundations.Univalence using (ua; univalence; pathToEquiv)

From 17a44f2e13c9b99bd24476fce4ba52454e88a83a Mon Sep 17 00:00:00 2001
From: Rahul <rahul29112002@gmail.com>
Date: Fri, 15 Sep 2023 22:19:01 +0530
Subject: [PATCH 2/5] Make repeated definition private

---
 Cubical/Foundations/Powerset.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cubical/Foundations/Powerset.agda b/Cubical/Foundations/Powerset.agda
index 50cd39f517..977cad23d0 100644
--- a/Cubical/Foundations/Powerset.agda
+++ b/Cubical/Foundations/Powerset.agda
@@ -111,7 +111,7 @@ private data _⊎_ (A B : Type ℓ) : Type ℓ where
   inr : B → A ⊎ B
 
 -- Repeated from Cubical.Functions.Logic
-∥_∥ₚ : (X : Type ℓ) → hProp ℓ
+private ∥_∥ₚ : (X : Type ℓ) → hProp ℓ
 ∥ X ∥ₚ = ∥ X ∥₁ , squash₁
 
 -- Binary Unions

From e2f60ee8867b95431f27ff5d46f09f2cb5c7091f Mon Sep 17 00:00:00 2001
From: Rahul <rahul29112002@gmail.com>
Date: Fri, 15 Sep 2023 22:19:46 +0530
Subject: [PATCH 3/5] Remove unnecessary using

---
 Cubical/Functions/Embedding.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cubical/Functions/Embedding.agda b/Cubical/Functions/Embedding.agda
index 8068eb2043..bf5c11648d 100644
--- a/Cubical/Functions/Embedding.agda
+++ b/Cubical/Functions/Embedding.agda
@@ -9,7 +9,7 @@ open import Cubical.Foundations.Equiv.HalfAdjoint
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Path
-open import Cubical.Foundations.Powerset using (ℙ; _∈_; ∈-isProp)
+open import Cubical.Foundations.Powerset
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Transport
 open import Cubical.Foundations.Univalence using (ua; univalence; pathToEquiv)

From de0a479dde1cfa02fdefec399fba74740df4873a Mon Sep 17 00:00:00 2001
From: Rahul Chhabra <rahul29112002@gmail.com>
Date: Sat, 23 Mar 2024 14:44:25 +0530
Subject: [PATCH 4/5] Sync with agda/cubical

---
 Cubical/Foundations/Powerset.agda | 94 -------------------------------
 1 file changed, 94 deletions(-)

diff --git a/Cubical/Foundations/Powerset.agda b/Cubical/Foundations/Powerset.agda
index 977cad23d0..043a0dfed8 100644
--- a/Cubical/Foundations/Powerset.agda
+++ b/Cubical/Foundations/Powerset.agda
@@ -18,12 +18,6 @@ open import Cubical.Foundations.Function
 open import Cubical.Foundations.Univalence using (hPropExt)
 
 open import Cubical.Data.Sigma
-open import Cubical.Data.Unit
-open import Cubical.Data.Empty
-
-open import Cubical.HITs.PropositionalTruncation.Base
-
-open import Cubical.Relation.Nullary using (¬_)
 
 private
   variable
@@ -47,26 +41,6 @@ A ⊆ B = ∀ x → x ∈ A → x ∈ B
 ∈-isProp : (A : ℙ X) (x : X) → isProp (x ∈ A)
 ∈-isProp A = snd ∘ A
 
-infix 5 _∈ₚ_
-
--- x ∈ₚ A differs from x ∈ A
--- in the sense that it produces an hProp
-_∈ₚ_ : {X : Type ℓ} → X → ℙ X → hProp ℓ
-x ∈ₚ A = x ∈ A , ∈-isProp A x
-
--- "not in" relations
-
-infix 5 _∉_
-_∉_ : {X : Type ℓ} → X → ℙ X → Type ℓ
-x ∉ A = ¬ x ∈ A
-
-∉-isProp : (A : ℙ X) (x : X) → isProp (x ∉ A)
-∉-isProp A x = isPropΠ λ _ → isProp⊥
-
-infix 5 _∉ₚ_
-_∉ₚ_ : {X : Type ℓ} → X → ℙ X → hProp ℓ
-x ∉ₚ A = x ∉ A , ∉-isProp A x
-
 ⊆-isProp : (A B : ℙ X) → isProp (A ⊆ B)
 ⊆-isProp A B = isPropΠ2 (λ x _ → ∈-isProp B x)
 
@@ -89,71 +63,3 @@ subst-∈ A = subst (_∈ A)
                                             (⊆-refl-consequence A B)
                                             (λ _ → isSetℙ A B _ _)
                                             (λ _ → isPropΣ (⊆-isProp A B) (λ _ → ⊆-isProp B A) _ _))
-
--- Binary Intersections
-infix 6 _∩_
-
--- Unfortunately, simply importing Cubical.Data.Sum, Cubical.HITs.PropositionalTruncation and
--- Cubical.Functions.Logic indirectly imports Cubical.Functions.Embeddings which
--- creates a circular dependency
--- For now, we will have to repeat a few definitions
--- We mark all these as private to ensure that no name clashes take place
-
-_∩_ : ℙ X → ℙ X → ℙ X
-A ∩ B = λ x → A x ⊓ B x where
-              -- Repeated from Cubical.Functions.Logic
-              _⊓_ : hProp ℓ → hProp ℓ → hProp ℓ
-              a ⊓ b = ⟨ a ⟩ × ⟨ b ⟩ , isOfHLevelΣ 1 (a .snd) λ _ → b .snd 
-
--- Repeated from Cubical.Data.Sum
-private data _⊎_ (A B : Type ℓ) : Type ℓ where
-  inl : A → A ⊎ B
-  inr : B → A ⊎ B
-
--- Repeated from Cubical.Functions.Logic
-private ∥_∥ₚ : (X : Type ℓ) → hProp ℓ
-∥ X ∥ₚ = ∥ X ∥₁ , squash₁
-
--- Binary Unions
-infix 6 _∪_
-
-_∪_ : ℙ X → ℙ X → ℙ X
-A ∪ B = λ x → A x ⊔ B x where
-              -- Repeated from Cubical.Functions.Logic
-              _⊔_ : hProp ℓ → hProp ℓ → hProp ℓ
-              a ⊔ b = ∥ ⟨ a ⟩ ⊎  ⟨ b ⟩ ∥ₚ 
-
--- When defining union and intersection over families
--- we define an implicit argument X instead of using the module private metavariable
--- since Agda is unable to infer that ℓ-max ℓ X.ℓ = ℓ
-
--- Indexed Unions
-⋃ : {X I : Type ℓ} → (I → ℙ X) → ℙ X
-⋃ {I = I} family = λ x → ∥ Σ[ i ∈ I ] (x ∈ family i) ∥ₚ 
-
--- Indexed Intersections
-⋂ : {X I : Type ℓ} → (I → ℙ X) → ℙ X
-⋂ {I = I} family = λ x → ∥ (∀ i → (x ∈ family i)) ∥ₚ 
-
--- Empty subset
-∅ : ℙ X
-∅ x = ⊥* , isProp⊥*
-
--- Total subset
-𝕋 : ℙ X
-𝕋 = λ x → ∥ Lift Unit ∥ₚ 
-
-infixl 7 ～_
-
-～_ : ℙ X → ℙ X
-～ A = λ x → x ∉ₚ A
-
--- The type of inhabited subsets
--- Inspired by the same definition in [martinescardo/TypeTopology](https://www.cs.bham.ac.uk/~mhe/TypeTopology/UF.Powerset.html#3251)
-
--- A subset A is inhabited if there merely exists an x such that x ∈ A
-isInhabited : {X : Type ℓ} → ℙ X → hProp ℓ
-isInhabited {X = X} A = ∥ (Σ[ x ∈ X ] x ∈ A) ∥ₚ
-
-ℙ⁺ : Type ℓ → Type (ℓ-suc ℓ)
-ℙ⁺ X = Σ[ A ∈ ℙ X ] ⟨ isInhabited A ⟩

From d4ca6faa0a5214e21303d14a75f039cc0643681b Mon Sep 17 00:00:00 2001
From: Rahul Chhabra <rahul29112002@gmail.com>
Date: Sat, 23 Mar 2024 19:28:28 +0530
Subject: [PATCH 5/5] Add preorder structure on the category of subobjects

---
 .../Categories/Constructions/Slice/Base.agda  | 16 ++++++
 .../Categories/Constructions/SubObject.agda   | 56 +++++++++++++++++++
 2 files changed, 72 insertions(+)

diff --git a/Cubical/Categories/Constructions/Slice/Base.agda b/Cubical/Categories/Constructions/Slice/Base.agda
index e2cfc8d81e..c11652b7cf 100644
--- a/Cubical/Categories/Constructions/Slice/Base.agda
+++ b/Cubical/Categories/Constructions/Slice/Base.agda
@@ -5,6 +5,7 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Path
 open import Cubical.Foundations.Transport using (transpFill)
 
 open import Cubical.Categories.Category renaming (isIso to isIsoC)
@@ -69,6 +70,21 @@ module _ {xf yg : SliceOb} where
 
   SOPath≡PathΣ = ua (isoToEquiv SOPathIsoPathΣ)
 
+-- If the type of objects of C forms a set then so does the type of objects of the slice cat
+module _ (isSetCOb : isSet (C .ob)) where
+  isSetSliceOb : isSet SliceOb
+  isSetSliceOb x y =
+    subst
+      (λ t → isProp t)
+      (sym (SOPath≡PathΣ {xf = x} {yg = y}))
+      (isPropΣ
+        (isSetCOb (x .S-ob) (y .S-ob))
+        λ x≡y →
+          subst
+            (λ t → isProp t)
+            (sym (ua (PathP≃Path (λ i → C [ x≡y i , c ]) (x .S-arr) (y .S-arr))))
+            (C .isSetHom (transport (λ i → C [ x≡y i , c ]) (x .S-arr)) (y .S-arr)))
+
 -- intro and elim for working with SliceHom equalities (is there a better way to do this?)
 SliceHom-≡-intro : ∀ {a b} {f g} {c₁} {c₂}
                 → (p : f ≡ g)
diff --git a/Cubical/Categories/Constructions/SubObject.agda b/Cubical/Categories/Constructions/SubObject.agda
index 45b420e4cd..2a5040bd49 100644
--- a/Cubical/Categories/Constructions/SubObject.agda
+++ b/Cubical/Categories/Constructions/SubObject.agda
@@ -2,6 +2,8 @@
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Powerset
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Univalence
 
 open import Cubical.Data.Sigma
 
@@ -9,6 +11,8 @@ open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Morphism
 
+open import Cubical.Relation.Binary.Order.Preorder
+
 open Category
 
 module Cubical.Categories.Constructions.SubObject
@@ -33,3 +37,55 @@ subObjMorIsMonic : {s t : SubObjCat .ob} (f : SubObjCat [ s , t ])
 subObjMorIsMonic {s = s} {t = t} f = postcompCreatesMonic C
   (S-hom f) (S-arr (t .fst)) comp-is-monic
   where comp-is-monic = subst (isMonic C) (sym (S-comm f)) (s .snd)
+
+isPropSubObjMor : (s t : SubObjCat .ob) → isProp (SubObjCat [ s , t ])
+SliceHom.S-hom
+  (isPropSubObjMor
+    (sliceob incS , isMonicIncS)
+    (sliceob incT , isMonicIncT)
+    (slicehom x xComm)
+    (slicehom y yComm) i) =
+    isMonicIncT {a = x} {a' = y} (xComm ∙ sym  yComm) i
+SliceHom.S-comm
+  (isPropSubObjMor
+    (sliceob incS , isMonicIncS)
+    (sliceob incT , isMonicIncT)
+    (slicehom x xComm)
+    (slicehom y yComm) i) =
+    isProp→PathP (λ i → C .isSetHom (seq' C (isMonicIncT (xComm ∙ sym yComm) i) incT) incS) xComm yComm i
+
+isReflSubObjMor : (x : SubObjCat .ob) → SubObjCat [ x , x ]
+SliceHom.S-hom (isReflSubObjMor (sliceob inc , isMonicInc)) = C .id
+SliceHom.S-comm (isReflSubObjMor (sliceob inc , isMonicInc)) = C .⋆IdL inc
+
+isTransSubObjMor : (x y z : SubObjCat .ob) → SubObjCat [ x , y ] → SubObjCat [ y , z ] → SubObjCat [ x , z ]
+SliceHom.S-hom
+  (isTransSubObjMor
+    (sliceob incX , isMonicIncX)
+    (sliceob incY , isMonicIncY)
+    (sliceob incZ , isMonicIncZ)
+    (slicehom f fComm)
+    (slicehom g gComm)) = seq' C f g
+SliceHom.S-comm
+  (isTransSubObjMor
+    (sliceob incX , isMonicIncX)
+    (sliceob incY , isMonicIncY)
+    (sliceob incZ , isMonicIncZ)
+    (slicehom f fComm)
+    (slicehom g gComm)) =
+  seq' C (seq' C f g) incZ
+    ≡⟨ C .⋆Assoc f g incZ ⟩
+  seq' C f (seq' C g incZ)
+    ≡⟨ cong (λ x → seq' C f x) gComm ⟩
+  seq' C f incY
+    ≡⟨ fComm ⟩
+  incX
+    ∎
+
+module _ (isSetCOb : isSet (C .ob)) where
+  subObjCatPreorderStr : PreorderStr _ (SubObjCat .ob)
+  PreorderStr._≲_ subObjCatPreorderStr x y = SubObjCat [ x , y ]
+  IsPreorder.is-set (PreorderStr.isPreorder subObjCatPreorderStr) = isSetΣ (isSetSliceOb isSetCOb) λ x → isProp→isSet (∈-isProp isSubObj x)
+  IsPreorder.is-prop-valued (PreorderStr.isPreorder subObjCatPreorderStr) = isPropSubObjMor
+  IsPreorder.is-refl (PreorderStr.isPreorder subObjCatPreorderStr) = isReflSubObjMor
+  IsPreorder.is-trans (PreorderStr.isPreorder subObjCatPreorderStr) = isTransSubObjMor