blob: b5d6f07b4383155bc30a16b34157eeec6515c69a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
{-# OPTIONS --without-K --safe #-}
open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
open import Categories.Functor.Monoidal.Symmetric using (module Lax)
open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
open FinitelyCocompleteCategory using () renaming (symmetricMonoidalCategory to smc)
open Lax using (SymmetricMonoidalFunctor)
module Cospan.Decorated
{o o′ ℓ ℓ′ e e′}
(C : FinitelyCocompleteCategory o ℓ e)
{D : SymmetricMonoidalCategory o′ ℓ′ e′}
(F : SymmetricMonoidalFunctor (smc C) D)
where
module C = FinitelyCocompleteCategory C
module D = SymmetricMonoidalCategory D
open import Category.Diagram.Cospan C using (Cospan)
open import Level using (_⊔_)
record DecoratedCospan (A B : C.Obj) : Set (o ⊔ ℓ ⊔ ℓ′) where
open SymmetricMonoidalFunctor F using (F₀)
field
cospan : Cospan A B
open Cospan cospan public
field
decoration : D.unit D.⇒ F₀ N
|
