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