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.
(** * Properties of pointwise functors *)
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import PathGroupoids Types.Forall HoTT.Tactics.Require Import Basics.Tactics.Set Universe Polymorphism.Set Implicit Arguments.Generalizable All Variables.Set Asymmetric Patterns.LocalOpen Scope category_scope.LocalOpen Scope functor_scope.Sectionparts.Context `{Funext}.(** We could do this all in a big [repeat match], but we split it up, to shave off about two seconds per proof. *)Local Ltacfunctor_pointwise_t helper_lem_match helper_lem :=
repeat (apply path_forall; intro);
rewrite !transport_forall_constant, !path_forall_2_beta;
path_natural_transformation;
repeatmatch goal with
| [ |- context[components_of (transport ?P?p?z)] ]
=> simplrewrite (@ap_transport _ P _ _ _ p (fun_ => components_of) z)
end;
rewrite !transport_forall_constant;
transport_to_ap;
repeatmatch goal with
| [ x : _ |- context[ap (funx3 : ?T => ?f (object_of x3 ?z))] ]
=> rewrite (@ap_compose' _ _ _ (funx3' : T => object_of x3') (funOx3 => f (Ox3 x)))
| [ x : _ |- context[ap (funx3 : ?T => ?f (object_of x3 ?z) ?w)] ]
=> rewrite (@ap_compose' _ _ _ (funx3' : T => object_of x3') (funOx3 => f (Ox3 x) w))
end;
repeatmatch goal with
| _ => done
| [ |- context[funF => @object_of ?C?D F] ]
=> progresschange (funF' => @object_of C D F') with (@object_of C D)
| [ |- context[helper_lem_match ?x] ]
=> rewrite (helper_lem x)
end.(** ** respects identity *)Sectionidentity_of.VariablesCD : PreCategory.
{HO : (funx : Functor C D => 1 o x o 1) = idmap &
transport
(funGO : Functor C D -> Functor C D =>
forallsd : Functor C D,
NaturalTransformation s d ->
NaturalTransformation (GO s) (GO d)) HO
(pointwise_morphism_of 11) =
(funsd : Functor C D => idmap)}
H: Funext C, D: PreCategory
transport
(funGO : Functor C D -> Functor C D =>
forallsd : Functor C D,
NaturalTransformation s d ->
NaturalTransformation (GO s) (GO d))
identity_of_helper (pointwise_morphism_of 11) =
(funsd : Functor C D => idmap)
H: Funext C, D: PreCategory
transport
(funGO : Functor C D -> Functor C D =>
forallsd : Functor C D,
NaturalTransformation s d ->
NaturalTransformation (GO s) (GO d))
(path_forall (funx : Functor C D => 1 o x o 1)
idmap
(funx : Functor C D =>
identity_of_helper_helper x))
(pointwise_morphism_of 11) =
(funsd : Functor C D => idmap)
abstract functor_pointwise_t
identity_of_helper_helper
identity_of_helper_helper_object_of.Defined.Endidentity_of.(** ** respects composition *)Sectioncomposition_of.VariablesCDC'D'C''D'' : PreCategory.VariableF' : Functor C' C''.VariableG : Functor D D'.VariableF : Functor C C'.VariableG' : Functor D' D''.
H: Funext C, D, C', D', C'', D'': PreCategory F': Functor C' C'' G: Functor D D' F: Functor C C' G': Functor D' D'' x: Functor C'' D
G' o G o x o (F' o F) = G' o (G o x o F') o F
H: Funext C, D, C', D', C'', D'': PreCategory F': Functor C' C'' G: Functor D D' F: Functor C C' G': Functor D' D'' x: Functor C'' D
H: Funext C, D, C', D', C'', D'': PreCategory F': Functor C' C'' G: Functor D D' F: Functor C C' G': Functor D' D''
(funx : Functor C'' D => G' o G o x o (F' o F)) =
(funx : Functor C'' D => G' o (G o x o F') o F)
H: Funext C, D, C', D', C'', D'': PreCategory F': Functor C' C'' G: Functor D D' F: Functor C C' G': Functor D' D''
(funx : Functor C'' D => G' o G o x o (F' o F)) =
(funx : Functor C'' D => G' o (G o x o F') o F)
H: Funext C, D, C', D', C'', D'': PreCategory F': Functor C' C'' G: Functor D D' F: Functor C C' G': Functor D' D'' x: Functor C'' D
G' o G o x o (F' o F) = G' o (G o x o F') o F
apply composition_of_helper_helper.Defined.
H: Funext C, D, C', D', C'', D'': PreCategory F': Functor C' C'' G: Functor D D' F: Functor C C' G': Functor D' D''
pointwise (F' o F) (G' o G) =
pointwise F G' o pointwise F' G
H: Funext C, D, C', D', C'', D'': PreCategory F': Functor C' C'' G: Functor D D' F: Functor C C' G': Functor D' D''
pointwise (F' o F) (G' o G) =
pointwise F G' o pointwise F' G
H: Funext C, D, C', D', C'', D'': PreCategory F': Functor C' C'' G: Functor D D' F: Functor C C' G': Functor D' D''
{HO
: (funx : Functor C'' D => G' o G o x o (F' o F)) =
(func : Functor C'' D => G' o (G o c o F') o F) &
transport
(funGO : Functor C'' D -> Functor C D'' =>
forallsd : Functor C'' D,
NaturalTransformation s d ->
NaturalTransformation (GO s) (GO d)) HO
(pointwise_morphism_of (F' o F) (G' o G)) =
(fun (sd : Functor C'' D)
(m : NaturalTransformation s d) =>
Core.whisker_r
(Core.whisker_l G'
(Core.whisker_r (Core.whisker_l G m) F')) F)}
H: Funext C, D, C', D', C'', D'': PreCategory F': Functor C' C'' G: Functor D D' F: Functor C C' G': Functor D' D''
transport
(funGO : Functor C'' D -> Functor C D'' =>
forallsd : Functor C'' D,
NaturalTransformation s d ->
NaturalTransformation (GO s) (GO d))
composition_of_helper
(pointwise_morphism_of (F' o F) (G' o G)) =
(fun (sd : Functor C'' D)
(m : NaturalTransformation s d) =>
Core.whisker_r
(Core.whisker_l G'
(Core.whisker_r (Core.whisker_l G m) F')) F)
H: Funext C, D, C', D', C'', D'': PreCategory F': Functor C' C'' G: Functor D D' F: Functor C C' G': Functor D' D''
transport
(funGO : Functor C'' D -> Functor C D'' =>
forallsd : Functor C'' D,
NaturalTransformation s d ->
NaturalTransformation (GO s) (GO d))
(path_forall
(funx : Functor C'' D => G' o G o x o (F' o F))
(funx : Functor C'' D => G' o (G o x o F') o F)
(funx : Functor C'' D =>
composition_of_helper_helper x))
(pointwise_morphism_of (F' o F) (G' o G)) =
(fun (sd : Functor C'' D)
(m : NaturalTransformation s d) =>
Core.whisker_r
(Core.whisker_l G'
(Core.whisker_r (Core.whisker_l G m) F')) F)