# Library Functor

Require Import Utf8.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Import JMeq.
Require Export Category.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.

# Functors

Section Functors.
Context `(C : @Category objC).
Context `(D : @Category objD).

Local Open Scope morphism_scope.

Quoting from the lecture notes for 18.705, Commutative Algebra:
A map of categories is known as a functor. Namely, given categories C and C', a (covariant) functor F : C C' is a rule that assigns to each object A of C an object F A of C' and to each map m : A B of C a map F m : F A F B of C' preserving composition and identity; that is,
• F (m' m) = (F m') (F m) for maps m : A B and m' : B C of C, and
• F (id A) = id (F A) for any object A of C, where id A is the identity morphism of A.
Record Functor :=
{
ObjectOf :> objCobjD;
MorphismOf : s d, C.(Morphism) s d
→ D.(Morphism) (ObjectOf s) (ObjectOf d);
FCompositionOf : s d d' (m1 : C.(Morphism) s d) (m2: C.(Morphism) d d'),
MorphismOf _ _ (m2 m1)
= (MorphismOf _ _ m2) (MorphismOf _ _ m1);
FIdentityOf : x, MorphismOf _ _ (Identity x)
= Identity (ObjectOf x)
}.
End Functors.

Delimit Scope functor_scope with functor.
Bind Scope functor_scope with Functor.

Create HintDb functor discriminated.

Arguments ObjectOf {objC C objD D} F c : simpl nomatch, rename.
Arguments MorphismOf {objC} [C] {objD} [D] F [s d] m : simpl nomatch, rename.

Arguments FCompositionOf [objC C objD D] F _ _ _ _ _ : rename.
Arguments FIdentityOf [objC C objD D] F _ : rename.

Hint Resolve @FCompositionOf @FIdentityOf : category.
Hint Resolve @FCompositionOf @FIdentityOf : functor.
Hint Rewrite @FIdentityOf : category.
Hint Rewrite @FIdentityOf : functor.

Section Functors_Equal.
Lemma Functor_Eq objC C objD D :
(F G : @Functor objC C objD D),
( x, ObjectOf F x = ObjectOf G x)
→ ( H : ( x, ObjectOf F x = ObjectOf G x),
s d m, match H s in (_ = y) return y ~> G d with
| eq_reflmatch H d in (_ = y) return F s ~> y with
| eq_reflMorphismOf F (s := s) (d := d) m
end
end
= MorphismOf G (s := s) (d := d) m)
→ F = G.
intros.
assert (H' : ObjectOf F = ObjectOf G)
by (apply functional_extensionality_dep; assumption);
pose F as F'; pose G as G';
destruct F, G;
simpl in *;
intuition.
assert (match H' in (_ = y) return s d : objC, (s ~> d) y s ~> y d with
| eq_reflMorphismOf F'
end
= MorphismOf G');
[ repeat (apply functional_extensionality_dep; intro); subst_body; simpl in ×
| ].
- rewrite <- (H0 H).
clear.
subst.
repeat match goal with
| [ |- appcontext[match ?f ?x with __ end] ] ⇒ generalize (f x); clear; intros
end.
repeat match goal with
| [ H : ?x = ?x |- _ ] ⇒ assert (H = eq_refl) by apply ProofIrrelevance.proof_irrelevance;
subst H
end.
reflexivity.
- subst_body.
simpl in ×.
repeat subst.
f_equal;
apply ProofIrrelevance.proof_irrelevance.
Qed.

Lemma Functor_Eq_by_JMeq objC C objD D :
(F G : @Functor objC C objD D),
( x, ObjectOf F x = ObjectOf G x)
→ (ObjectOf F = ObjectOf G
→ s d m, MorphismOf F (s := s) (d := d) m
== MorphismOf G (s := s) (d := d) m)
→ F = G.
intros.
assert (H' : ObjectOf F = ObjectOf G)
by (apply functional_extensionality_dep; assumption);
pose F as F'; pose G as G';
destruct F, G;
simpl in *;
intuition;
subst.
assert (MorphismOf F' = MorphismOf G');
subst F' G';
simpl;
repeat (apply functional_extensionality_dep; intro);
try solve [ apply JMeq_eq; intuition ];
simpl in ×.
subst;
f_equal; apply ProofIrrelevance.proof_irrelevance.
Qed.
End Functors_Equal.

Ltac functor_eq :=
simpl;
repeat intro;
simpl;
apply Functor_Eq;
intros;
subst_eq_refl_in_match;
try easy.

Section FunctorComposition.
Context `(B : @Category objB).
Context `(C : @Category objC).
Context `(D : @Category objD).
Context `(E : @Category objE).

Hint Rewrite @FCompositionOf : functor.

Definition ComposeFunctors (G : Functor D E) (F : Functor C D) : Functor C E.
refine (Build_Functor C E
(fun cG (F c))
(fun _ _ mG.(MorphismOf) (F.(MorphismOf) m))
_
_);
abstract (
intros; autorewrite with functor; reflexivity
).
Defined.
End FunctorComposition.

Infix "○" := (@ComposeFunctors _ _ _ _ _ _) : functor_scope.

Section IdentityFunctor.
Context `(C : @Category objC).

There is an identity functor. It does the obvious thing.
Definition IdentityFunctor : Functor C C.
refine {| ObjectOf := (fun x x);
MorphismOf := (fun _ _ x x)
|};
abstract t.
Defined.
End IdentityFunctor.

Section IdentityFunctorLemmas.
Context `(C : @Category objC).
Context `(D : @Category objD).

Lemma LeftIdentityFunctor (F : Functor D C)
: ComposeFunctors (IdentityFunctor _) F = F.
functor_eq.
Qed.

Lemma RightIdentityFunctor (F : Functor C D)
: ComposeFunctors F (IdentityFunctor _) = F.
functor_eq.
Qed.
End IdentityFunctorLemmas.

Hint Rewrite @LeftIdentityFunctor @RightIdentityFunctor : category.
Hint Immediate @LeftIdentityFunctor @RightIdentityFunctor : category.
Hint Rewrite @LeftIdentityFunctor @RightIdentityFunctor : functor.
Hint Immediate @LeftIdentityFunctor @RightIdentityFunctor : functor.

Section FunctorCompositionLemmas.
Context `(B : @Category objB).
Context `(C : @Category objC).
Context `(D : @Category objD).
Context `(E : @Category objE).

Lemma ComposeFunctorsAssociativity
(F : Functor B C)
(G : Functor C D)
(H : Functor D E)
: ComposeFunctors (ComposeFunctors H G) F
= ComposeFunctors H (ComposeFunctors G F).
functor_eq.
Qed.
End FunctorCompositionLemmas.

Hint Resolve @ComposeFunctorsAssociativity : category.
Hint Resolve @ComposeFunctorsAssociativity : functor.