From ddaccf7dc2ec02a7eaf39b52f9744be2459118cb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Sat, 8 Mar 2025 11:26:43 -0300
Subject: [PATCH] connect generic subobjects and generic sub-objects

---
 src/Cat/Diagram/Omega.lagda.md | 37 ++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/src/Cat/Diagram/Omega.lagda.md b/src/Cat/Diagram/Omega.lagda.md
index 2d19e97f5..984403f46 100644
--- a/src/Cat/Diagram/Omega.lagda.md
+++ b/src/Cat/Diagram/Omega.lagda.md
@@ -3,9 +3,11 @@
 open import 1Lab.Reflection.Copattern
 
 open import Cat.Diagram.Pullback.Properties
+open import Cat.Displayed.GenericObject
 open import Cat.Instances.Sets.Complete
 open import Cat.Diagram.Pullback.Along
 open import Cat.Diagram.Limit.Finite
+open import Cat.Displayed.Cartesian
 open import Cat.Diagram.Pullback
 open import Cat.Diagram.Terminal
 open import Cat.Instances.Sets
@@ -244,6 +246,41 @@ fiddling, but it's nothing outrageous.
     (λ ha → inc ((a , lift tt , ap lift (to-is-true ha)) , refl))
 ```
 
+## As generic objects
+
+We can connect the definition above with that of [[generic objects]] in
+a [[fibration]]: specifically, a generic subobject is a generic object
+in the fibration of subobjects. The similar naming is not an accident:
+the proof boils down to shuffling data around.
+
+<!--
+```agda
+module _ {o ℓ} (C : Precategory o ℓ)  where
+  open is-generic-subobject
+  open is-pullback-along
+  open Generic-object
+  open Cat.Reasoning C using (pulll)
+  open is-cartesian
+  open Subobjs C
+```
+-->
+
+```agda
+  from-generic-subobject
+    : ∀ {Ω} {tru : Subobject Ω} → is-generic-subobject C tru
+    → Generic-object Subobjects tru
+  from-generic-subobject gen .classify    = gen .name
+  from-generic-subobject gen .classify' s = record { sq = gen .classifies s .square }
+  from-generic-subobject gen .classify-cartesian s = record
+    { universal = λ {u} {u'} m a → record
+      { map = gen .classifies s .universal (pulll refl ∙ a .sq)
+      ; sq = sym (gen .classifies s .p₁∘universal)
+      }
+    ; commutes  = λ m h → prop!
+    ; unique    = λ m h → prop!
+    }
+```
+
 <!--
 ```agda
 open Subobject-classifier using (unique)