Merge pull request #420 from agda/dagger-functors

More dagger category theory

src/Categories/Category/Construction/DaggerFunctors.agda

@@ -0,0 +1,18 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.Category.Construction.DaggerFunctors where
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Construction.Functors using (Functors)
+open import Categories.Category.SubCategory using (FullSubCategory)
+open import Categories.Category.Dagger using (DaggerCategory)
+open import Categories.Functor.Dagger using (DaggerFunctor)
+
+open import Level using (Level; _⊔_)
+
+private
+  variable
+    o ℓ e o′ ℓ′ e′ : Level
+
+DaggerFunctors : DaggerCategory o ℓ e → DaggerCategory o′ ℓ′ e′ → Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)
+DaggerFunctors C D = FullSubCategory (Functors (DaggerCategory.C C) (DaggerCategory.C D)) {I = DaggerFunctor C D} DaggerFunctor.functor

src/Categories/Category/Dagger/Construction/DaggerFunctors.agda

@@ -0,0 +1,65 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.Category.Dagger.Construction.DaggerFunctors where
+
+open import Categories.Category.Dagger using (DaggerCategory)
+import Categories.Category.Construction.DaggerFunctors as cat
+open import Categories.Functor.Dagger using (DaggerFunctor)
+open import Categories.NaturalTransformation using (NaturalTransformation)
+
+open import Function.Base using (_$_)
+open import Level using (Level; _⊔_)
+
+private
+  variable
+    o ℓ e o′ ℓ′ e′ : Level
+
+DaggerFunctors : (C : DaggerCategory o ℓ e) (D : DaggerCategory o′ ℓ′ e′)
+               → DaggerCategory (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)
+DaggerFunctors C D = record
+  { C = cat.DaggerFunctors C D
+  ; hasDagger = record
+    { _† = λ {F} {G} α → dagger F G α
+    ; †-identity = †-identity
+    ; †-homomorphism = †-homomorphism
+    ; †-resp-≈ = λ α≈β → †-resp-≈ α≈β
+    ; †-involutive = λ α → †-involutive (NaturalTransformation.η α _)
+    }
+  }
+  where
+    open DaggerCategory C using () renaming (_† to _‡)
+    open DaggerCategory D hiding (C)
+    open HomReasoning
+
+    dagger : ∀ (F G : DaggerFunctor C D)
+           → NaturalTransformation (DaggerFunctor.functor F) (DaggerFunctor.functor G)
+           → NaturalTransformation (DaggerFunctor.functor G) (DaggerFunctor.functor F)
+    dagger F G α = record
+      { η = λ X → α.η X †
+      ; commute = λ {X Y} f → begin
+        α.η Y † ∘ G.₁ f       ≈˘⟨ †-involutive _ ⟩
+        (α.η Y † ∘ G.₁ f) † † ≈⟨ †-resp-≈ $ begin
+          (α.η Y † ∘ G.₁ f) †   ≈⟨ †-homomorphism ⟩
+          G.₁ f † ∘ α.η Y † †   ≈⟨ G.F-resp-† ⟩∘⟨ †-involutive _ ⟩
+          G.₁ (f ‡) ∘ α.η Y     ≈⟨ α.sym-commute (f ‡) ⟩
+          α.η X ∘ F.₁ (f ‡)     ≈˘⟨ †-involutive _ ⟩∘⟨ F.F-resp-† ⟩
+          α.η X † † ∘ F.₁ f †   ≈˘⟨ †-homomorphism ⟩
+          (F.₁ f ∘ α.η X †) †   ∎ ⟩
+        (F.₁ f ∘ α.η X †) † † ≈⟨ †-involutive _ ⟩
+        F.₁ f ∘ α.η X †       ∎
+      ; sym-commute = λ {X Y} f → begin
+        F.₁ f ∘ α.η X †       ≈˘⟨ †-involutive _ ⟩
+        (F.₁ f ∘ α.η X †) † † ≈⟨ †-resp-≈ $ begin
+          (F.₁ f ∘ α.η X †) †   ≈⟨ †-homomorphism ⟩
+          α.η X † † ∘ F.₁ f †   ≈⟨ †-involutive _ ⟩∘⟨ F.F-resp-† ⟩
+          α.η X ∘ F.₁ (f ‡)     ≈⟨ α.commute (f ‡) ⟩
+          G.₁ (f ‡) ∘ α.η Y     ≈˘⟨ G.F-resp-† ⟩∘⟨ †-involutive _ ⟩
+          G.₁ f † ∘ α.η Y † †   ≈˘⟨ †-homomorphism ⟩
+          (α.η Y † ∘ G.₁ f) †   ∎ ⟩
+        (α.η Y † ∘ G.₁ f) † † ≈⟨ †-involutive _ ⟩
+        α.η Y † ∘ G.₁ f       ∎
+      }
+      where
+        module F = DaggerFunctor F
+        module G = DaggerFunctor G
+        module α = NaturalTransformation α

