Define Dagger categories

Cubical/Categories/Dagger.agda

@@ -0,0 +1,8 @@
+-- Dagger categories
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Dagger where
+
+open import Cubical.Categories.Dagger.Base public
+open import Cubical.Categories.Dagger.Properties public
+open import Cubical.Categories.Dagger.Functor public

Cubical/Categories/Dagger/Base.agda

@@ -0,0 +1,74 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Dagger.Base where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Categories.Category
+
+private variable
+  ℓ ℓ' : Level
+
+module _ (C : Category ℓ ℓ') where
+  open Category C
+  private variable
+    x y z w : ob
+
+  record IsDagger (_† : {x y : ob} → Hom[ x , y ] → Hom[ y , x ]) : Type (ℓ-max ℓ ℓ') where
+    field
+      †-invol : (f : Hom[ x , y ]) → f † † ≡ f
+      †-id : id † ≡ id {x}
+      †-seq : (f : Hom[ x , y ]) (g : Hom[ y , z ]) → (f ⋆ g) † ≡ g † ⋆ f †
+
+  open IsDagger
+
+  makeIsDagger : {_† : {x y : ob} → Hom[ x , y ] → Hom[ y , x ]}
+               → (∀ {x y} (f : Hom[ x , y ]) → f † † ≡ f)
+               → (∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → (f ⋆ g) † ≡ g † ⋆ f †)
+               → IsDagger _†
+  makeIsDagger {_†} †-invol †-seq .†-invol = †-invol
+  makeIsDagger {_†} †-invol †-seq .†-seq   = †-seq
+  makeIsDagger {_†} †-invol †-seq .†-id    = -- this actually follows from the other axioms
+    id †          ≡⟨ sym (⋆IdR _) ⟩
+    id † ⋆ id     ≡⟨ congR _⋆_ (sym (†-invol id)) ⟩
+    id † ⋆ id † † ≡⟨ sym (†-seq (id †) id) ⟩
+    (id † ⋆ id) † ≡⟨ cong _† (⋆IdR _) ⟩
+    id † †        ≡⟨ †-invol id ⟩
+    id            ∎
+
+  record DaggerStr : Type (ℓ-max ℓ ℓ') where
+    field
+      _† : Hom[ x , y ] → Hom[ y , x ]
+      is-dag : IsDagger _†
+
+    open IsDagger is-dag public
+
+
+record DagCat (ℓ ℓ' : Level) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
+  no-eta-equality
+
+  field
+    cat : Category ℓ ℓ'
+    dagstr : DaggerStr cat
+
+  open DaggerStr dagstr public
+  open Category cat public
+
+open IsDagger
+open DaggerStr
+open DagCat
+
+dag : ∀ (C : DagCat ℓ ℓ') {x y} → C .cat [ x , y ] → C .cat [ y , x ]
+dag C x = C ._† x
+
+syntax dag C x = x †[ C ]
+
+opDaggerStr : {C : Category ℓ ℓ'} → DaggerStr C → DaggerStr (C ^op)
+opDaggerStr d ._†     = d ._†
+opDaggerStr d .is-dag .†-invol = d .is-dag .†-invol
+opDaggerStr d .is-dag .†-id    = d .is-dag .†-id
+opDaggerStr d .is-dag .†-seq   f g = d .is-dag .†-seq g f
+
+opDagCat : DagCat ℓ ℓ' → DagCat ℓ ℓ'
+opDagCat C .cat    = C .cat ^op
+opDagCat C .dagstr = opDaggerStr (C .dagstr)

Cubical/Categories/Dagger/Functor.agda

@@ -0,0 +1,80 @@
+{-# OPTIONS --safe --hidden-argument-puns #-}
+
+module Cubical.Categories.Dagger.Functor where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Functors.Constant
+
+open import Cubical.Categories.Dagger.Base
+
+private variable
+  ℓC ℓC' ℓD ℓD' ℓ ℓ' ℓ'' ℓ''' : Level
+  C D E : DagCat ℓ ℓ'
+
+open DagCat
+
+module _ (C : DagCat ℓC ℓC') (D : DagCat ℓD ℓD') where
+  record IsDagFunctor (F : Functor (C .cat) (D .cat)) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
+    no-eta-equality
+    field
+      F-† : ∀ {x y} (f : C .cat [ x , y ]) → F ⟪ f †[ C ] ⟫ ≡ F ⟪ f ⟫ †[ D ]
+
+  open IsDagFunctor public
+
+  isPropIsDagFunctor : ∀ F → isProp (IsDagFunctor F)
+  isPropIsDagFunctor F a b i .F-† f = D .isSetHom _ _ (a .F-† f) (b .F-† f) i
+
+  DagFunctor : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
+  DagFunctor = Σ[ F ∈ Functor (C .cat) (D .cat) ] IsDagFunctor F
+
+open Functor
+
+†Id : DagFunctor C C
+†Id .fst = Id
+†Id .snd .F-† f = refl
+
+†FuncComp : DagFunctor C D → DagFunctor D E → DagFunctor C E
+†FuncComp F G .fst = G .fst ∘F F .fst
+†FuncComp {C = C} {D = D} {E = E} F G .snd .F-† f =
+  G .fst ⟪ F .fst ⟪ f †[ C ] ⟫ ⟫ ≡⟨ cong (G .fst .F-hom) (F .snd .F-† f) ⟩
+  G .fst ⟪ F .fst ⟪ f ⟫ †[ D ] ⟫ ≡⟨ G .snd .F-† (F .fst .F-hom f) ⟩
+  G .fst ⟪ F .fst ⟪ f ⟫ ⟫ †[ E ] ∎
+
+_∘†F_ : DagFunctor D E → DagFunctor C D → DagFunctor C E
+G ∘†F F = †FuncComp F G
+
+†Func^op : DagFunctor C D → DagFunctor (opDagCat C) (opDagCat D)
+†Func^op F .fst = F .fst ^opF
+†Func^op F .snd .F-† f = F .snd .F-† f
+
+†Func≡ : (F G : DagFunctor C D) → F .fst ≡ G .fst → F ≡ G
+†Func≡ {C} {D} F G = Σ≡Prop (isPropIsDagFunctor C D)
+
+open DagCat
+
+†Const : ob D → DagFunctor C D
+†Const {D} d .fst = Constant _ _ d
+†Const {D} d .snd .F-† _ = sym (D .†-id)
+
+open NatTrans
+
+NT† : (F G : DagFunctor C D) → NatTrans (F .fst) (G .fst) → NatTrans (G .fst) (F .fst)
+NT† {C} {D} F G n .N-ob x = n ⟦ x ⟧ †[ D ]
+NT† {C} {D} F G n .N-hom {x} {y} f =
+  G .fst ⟪ f ⟫ ⋆D n ⟦ y ⟧ †D       ≡⟨ congL _⋆D_ (sym (D .†-invol (G .fst ⟪ f ⟫))) ⟩
+  G .fst ⟪ f ⟫ †D †D ⋆D n ⟦ y ⟧ †D ≡⟨ sym (D .†-seq (n ⟦ y ⟧) (G .fst ⟪ f ⟫ †D)) ⟩
+  (n ⟦ y ⟧ ⋆D G .fst ⟪ f ⟫ †D) †D  ≡⟨ cong _†D (congR _⋆D_ (sym (G .snd .F-† f))) ⟩
+  (n ⟦ y ⟧ ⋆D G .fst ⟪ f †C ⟫) †D  ≡⟨ cong _†D (sym (n .N-hom (f †C))) ⟩
+  (F .fst ⟪ f †C ⟫ ⋆D n ⟦ x ⟧) †D  ≡⟨ cong _†D (congL _⋆D_ (F .snd .F-† f)) ⟩
+  (F .fst ⟪ f ⟫ †D ⋆D n ⟦ x ⟧) †D  ≡⟨ D .†-seq (F .fst ⟪ f ⟫ †D) (n ⟦ x ⟧) ⟩
+  n ⟦ x ⟧ †D ⋆D F .fst ⟪ f ⟫ †D †D ≡⟨ congR _⋆D_ (D .†-invol (F .fst ⟪ f ⟫)) ⟩
+  n ⟦ x ⟧ †D ⋆D F .fst ⟪ f ⟫       ∎
+
+  where
+    open DagCat D using () renaming (_⋆_ to _⋆D_; _† to _†D)
+    open DagCat C using () renaming (_⋆_ to _⋆C_; _† to _†C)

Cubical/Categories/Dagger/Instances/BinProduct.agda

@@ -0,0 +1,73 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Dagger.Instances.BinProduct where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Morphism
+
+open import Cubical.Categories.Dagger.Base
+open import Cubical.Categories.Dagger.Properties
+open import Cubical.Categories.Dagger.Functor
+
+private variable
+  ℓ ℓ' ℓ'' ℓ''' : Level
+
+open DaggerStr
+open IsDagger
+open DagCat
+
+BinProdDaggerStr : {C : Category ℓ ℓ'} {D : Category ℓ'' ℓ'''} → DaggerStr C → DaggerStr D → DaggerStr (C ×C D)
+BinProdDaggerStr dagC dagD ._† (f , g) = dagC ._† f , dagD ._† g
+BinProdDaggerStr dagC dagD .is-dag .†-invol (f , g) = ≡-× (dagC .†-invol f) (dagD .†-invol g)
+BinProdDaggerStr dagC dagD .is-dag .†-id = ≡-× (dagC .†-id) (dagD .†-id)
+BinProdDaggerStr dagC dagD .is-dag .†-seq (f , g) (f' , g') = ≡-× (dagC .†-seq f f') (dagD .†-seq g g')
+
+DagBinProd _×D_ : DagCat ℓ ℓ' → DagCat ℓ'' ℓ''' → DagCat (ℓ-max ℓ ℓ'') (ℓ-max ℓ' ℓ''')
+DagBinProd C D .cat = C .cat ×C D .cat
+DagBinProd C D .dagstr = BinProdDaggerStr (C .dagstr) (D .dagstr)
+_×D_ = DagBinProd
+
+module _ (C : DagCat ℓ ℓ') (D : DagCat ℓ'' ℓ''') where
+  †Fst : DagFunctor (C ×D D) C
+  †Fst .fst = Fst (C .cat) (D .cat)
+  †Fst .snd .F-† (f , g) = refl
+
+  †Snd : DagFunctor (C ×D D) D
+  †Snd .fst = Snd (C .cat) (D .cat)
+  †Snd .snd .F-† (f , g) = refl
+
+module _ where
+  private variable
+    B C D E : DagCat ℓ ℓ'
+
+  _,†F_ : DagFunctor C D → DagFunctor C E → DagFunctor C (D ×D E)
+  (F ,†F G) .fst = F .fst ,F G .fst
+  (F ,†F G) .snd .F-† f = ≡-× (F .snd .F-† f) (G .snd .F-† f)
+
+  _׆F_ : DagFunctor B D → DagFunctor C E → DagFunctor (B ×D C) (D ×D E)
+  _׆F_ {B = B} {C = C} F G = (F ∘†F †Fst B C) ,†F (G ∘†F †Snd B C)
+
+  †Δ : DagFunctor C (C ×D C)
+  †Δ = †Id ,†F †Id
+
+module _ (C : DagCat ℓ ℓ') (D : DagCat ℓ'' ℓ''') where
+  †Swap : DagFunctor (C ×D D) (D ×D C)
+  †Swap = †Snd C D ,†F †Fst C D
+
+  †Linj : ob D → DagFunctor C (C ×D D)
+  †Linj d = †Id ,†F †Const d
+
+  †Rinj : ob C → DagFunctor D (C ×D D)
+  †Rinj c = †Const c ,†F †Id
+
+  open areInv
+
+  †CatIso× : ∀ {x y z w} → †CatIso C x y → †CatIso D z w → †CatIso (C ×D D) (x , z) (y , w)
+  †CatIso× (f , fiso) (g , giso) .fst = f , g
+  †CatIso× (f , fiso) (g , giso) .snd .sec = ≡-× (fiso .sec) (giso .sec)
+  †CatIso× (f , fiso) (g , giso) .snd .ret = ≡-× (fiso .ret) (giso .ret)

Cubical/Categories/Dagger/Instances/Functors.agda

@@ -0,0 +1,34 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Dagger.Instances.Functors where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Constructions.FullSubcategory
+open import Cubical.Categories.Instances.Functors
+
+open import Cubical.Categories.Dagger.Base
+open import Cubical.Categories.Dagger.Properties
+open import Cubical.Categories.Dagger.Functor
+
+private variable
+  ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level
+
+module _ (C : DagCat ℓC ℓC') (D : DagCat ℓD ℓD') where
+
+  open Category
+  open DagCat
+  open DaggerStr
+  open IsDagger
+  open NatTrans
+
+  †FUNCTOR : DagCat (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) (ℓ-max (ℓ-max ℓC ℓC') ℓD')
+  †FUNCTOR .cat = FullSubcategory (FUNCTOR (C .cat) (D .cat)) (IsDagFunctor C D)
+  †FUNCTOR .dagstr ._† {x = F} {y = G} = NT† F G
+  †FUNCTOR .dagstr .is-dag .†-invol n = makeNatTransPath (funExt λ x → D .†-invol (n ⟦ x ⟧))
+  †FUNCTOR .dagstr .is-dag .†-id = makeNatTransPath (funExt λ x → D .†-id)
+  †FUNCTOR .dagstr .is-dag .†-seq m n = makeNatTransPath (funExt λ x → D .†-seq (m ⟦ x ⟧) (n ⟦ x ⟧))