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
35
36
37
38
|
Require Import
MathClasses.theory.categories MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors.
Section constant_functor.
Context `{Category A} `{Category B}.
Context (b:B).
Notation F := (const b: A → B).
Global Instance: Fmap F := λ _ _ _, cat_id.
Global Instance: ∀ a a' : A, Setoid_Morphism (fmap F : (a ⟶ a') → (F a ⟶ F a')).
Proof.
intros; constructor; try apply _.
now intros ? ? ?.
Qed.
Global Instance ConstantFunctor : Functor F (λ _ _ _, cat_id).
Proof.
split; try apply _.
reflexivity.
intros; symmetry; compute; apply left_identity.
Qed.
End constant_functor.
Set Warnings "-unsupported-attributes". (* FIXME: remove when minimal Coq version is enough *)
#[global]
Typeclasses Transparent const.
Set Warnings "+unsupported-attributes".
Section constant_transformation.
Context `{Category A} `{Category J}.
Context {a a' : A}.
Global Instance constant_transformation {f : a⟶a'} : NaturalTransformation (const f : J → _).
Proof. intros ? ? ?. now rewrite left_identity, right_identity. Qed.
End constant_transformation.
|