src/Categories/Category/Instance/Cats.agda

@@ -9,7 +9,7 @@ open import Level
 open import Categories.Category using (Category)
 open import Categories.Functor using (Functor; id; _∘F_)
 open import Categories.NaturalTransformation.NaturalIsomorphism
-  using (NaturalIsomorphism; associator; unitorˡ; unitorʳ; unitor²; isEquivalence; _ⓘₕ_; sym)
+  using (NaturalIsomorphism; associator; sym-associator; unitorˡ; unitorʳ; unitor²; isEquivalence; _ⓘₕ_)
 private
   variable
     o ℓ e : Level
@@ -24,7 +24,7 @@ Cats o ℓ e = record
   ; id        = id
   ; _∘_       = _∘F_
   ; assoc     = λ {_ _ _ _ F G H} → associator F G H
-  ; sym-assoc = λ {_ _ _ _ F G H} → sym (associator F G H)
+  ; sym-assoc = λ {_ _ _ _ F G H} → sym-associator F G H
   ; identityˡ = unitorˡ
   ; identityʳ = unitorʳ
   ; identity² = unitor²

src/Categories/Category/Instance/DagCats.agda

@@ -0,0 +1,31 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.Category.Instance.DagCats where
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Dagger using (DaggerCategory)
+open import Categories.Functor.Dagger using (DaggerFunctor; id; _∘F†_)
+open import Categories.NaturalTransformation.NaturalIsomorphism
+
+open import Function.Base using (_on_)
+open import Level using (suc; _⊔_)
+
+DagCats : ∀ o ℓ e → Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
+DagCats o ℓ e = record
+  { Obj = DaggerCategory o ℓ e
+  ; _⇒_ = DaggerFunctor
+  ; _≈_ = NaturalIsomorphism on functor
+  ; id = id
+  ; _∘_ = _∘F†_
+  ; assoc = λ {_ _ _ _ F G H} → associator (functor F) (functor G) (functor H)
+  ; sym-assoc = λ {_ _ _ _ F G H} → sym-associator (functor F) (functor G) (functor H)
+  ; identityˡ = unitorˡ
+  ; identityʳ = unitorʳ
+  ; identity² = unitor²
+  ; equiv = record
+    { refl = refl
+    ; sym = sym
+    ; trans = trans
+    }
+  ; ∘-resp-≈ = _ⓘₕ_
+  } where open DaggerFunctor

src/Categories/Functor/Dagger.agda

@@ -0,0 +1,40 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.Functor.Dagger where
+
+open import Categories.Category.Dagger using (DaggerCategory)
+open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
+
+open import Level using (Level; _⊔_)
+
+private
+  variable
+    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ : Level
+
+record DaggerFunctor (C : DaggerCategory o ℓ e) (D : DaggerCategory o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
+  private
+    module C = DaggerCategory C
+    module D = DaggerCategory D
+  field
+    functor : Functor C.C D.C
+
+  open Functor functor public
+
+  field
+    F-resp-† : ∀ {X Y} {f : X C.⇒ Y} → F₁ f D.† D.≈ F₁ (f C.†)
+
+id : ∀ {C : DaggerCategory o ℓ e} → DaggerFunctor C C
+id {C = C} = record
+  { functor = idF
+  ; F-resp-† = DaggerCategory.Equiv.refl C
+  }
+
+_∘F†_ : ∀ {C : DaggerCategory o ℓ e} {D : DaggerCategory o′ ℓ′ e′} {E : DaggerCategory o″ ℓ″ e″}
+      → DaggerFunctor D E → DaggerFunctor C D → DaggerFunctor C E
+_∘F†_ {E = E} F G = record
+  { functor = F.functor ∘F G.functor
+  ; F-resp-† = DaggerCategory.Equiv.trans E F.F-resp-† (F.F-resp-≈ G.F-resp-†)
+  }
+  where
+    module F = DaggerFunctor F
+    module G = DaggerFunctor G