Skip to content
Browse files

Bifunctor flip

  • Loading branch information...
1 parent a5b836a commit 2d151dc51543341e7e31a2e2af0304123705ab34 @djahandarie committed Jun 29, 2011
Showing with 19 additions and 3 deletions.
  1. +5 −1 Categories/Bifunctor.agda
  2. +14 −2 Categories/Product.agda
View
6 Categories/Bifunctor.agda
@@ -2,6 +2,7 @@
module Categories.Bifunctor where
open import Level
+open import Data.Product using (_,_; swap)
open import Categories.Category
@@ -15,4 +16,7 @@ overlap-× : ∀ {o ℓ e} {o′₁ ℓ′₁ e′₁} {o′₂ ℓ′₂ e′
overlap-× H F G = H ∘ (F ※ G)
reduce-× : {o ℓ e} {o′₁ ℓ′₁ e′₁} {o′₂ ℓ′₂ e′₂} {C : Category o ℓ e} {D₁ : Category o′₁ ℓ′₁ e′₁} {D₂ : Category o′₂ ℓ′₂ e′₂} (H : Bifunctor D₁ D₂ C) {o″₁ ℓ″₁ e″₁} {E₁ : Category o″₁ ℓ″₁ e″₁} (F : Functor E₁ D₁) {o″₂ ℓ″₂ e″₂} {E₂ : Category o″₂ ℓ″₂ e″₂} (G : Functor E₂ D₂) Bifunctor E₁ E₂ C
-reduce-× H F G = H ∘ (F ⁂ G)
+reduce-× H F G = H ∘ (F ⁂ G)
+
+flip-bifunctor : {o ℓ e} {o′ ℓ′ e′} {o′′ ℓ′′ e′′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {E : Category o′′ ℓ′′ e′′} Bifunctor C D E Bifunctor D C E
+flip-bifunctor {C = C} {D = D} {E = E} b = _∘_ b (Swap {C = C} {D = D})
View
16 Categories/Product.agda
@@ -2,7 +2,7 @@
module Categories.Product where
open import Level
-open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂; zip; map; <_,_>)
+open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂; zip; map; <_,_>; swap)
open import Categories.Category
@@ -80,4 +80,16 @@ _※ⁿ_ : ∀ {o ℓ e o′₁ ℓ′₁ e′₁} {C : Category o ℓ e} {D₁
α ※ⁿ β = record { η = < α.η , β.η >; commute = < α.commute , β.commute > }
where
module α = NaturalTransformation α
- module β = NaturalTransformation β
+ module β = NaturalTransformation β
+
+Swap : {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} Functor (Product D C) (Product C D)
+Swap {C = C} {D = D} = (record
+ { F₀ = swap
+ ; F₁ = swap
+ ; identity = C.Equiv.refl , D.Equiv.refl
+ ; homomorphism = C.Equiv.refl , D.Equiv.refl
+ ; F-resp-≡ = swap
+ })
+ where
+ module C = Category C
+ module D = Category D

0 comments on commit 2d151dc

Please sign in to comment.
Something went wrong with that request. Please try again.