From 976b565a36267bfd1bf43bf0764c04b29745a2c6 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 20 Oct 2022 14:38:32 -0400
Subject: [PATCH] theta as a left adjoint?

---
 .../guarded-cubical/GuardedCat.agda           | 43 +++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 formalizations/guarded-cubical/GuardedCat.agda

diff --git a/formalizations/guarded-cubical/GuardedCat.agda b/formalizations/guarded-cubical/GuardedCat.agda
new file mode 100644
index 0000000..210839d
--- /dev/null
+++ b/formalizations/guarded-cubical/GuardedCat.agda
@@ -0,0 +1,43 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+open import Later
+
+module GuardedCat (k : Clock) where
+
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Adjoint
+
+variable
+  â„“ â„“' : Level
+
+▸c : ∀ (C : ▹ k , Category ℓ ℓ') → Category ℓ ℓ'
+â–¸c C = record
+         { ob = ▸ λ t → Category.ob (C t)
+         ; Hom[_,_] = λ a b → ▸ (λ t → Category.Hom[_,_] (C t) (a t) (b t))
+         ; id = λ t → Category.id (C t)
+         ; _⋆_ = λ f g t → Category._⋆_ (C t) (f t) (g t)
+         ; ⋆IdL = λ f i t → Category.⋆IdL (C t) (f t) i
+         ; ⋆IdR = λ f i t → Category.⋆IdR (C t) (f t) i
+         ; ⋆Assoc = λ f g h i t → Category.⋆Assoc (C t) (f t) (g t) (h t) i
+         ; 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))
+next-c C = record
+  { F-ob = λ x t → x
+  ; F-hom = λ z t → z
+  ; F-id = λ i t → C.id
+  ; F-seq = λ f g i t → f ⋆ g
+  }
+  where module C = Category C
+        open C
+
+record GuardedCat : Type (â„“-suc (â„“-max â„“ â„“')) where
+  open NaturalBijection
+  field
+    C : Category â„“ â„“'
+    θ-UMP : isRightAdjoint (next-c C)
+
+-- Conjecture: Every GuardedCat has an initial object ⊥ = fix θ₀
-- 
GitLab