Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Add constant functors/natural transformation.

Reformatting by Robbert Krebbers.
  • Loading branch information...
commit 08cee955783a853f1d8e7be13b91bc9b45567e7e 1 parent 52be92a
@tomprince tomprince authored
Showing with 34 additions and 1 deletion.
  1. +1 −1  src/SConstruct
  2. +33 −0 src/functors/constant.v
View
2  src/SConstruct
@@ -5,7 +5,7 @@ env = DefaultEnvironment(ENV = os.environ, tools=['default', 'Coq'])
env['COQFLAGS'] = Rs = ' -R . MathClasses '
-Default('implementations', 'theory', 'categories', 'orders', 'varieties', 'misc')
+Default('implementations', 'theory', 'categories', 'orders', 'varieties', 'misc', 'functors')
env.CoqDoc(env.Dir('coqdoc'), vs, COQDOCFLAGS='-utf8 --toc -g --no-lib-name http://coq.inria.fr/library')
# Todo: Do "patch --backup $TARGET/coqdoc.css ../tools/coqdoc.css.diff", including the dependency on the .diff file.
View
33 src/functors/constant.v
@@ -0,0 +1,33 @@
+Require Import
+ theory.categories abstract_algebra 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.
+
+Typeclasses Transparent const.
+
+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.
Please sign in to comment.
Something went wrong with that request. Please try again.