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
|
Require Import
MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.categories.
Require MathClasses.categories.setoids.
Section contents.
Context `{Category C} (x: C).
Definition homFrom (y: C): setoids.Object := setoids.object (x ⟶ y).
Global Program Instance: Fmap homFrom := λ v w X, (X ◎): (x ⟶ v) → (x ⟶ w).
Next Obligation. constructor; apply _. Qed.
Global Instance: Functor homFrom _.
Proof.
constructor; try apply _.
constructor; try apply _.
repeat intro. simpl in *.
apply comp_proper; auto.
repeat intro.
simpl.
rewrite H1.
apply left_identity.
repeat intro.
simpl.
unfold compose.
rewrite H1.
symmetry.
apply comp_assoc.
Qed.
End contents.
|
