Skip to content

Commit d96372c

Browse files
anshwad10anshwad10
authored
Define Dagger categories (#1201)
* Create folder for Dagger Categories * Add files via upload * Update Base.agda * Add files via upload * Update Properties.agda * add syntax for dagger, fix whitespace, other minor improvements * fix whitespace, add more lemmas for univalence * Add files via upload * Dagger functors * `areInv` is a proposition * Update Properties.agda * fix whitespace * fix whitespace * remove trailing newlines * Update Morphism.agda * fix type error * fix import * Create Dagger.agda * Update Properties.agda * undo Update Properties.agda * Update Functor.agda * add binary products of dagger categories * Add files via upload * Update Functors.agda * Update BinProduct.agda * fix whitespace * fix whitespace * fix whitespace * Update Functor.agda * Update Functor.agda * import Functors.Constant * import natural transformations * add hidden argument puns * Update Properties.agda * Update Properties.agda * Every dagger category is equivalent to its opposite * fix whitespace * Credit Karvonen, rename PIso * Consistent naming * fix whitespace * Update BinProduct.agda * Update Functors.agda * Update Dagger.agda * fix naming * remove unnecessary --safe
1 parent d569148 commit d96372c

File tree

7 files changed

+494
-0
lines changed

7 files changed

+494
-0
lines changed

‎Cubical/Categories/Dagger.agda‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
-- Dagger categories
2+
{-# OPTIONS --safe #-}
3+
4+
module Cubical.Categories.Dagger where
5+
6+
open import Cubical.Categories.Dagger.Base public
7+
open import Cubical.Categories.Dagger.Properties public
8+
open import Cubical.Categories.Dagger.Functor public
9+
open import Cubical.Categories.Dagger.Instances.BinProduct public
10+
open import Cubical.Categories.Dagger.Instances.Functors public

‎Cubical/Categories/Dagger/Base.agda‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
{-# OPTIONS --safe #-}
2+
3+
module Cubical.Categories.Dagger.Base where
4+
5+
open import Cubical.Foundations.Prelude
6+
7+
open import Cubical.Categories.Category
8+
9+
private variable
10+
ℓ ℓ' : Level
11+
12+
module _ (C : Category ℓ ℓ') where
13+
open Category C
14+
private variable
15+
x y z w : ob
16+
17+
record IsDagger (_† : {x y : ob} → Hom[ x , y ] → Hom[ y , x ]) : Type (ℓ-max ℓ ℓ') where
18+
field
19+
†-invol : (f : Hom[ x , y ]) → f † † ≡ f
20+
†-id : id † ≡ id {x}
21+
†-seq : (f : Hom[ x , y ]) (g : Hom[ y , z ]) → (f ⋆ g) † ≡ g † ⋆ f †
22+
23+
open IsDagger
24+
25+
makeIsDagger : {_† : {x y : ob} → Hom[ x , y ] → Hom[ y , x ]}
26+
→ (∀ {x y} (f : Hom[ x , y ]) → f † † ≡ f)
27+
→ (∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → (f ⋆ g) † ≡ g † ⋆ f †)
28+
→ IsDagger _†
29+
makeIsDagger {_†} †-invol †-seq .†-invol = †-invol
30+
makeIsDagger {_†} †-invol †-seq .†-seq = †-seq
31+
makeIsDagger {_†} †-invol †-seq .†-id = -- this actually follows from the other axioms
32+
id † ≡⟨ sym (⋆IdR _) ⟩
33+
id † ⋆ id ≡⟨ congR _⋆_ (sym (†-invol id)) ⟩
34+
id † ⋆ id † † ≡⟨ sym (†-seq (id †) id) ⟩
35+
(id † ⋆ id) † ≡⟨ cong _† (⋆IdR _) ⟩
36+
id † † ≡⟨ †-invol id ⟩
37+
id ∎
38+
39+
record DaggerStr : Type (ℓ-max ℓ ℓ') where
40+
field
41+
_† : Hom[ x , y ] → Hom[ y , x ]
42+
is-dag : IsDagger _†
43+
44+
open IsDagger is-dag public
45+
46+
47+
record †Category (ℓ ℓ' : Level) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
48+
no-eta-equality
49+
50+
field
51+
cat : Category ℓ ℓ'
52+
dagstr : DaggerStr cat
53+
54+
open DaggerStr dagstr public
55+
open Category cat public
56+
57+
open IsDagger
58+
open DaggerStr
59+
open †Category
60+
61+
dag : ∀ (C : †Category ℓ ℓ') {x y} → C .cat [ x , y ] → C .cat [ y , x ]
62+
dag C f = C ._† f
63+
64+
syntax dag C f = f †[ C ]

‎Cubical/Categories/Dagger/Functor.agda‎

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
{-# OPTIONS --hidden-argument-puns #-}
2+
3+
module Cubical.Categories.Dagger.Functor where
4+
5+
open import Cubical.Foundations.Prelude
6+
open import Cubical.Data.Sigma
7+
8+
open import Cubical.Categories.Category
9+
open import Cubical.Categories.Functor
10+
open import Cubical.Categories.NaturalTransformation
11+
open import Cubical.Categories.Functors.Constant
12+
13+
open import Cubical.Categories.Dagger.Base
14+
15+
private variable
16+
ℓC ℓC' ℓD ℓD' ℓ ℓ' ℓ'' ℓ''' : Level
17+
C D E : †Category ℓ ℓ'
18+
19+
open †Category
20+
21+
module _ (C : †Category ℓC ℓC') (D : †Category ℓD ℓD') where
22+
record Is†Functor (F : Functor (C .cat) (D .cat)) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
23+
no-eta-equality
24+
field
25+
F-† : ∀ {x y} (f : C .cat [ x , y ]) → F ⟪ f †[ C ] ⟫ ≡ F ⟪ f ⟫ †[ D ]
26+
27+
open Is†Functor public
28+
29+
isPropIs†Functor : ∀ F → isProp (Is†Functor F)
30+
isPropIs†Functor F a b i .F-† f = D .isSetHom _ _ (a .F-† f) (b .F-† f) i
31+
32+
†Functor : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
33+
†Functor = Σ[ F ∈ Functor (C .cat) (D .cat) ] Is†Functor F
34+
35+
open Functor
36+
37+
†Id : †Functor C C
38+
†Id .fst = Id
39+
†Id .snd .F-† f = refl
40+
41+
†FuncComp : †Functor C D → †Functor D E → †Functor C E
42+
†FuncComp F G .fst = G .fst ∘F F .fst
43+
†FuncComp {C} {D} {E} F G .snd .F-† f =
44+
G .fst ⟪ F .fst ⟪ f †[ C ] ⟫ ⟫ ≡⟨ cong (G .fst .F-hom) (F .snd .F-† f) ⟩
45+
G .fst ⟪ F .fst ⟪ f ⟫ †[ D ] ⟫ ≡⟨ G .snd .F-† (F .fst .F-hom f) ⟩
46+
G .fst ⟪ F .fst ⟪ f ⟫ ⟫ †[ E ] ∎
47+
48+
_∘†F_ : †Functor D E → †Functor C D → †Functor C E
49+
G ∘†F F = †FuncComp F G
50+
51+
†Func≡ : (F G : †Functor C D) → F .fst ≡ G .fst → F ≡ G
52+
†Func≡ {C} {D} F G = Σ≡Prop (isPropIs†Functor C D)
53+
54+
open †Category
55+
56+
†Constant : ob D → †Functor C D
57+
†Constant {D} d .fst = Constant _ _ d
58+
†Constant {D} d .snd .F-† _ = sym (D .†-id)
59+
60+
open NatTrans
61+
62+
NT† : (F G : †Functor C D) → NatTrans (F .fst) (G .fst) → NatTrans (G .fst) (F .fst)
63+
NT† {C} {D} F G n .N-ob x = n ⟦ x ⟧ †[ D ]
64+
NT† {C} {D} F G n .N-hom {x} {y} f =
65+
G .fst ⟪ f ⟫ D.⋆ n ⟦ y ⟧ D.† ≡⟨ congL D._⋆_ (sym (D .†-invol (G .fst ⟪ f ⟫))) ⟩
66+
G .fst ⟪ f ⟫ D.† D.† D.⋆ n ⟦ y ⟧ D.† ≡⟨ sym (D .†-seq (n ⟦ y ⟧) (G .fst ⟪ f ⟫ D.†)) ⟩
67+
(n ⟦ y ⟧ D.⋆ G .fst ⟪ f ⟫ D.†) D.† ≡⟨ cong D._† (congR D._⋆_ (sym (G .snd .F-† f))) ⟩
68+
(n ⟦ y ⟧ D.⋆ G .fst ⟪ f C.† ⟫) D.† ≡⟨ cong D._† (sym (n .N-hom (f C.†))) ⟩
69+
(F .fst ⟪ f C.† ⟫ D.⋆ n ⟦ x ⟧) D.† ≡⟨ cong D._† (congL D._⋆_ (F .snd .F-† f)) ⟩
70+
(F .fst ⟪ f ⟫ D.† D.⋆ n ⟦ x ⟧) D.† ≡⟨ D .†-seq (F .fst ⟪ f ⟫ D.†) (n ⟦ x ⟧) ⟩
71+
n ⟦ x ⟧ D.† D.⋆ F .fst ⟪ f ⟫ D.† D.† ≡⟨ congR D._⋆_ (D .†-invol (F .fst ⟪ f ⟫)) ⟩
72+
n ⟦ x ⟧ D.† D.⋆ F .fst ⟪ f ⟫ ∎
73+
where module D = †Category D; module C = †Category C

‎Cubical/Categories/Dagger/Instances/BinProduct.agda‎

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
module Cubical.Categories.Dagger.Instances.BinProduct where
2+
3+
open import Cubical.Foundations.Prelude
4+
open import Cubical.Data.Sigma
5+
6+
open import Cubical.Categories.Category
7+
open import Cubical.Categories.Functor
8+
open import Cubical.Categories.Constructions.BinProduct
9+
open import Cubical.Categories.Morphism
10+
11+
open import Cubical.Categories.Dagger.Base
12+
open import Cubical.Categories.Dagger.Properties
13+
open import Cubical.Categories.Dagger.Functor
14+
15+
private variable
16+
ℓ ℓ' ℓ'' ℓ''' : Level
17+
18+
open DaggerStr
19+
open IsDagger
20+
open †Category
21+
22+
BinProdDaggerStr : {C : Category ℓ ℓ'} {D : Category ℓ'' ℓ'''} → DaggerStr C → DaggerStr D → DaggerStr (C ×C D)
23+
BinProdDaggerStr dagC dagD ._† (f , g) = dagC ._† f , dagD ._† g
24+
BinProdDaggerStr dagC dagD .is-dag .†-invol (f , g) = ≡-× (dagC .†-invol f) (dagD .†-invol g)
25+
BinProdDaggerStr dagC dagD .is-dag .†-id = ≡-× (dagC .†-id) (dagD .†-id)
26+
BinProdDaggerStr dagC dagD .is-dag .†-seq (f , g) (f' , g') = ≡-× (dagC .†-seq f f') (dagD .†-seq g g')
27+
28+
†BinProd _׆_ : †Category ℓ ℓ' → †Category ℓ'' ℓ''' → †Category (ℓ-max ℓ ℓ'') (ℓ-max ℓ' ℓ''')
29+
†BinProd C D .cat = C .cat ×C D .cat
30+
†BinProd C D .dagstr = BinProdDaggerStr (C .dagstr) (D .dagstr)
31+
_׆_ = †BinProd
32+
33+
module _ (C : †Category ℓ ℓ') (D : †Category ℓ'' ℓ''') where
34+
†Fst : †Functor (C ׆ D) C
35+
†Fst .fst = Fst (C .cat) (D .cat)
36+
†Fst .snd .F-† (f , g) = refl
37+
38+
†Snd : †Functor (C ׆ D) D
39+
†Snd .fst = Snd (C .cat) (D .cat)
40+
†Snd .snd .F-† (f , g) = refl
41+
42+
module _ where
43+
private variable
44+
B C D E : †Category ℓ ℓ'
45+
46+
_,†F_ : †Functor C D → †Functor C E → †Functor C (D ׆ E)
47+
(F ,†F G) .fst = F .fst ,F G .fst
48+
(F ,†F G) .snd .F-† f = ≡-× (F .snd .F-† f) (G .snd .F-† f)
49+
50+
_׆F_ : †Functor B D → †Functor C E → †Functor (B ׆ C) (D ׆ E)
51+
_׆F_ {B = B} {C = C} F G = (F ∘†F †Fst B C) ,†F (G ∘†F †Snd B C)
52+
53+
†Δ : †Functor C (C ׆ C)
54+
†Δ = †Id ,†F †Id
55+
56+
module _ (C : †Category ℓ ℓ') (D : †Category ℓ'' ℓ''') where
57+
†Swap : †Functor (C ׆ D) (D ׆ C)
58+
†Swap = †Snd C D ,†F †Fst C D
59+
60+
†Linj : ob D → †Functor C (C ׆ D)
61+
†Linj d = †Id ,†F †Constant d
62+
63+
†Rinj : ob C → †Functor D (C ׆ D)
64+
†Rinj c = †Constant c ,†F †Id
65+
66+
open areInv
67+
open †Morphisms
68+
69+
†CatIso× : ∀ {x y z w} → †CatIso C x y → †CatIso D z w → †CatIso (C ׆ D) (x , z) (y , w)
70+
†CatIso× (f , fiso) (g , giso) .fst = f , g
71+
†CatIso× (f , fiso) (g , giso) .snd .sec = ≡-× (fiso .sec) (giso .sec)
72+
†CatIso× (f , fiso) (g , giso) .snd .ret = ≡-× (fiso .ret) (giso .ret)

‎Cubical/Categories/Dagger/Instances/Functors.agda‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
module Cubical.Categories.Dagger.Instances.Functors where
2+
3+
open import Cubical.Foundations.Prelude
4+
open import Cubical.Data.Sigma
5+
6+
open import Cubical.Categories.Category
7+
open import Cubical.Categories.Functor
8+
open import Cubical.Categories.NaturalTransformation
9+
open import Cubical.Categories.Constructions.FullSubcategory
10+
open import Cubical.Categories.Instances.Functors
11+
12+
open import Cubical.Categories.Dagger.Base
13+
open import Cubical.Categories.Dagger.Properties
14+
open import Cubical.Categories.Dagger.Functor
15+
16+
private variable
17+
ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level
18+
19+
module _ (C : †Category ℓC ℓC') (D : †Category ℓD ℓD') where
20+
21+
open Category
22+
open †Category
23+
open DaggerStr
24+
open IsDagger
25+
open NatTrans
26+
27+
†FUNCTOR : †Category (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) (ℓ-max (ℓ-max ℓC ℓC') ℓD')
28+
†FUNCTOR .cat = FullSubcategory (FUNCTOR (C .cat) (D .cat)) (Is†Functor C D)
29+
†FUNCTOR .dagstr ._† {x = F} {y = G} = NT† F G
30+
†FUNCTOR .dagstr .is-dag .†-invol n = makeNatTransPath (funExt λ x → D .†-invol (n ⟦ x ⟧))
31+
†FUNCTOR .dagstr .is-dag .†-id = makeNatTransPath (funExt λ x → D .†-id)
32+
†FUNCTOR .dagstr .is-dag .†-seq m n = makeNatTransPath (funExt λ x → D .†-seq (m ⟦ x ⟧) (n ⟦ x ⟧))

0 commit comments

Comments
 (0)