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.
(** * Morphisms in a functor category *)
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Basics.Tactics.Set Universe Polymorphism.Set Implicit Arguments.Generalizable All Variables.Set Asymmetric Patterns.LocalOpen Scope path_scope.LocalOpen Scope category_scope.LocalOpen Scope morphism_scope.(** ** Natural Isomorphisms - isomorphisms in a functor category *)DefinitionNaturalIsomorphism `{Funext} (C D : PreCategory) F G :=
@Isomorphic (C -> D) F G.Arguments NaturalIsomorphism {_} [C D] F G / .Global Instancereflexive_natural_isomorphism `{Funext} C D
: Reflexive (@NaturalIsomorphism _ C D) | 0
:= _.Coercionnatural_transformation_of_natural_isomorphism `{Funext} C D F G
(T : @NaturalIsomorphism _ C D F G)
: NaturalTransformation F G
:= T : morphism _ _ _.LocalInfix"<~=~>" := NaturalIsomorphism : natural_transformation_scope.(** ** If [T] is an isomorphism, then so is [T x] for any [x] *)
H: Funext C, D: PreCategory F, G: C -> D T: morphism (C -> D) F G H0: IsIsomorphism T x: C
IsIsomorphism (T x)
H: Funext C, D: PreCategory F, G: C -> D T: morphism (C -> D) F G H0: IsIsomorphism T x: C
IsIsomorphism (T x)
H: Funext C, D: PreCategory F, G: C -> D T: morphism (C -> D) F G H0: IsIsomorphism T x: C
T^-1 x o T x = 1
H: Funext C, D: PreCategory F, G: C -> D T: morphism (C -> D) F G H0: IsIsomorphism T x: C
T x o T^-1 x = 1
H: Funext C, D: PreCategory F, G: C -> D T: morphism (C -> D) F G H0: IsIsomorphism T x: C
T^-1 x o T x = 1
exact (apD10 (ap components_of left_inverse) x).
H: Funext C, D: PreCategory F, G: C -> D T: morphism (C -> D) F G H0: IsIsomorphism T x: C
T x o T^-1 x = 1
exact (apD10 (ap components_of right_inverse) x).Defined.#[export]
Hint Immediate isisomorphism_components_of : typeclass_instances.(** When one of the functors is the identity functor, we fail to match correctly, because [apply] is stupid. So we do its work for it. *)#[export]
Hint Extern10 (@IsIsomorphism _ _ _ (@components_of ?C?D?F?G?T?x))
=> apply (funH' => @isisomorphism_components_of _ C D F G T H' x)
: typeclass_instances.
C, D: PreCategory F, G: Functor C D T: NaturalTransformation F G H: forallx : C, IsIsomorphism (T x)
NaturalTransformation G F
C, D: PreCategory F, G: Functor C D T: NaturalTransformation F G H: forallx : C, IsIsomorphism (T x)
NaturalTransformation G F
exists (funx => (T x)^-1);
abstract (
intros;
iso_move_inverse;
first [ apply commutes
| symmetry; apply commutes ]
).Defined.(** ** If [T x] is an isomorphism for all [x], then so is [T] *)
H: Funext C, D: PreCategory F, G: Functor C D T: NaturalTransformation F G H0: forallx : C, IsIsomorphism (T x)
IsIsomorphism T
H: Funext C, D: PreCategory F, G: Functor C D T: NaturalTransformation F G H0: forallx : C, IsIsomorphism (T x)
IsIsomorphism T
exists (inverse_);
abstract (
path_natural_transformation;
first [ apply left_inverse
| apply right_inverse ]
).Defined.#[export]
Hint Immediate isisomorphism_natural_transformation : typeclass_instances.(** ** Variant of [idtoiso] for natural transformations *)Sectionidtoiso.Context `{Funext}.VariablesCD : PreCategory.