From cdf3c3396d1f129922335f5478e1331c6285cc6c Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 20 Oct 2022 18:22:13 -0400
Subject: [PATCH] More guarded cat ideas

---
 .../guarded-cubical/GuardedCat.agda           | 60 ++++++++++++++++++-
 1 file changed, 59 insertions(+), 1 deletion(-)

diff --git a/formalizations/guarded-cubical/GuardedCat.agda b/formalizations/guarded-cubical/GuardedCat.agda
index 210839d..cc6c059 100644
--- a/formalizations/guarded-cubical/GuardedCat.agda
+++ b/formalizations/guarded-cubical/GuardedCat.agda
@@ -8,6 +8,11 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Adjoint
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Instances.Functors
+open import Cubical.Categories.Constructions.BinProduct
+
+open import Cubical.Categories.Instances.Sets
 
 variable
   â„“ â„“' : Level
@@ -24,7 +29,21 @@ variable
          ; isSetHom = λ x y → λ p:x≡y q:x≡y i j t → Category.isSetHom (C t) (x t) (y t) (λ k → p:x≡y k t) ((λ k → q:x≡y k t)) i j
          }
 
-next-c : ∀ (C : Category ℓ ℓ') → Functor C (▸c (next C))
+
+▹c : ∀ (C : Category ℓ ℓ') → Category ℓ ℓ'
+â–¹c C = â–¸c (next C)
+
+▹F : ∀ {C D : Category ℓ ℓ'} → Functor C D → Functor (▹c C) (▹c D)
+â–¹F F = record
+  { F-ob = λ x t → F-ob (x t)
+  ; F-hom = λ x t → F-hom (x t)
+  ; F-id = λ i t → F-id i
+  ; F-seq = λ f g i t → F-seq (f t) (g t) i
+  }
+  where module F = Functor F
+        open F
+
+next-c : ∀ (C : Category ℓ ℓ') → Functor C (▹c C)
 next-c C = record
   { F-ob = λ x t → x
   ; F-hom = λ z t → z
@@ -41,3 +60,42 @@ record GuardedCat : Type (â„“-suc (â„“-max â„“ â„“')) where
     θ-UMP : isRightAdjoint (next-c C)
 
 -- Conjecture: Every GuardedCat has an initial object ⊥ = fix θ₀
+
+
+PROF : (ℓ' : Level) → (C : Category ℓ ℓ') (D : Category ℓ ℓ') → Category (ℓ-max ℓ (ℓ-suc ℓ')) (ℓ-max ℓ ℓ')
+PROF ℓ' C D = FUNCTOR ((C ^op) × D) (SET ℓ')
+
+Profunctor : (C : Category ℓ ℓ') (D : Category ℓ ℓ') → Type (ℓ-max ℓ (ℓ-suc ℓ'))
+Profunctor C D = Category.ob (PROF _ C D)
+
+-- e : A → B
+-- p : B → ▹ A
+
+-- e a ~> b
+-- iff (next a) ~> p b
+-- defines e as a relative left adjoint
+-- doesn't uniquely determine p
+
+-- aâ–¹ ~> p b
+-- iff ▹ (λ t → e (a▹ t) ~> b)
+-- iff (â–¹ e) aâ–¹ ~> (next b)
+-- defines p as a relative right adjoint
+-- doesn't uniquely determine e
+
+-- e seems more fundamental than p tbh...but which of these holds period?
+
+
+-- e : A → B
+-- p : B → Option (▹ A)
+
+-- e a ~> b
+-- iff some (next a) ~> p b
+-- defines e as a relative left adjoint
+-- doesn't uniquely determine p
+
+-- a?â–¹ ~> p b
+-- iff Option (â–¹ e) aâ–¹ ~> (next b)
+-- defines p as a relative right adjoint
+-- doesn't uniquely determine e
+
+-- ▹p : Profunctor C D → (Profunctor (▹ C) (▹ D))
-- 
GitLab