Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โCtrl+โ to navigate, Ctrl+๐ฑ๏ธ to focus. On Mac, use โ instead of Ctrl.
(** * Definition of a [PreCategory] *)
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Set Universe Polymorphism.Set Implicit Arguments.Generalizable All Variables.Set Asymmetric Patterns.Declare Scope morphism_scope.Declare Scope category_scope.Declare Scope object_scope.Delimit Scope morphism_scope with morphism.Delimit Scope category_scope with category.Delimit Scope object_scope with object.LocalOpen Scope morphism_scope.(** Quoting the HoTT Book: *)(** Definition 9.1.1. A precategory [A] consists of the following. (i) A type [Aโ] of objects. We write [a : A] for [a : Aโ]. (ii) For each [a, b : A], a set [hom_A(a, b)] of arrows or morphisms. (iii) For each [a : A], a morphism [1โ : hom_A(a, a)]. (iv) For each [a, b, c : A], a function [hom_A(b, c) โ hom_A(a, b) โ hom_A(a, c)] denoted infix by [g โฆ f โฆ g โ f] , or sometimes simply by [g f]. (v) For each [a, b : A] and [f : hom_A(a, b)], we have [f = 1_b โ f] and [f = f โ 1โ]. (vi) For each [a, b, c, d : A] and [f : hom_A(a, b)], [g : hom_A(b, c)], [h : hom_A(c,d)], we have [h โ (g โ f) = (h โ g) โ f]. *)(** In addition to these laws, we ask for a few redundant laws to give us more judgmental equalities. For example, since [(p^)^ โข p] for paths [p], we ask for the symmetrized version of the associativity law, so we can swap them when we take the dual. *)RecordPreCategory :=
Build_PreCategory' {
object :> Type;
morphism : object -> object -> Type;
identity : forallx, morphism x x;
compose : forallsdd',
morphism d d'
-> morphism s d
-> morphism s d'
where"f 'o' g" := (compose f g);
associativity : forallx1x2x3x4
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
(m3 o m2) o m1 = m3 o (m2 o m1);
(** Ask for the symmetrized version of [associativity], so that [(Cแตแต)แตแต] and [C] are equal without [Funext] *)
associativity_sym : forallx1x2x3x4
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
m3 o (m2 o m1) = (m3 o m2) o m1;
left_identity : forallab (f : morphism a b), identity b o f = f;
right_identity : forallab (f : morphism a b), f o identity a = f;
(** Ask for the double-identity version so that [InitialTerminalCategory.Functors.from_terminal Cแตแต X] and [(InitialTerminalCategory.Functors.from_terminal C X)แตแต] are convertible. *)
identity_identity : forallx, identity x o identity x = identity x;
trunc_morphism : forallsd, IsHSet (morphism s d)
}.Bind Scope category_scope with PreCategory.Bind Scope object_scope with object.Bind Scope morphism_scope with morphism.(** We want eta-expanded primitive projections to [simpl] away. *)Arguments object !C%category / : rename.Arguments morphism !C%category / s d : rename.Arguments identity {!C%category} / x%object : rename.Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename.LocalInfix"o" := compose : morphism_scope.(** Perhaps we should consider making this notation more global. *)(** Perhaps we should pre-reserve all of the notations. *)LocalNotation"x --> y" := (morphism _ x y) : type_scope.LocalNotation"1" := (identity _) : morphism_scope.(** Define a convenience wrapper for building a precategory without specifying the redundant proofs. *)DefinitionBuild_PreCategoryobjectmorphismidentitycomposeassociativityleft_identityright_identity
:= @Build_PreCategory'
object
morphism
identity
compose
associativity
(fun_______ => symmetry _ _ (associativity _ _ _ _ _ _ _))
left_identity
right_identity
(fun_ => left_identity _ _ _).Global Existing Instancetrunc_morphism.(** create a hint db for all category theory things *)Create HintDb category discriminated.(** create a hint db for morphisms in categories *)Create HintDb morphism discriminated.#[export]
Hint Resolve left_identity right_identity associativity : category morphism.#[export]
Hint Rewrite left_identity right_identity : category.#[export]
Hint Rewrite left_identity right_identity : morphism.(** ** Simple laws about the identity morphism *)Sectionidentity_unique.VariableC : PreCategory.(** The identity morphism is unique. *)
C: PreCategory id0, id1: forallx : C, x --> x id1_left: forall (sd : C) (m : s --> d),
id1 d o m = m id0_right: forall (sd : C) (m : s --> d),
m o id0 s = m
id0 == id1
C: PreCategory id0, id1: forallx : C, x --> x id1_left: forall (sd : C) (m : s --> d),
id1 d o m = m id0_right: forall (sd : C) (m : s --> d),
m o id0 s = m
id0 == id1
C: PreCategory id0, id1: forallx : C, x --> x id1_left: forall (sd : C) (m : s --> d),
id1 d o m = m id0_right: forall (sd : C) (m : s --> d),
m o id0 s = m x: C
id0 x = id1 x
etransitivity;
[ symmetry; apply id1_left
| apply id0_right ].Qed.(** Anything equal to the identity acts like it. This is obvious, but useful as a helper lemma for automation. *)Definitionconcat_left_identitysd (m : morphism C s d) i
: i = 1 -> i o m = m
:= funH => (ap10 (ap _ H) _ @ left_identity _ _ _ m)%path.Definitionconcat_right_identitysd (m : morphism C s d) i
: i = 1 -> m o i = m
:= funH => (ap _ H @ right_identity _ _ _ m)%path.Endidentity_unique.(** Make a separate module for Notations, which can be exported/imported separately. *)ModuleExport CategoryCoreNotations.Infix"o" := compose : morphism_scope.(** Perhaps we should consider making this notation more global. *)(** Perhaps we should pre-reserve all of the notations. *)LocalNotation"x --> y" := (@morphism _ x y) : type_scope.LocalNotation"x --> y" := (morphism _ x y) : type_scope.Notation"1" := (identity _) : morphism_scope.EndCategoryCoreNotations.(** We have a tactic for trying to run a tactic after associating morphisms either all the way to the left, or all the way to the right *)Tactic Notation"try_associativity_quick" tactic(tac) :=
first [ rewrite <- ?associativity; tac
| rewrite -> ?associativity; tac ].