blob: 2c786ef0f084f5ada321fc9a167c76f5f8086475 (
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
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Monoidal using (MonoidalCategory)
open import Level using (Level)
module Functor.Forgetful.Instance.Monoid {o ℓ e : Level} (S : MonoidalCategory o ℓ e) where
open import Categories.Category.Construction.Monoids using (Monoids)
open import Categories.Functor using (Functor)
open import Categories.Object.Monoid using (Monoid; Monoid⇒)
open import Function using (id)
module S = MonoidalCategory S
open Monoid
open Monoid⇒
open S.Equiv using (refl)
open Functor
Forget : Functor (Monoids S.monoidal) S.U
Forget .F₀ = Carrier
Forget .F₁ = arr
Forget .identity = refl
Forget .homomorphism = refl
Forget .F-resp-≈ = id
module Forget = Functor Forget
|
