From f4bb7741c82efab71357270b513e6fa5c6720fe5 Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Tue, 30 May 2023 13:07:18 -0400
Subject: [PATCH] Begin formalizing coalgebras categorically

---
 .../Cubical/Categories/Coalgebra.agda         | 58 +++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100644 formalizations/guarded-cubical/Cubical/Categories/Coalgebra.agda

diff --git a/formalizations/guarded-cubical/Cubical/Categories/Coalgebra.agda b/formalizations/guarded-cubical/Cubical/Categories/Coalgebra.agda
new file mode 100644
index 0000000..90bb156
--- /dev/null
+++ b/formalizations/guarded-cubical/Cubical/Categories/Coalgebra.agda
@@ -0,0 +1,58 @@
+
+
+module Cubical.Categories.Coalgebra where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Data.Sigma
+
+
+private
+  variable
+    â„“ â„“' : Level
+
+module _ (C : Category â„“ â„“') (F : Functor C C) where
+
+  open Category
+
+  record Coalgebra : Type (â„“-max â„“ â„“') where
+    field
+      V : C .ob
+      un : C [ V , F ⟅ V ⟆ ]
+
+  open Coalgebra
+
+  record CoalgMorphism (c d : Coalgebra) : Type â„“' where
+    field
+      f : C [ c .V , d .V ]
+      com : d .un ∘⟨ C ⟩ f ≡ F ⟪ f ⟫ ∘⟨ C ⟩ c .un
+
+  open CoalgMorphism
+
+  is-final : Coalgebra -> Type (â„“-max â„“ â„“')
+  is-final d = ∀ (c : Coalgebra) -> isContr (CoalgMorphism c d)
+
+  FinalCoalg : Type (â„“-max â„“ â„“')
+  FinalCoalg = Σ[ c ∈ Coalgebra ] is-final c
+
+
+  -- Final coalgebras are unique up to unique isomorphism
+  final-unique : (c c' : FinalCoalg) ->
+    isContr (Σ[ α ∈ CoalgMorphism (fst c) (fst c') ] (isIso C (α .f)))
+    -- CatIso C (fst c .V) (fst c' .V)
+  final-unique c c' = (!c' , {!!}) , {!!}
+    where
+      !c : CoalgMorphism (fst c') (fst c)
+      !c = fst (snd c (fst c'))
+
+      !c' : CoalgMorphism (fst c) (fst c')
+      !c' = fst (snd c' (fst c))
+
+      isom : isIso C (!c' .f)
+      isom = isiso (!c .f) {!!} {!!}
+
+     
+
+
-- 
GitLab