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.
(** * Functoriality of the comma category construction with projection functors *)
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Category.Prod Functor.Prod.Core.Require Import Category.Dual Functor.Dual.Require Import Functor.Composition.Core.Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors NatCategory.Require Import FunctorCategory.Core.Require Import Cat.Core.Require Import Functor.Paths.Require Comma.Core.Local Set Warnings Append "-notation-overridden". (* work around bug #5567, https://coq.inria.fr/bugs/show_bug.cgi?id=5567, notation-overridden,parsing should not trigger for only printing notations *)Import Comma.Core.Local Set Warnings Append "notation-overridden".Require Import Comma.InducedFunctors Comma.Projection.Require ProductLaws ExponentialLaws.Law1.Functors ExponentialLaws.Law4.Functors.Require Import Types.Forall PathGroupoids HoTT.Tactics.Set Universe Polymorphism.Set Implicit Arguments.Generalizable All Variables.Set Asymmetric Patterns.LocalOpen Scope category_scope.(** ** Functor from [(A โ C)แตแต ร (B โ C)] to [cat / (A ร B)] *)(** It sends [S : A โ C โ B : T] to the category [(S / T)] and its projection functor to [A ร B]. *)Sectioncomma.LocalOpen Scope type_scope.Context `{Funext}.VariableP : PreCategory -> Type.Context `{HF : forallCD, P C -> P D -> IsHSet (Functor C D)}.Local NotationCat := (@sub_pre_cat _ P HF).VariablesABC : PreCategory.HypothesisPAB : P (A * B).HypothesisP_comma : forall (S : Functor A C) (T : Functor B C),
P (S / T).LocalOpen Scope category_scope.LocalOpen Scope morphism_scope.
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) ST: (A -> C)^op * (B -> C)
Cat / !((A * B; PAB) : Cat)
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) ST: (A -> C)^op * (B -> C)
Cat / !((A * B; PAB) : Cat)
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) ST: (A -> C)^op * (B -> C)
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) s, d: (A -> C)^op * (B -> C) m: morphism ((A -> C)^op * (B -> C)) s d
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) s, d: (A -> C)^op * (B -> C) m: morphism ((A -> C)^op * (B -> C)) s d
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) s, d: (A -> C)^op * (B -> C) m: morphism ((A -> C)^op * (B -> C)) s d
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) s, d: (A -> C)^op * (B -> C) m: morphism ((A -> C)^op * (B -> C)) s d
!(A * B; PAB)
_1 (center
(morphism 1
(CommaCategory.b
(comma_category_projection_functor_object_of
s))
(CommaCategory.b
(comma_category_projection_functor_object_of
d))))
o CommaCategory.f
(comma_category_projection_functor_object_of s) =
CommaCategory.f
(comma_category_projection_functor_object_of d)
o Cat _1 (comma_category_induced_functor m)
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) s, d: (A -> C)^op * (B -> C) m: morphism ((A -> C)^op * (B -> C)) s d
(Identity.identity (A * B)
o comma_category_projection (Overture.fst s)
(Overture.snd s))%functor =
(comma_category_projection (Overture.fst d)
(Overture.snd d) o comma_category_induced_functor m)%functor
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) fst1: Functor A C snd1: Functor B C fst0: Functor A C snd0: Functor B C fst: Core.NaturalTransformation fst0 fst1 snd: Core.NaturalTransformation snd1 snd0
(Identity.identity (A * B)
o comma_category_projection fst1 snd1)%functor =
(comma_category_projection fst0 snd0
o comma_category_induced_functor (fst, snd)%core)%functor
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) x: (A -> C)^op * (B -> C)
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) x: (A -> C)^op * (B -> C)
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) x: (A -> C)^op * (B -> C)
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) x: (A -> C)^op * (B -> C)
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) x: (A -> C)^op * (B -> C)
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) s, d, d': (A -> C)^op * (B -> C) m: morphism ((A -> C)^op * (B -> C)) s d m': morphism ((A -> C)^op * (B -> C)) d d'
comma_category_projection_functor_morphism_of (m' o m) =
comma_category_projection_functor_morphism_of m'
o comma_category_projection_functor_morphism_of m
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) s, d, d': (A -> C)^op * (B -> C) m: morphism ((A -> C)^op * (B -> C)) s d m': morphism ((A -> C)^op * (B -> C)) d d'
comma_category_projection_functor_morphism_of (m' o m) =
comma_category_projection_functor_morphism_of m'
o comma_category_projection_functor_morphism_of m
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) s, d, d': (A -> C)^op * (B -> C) m: morphism ((A -> C)^op * (B -> C)) s d m': morphism ((A -> C)^op * (B -> C)) d d'
comma_category_induced_functor
(Core.compose (Overture.fst m) (Overture.fst m'),
Core.compose (Overture.snd m') (Overture.snd m)) =
(comma_category_induced_functor m'
o comma_category_induced_functor m)%functor
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) s, d, d': (A -> C)^op * (B -> C) m: morphism ((A -> C)^op * (B -> C)) s d m': morphism ((A -> C)^op * (B -> C)) d d'
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) s, d, d': (A -> C)^op * (B -> C) m: morphism ((A -> C)^op * (B -> C)) s d m': morphism ((A -> C)^op * (B -> C)) d d'
H: Funext P: (PreCategory -> Type)%type HF: forallCD : PreCategory,
(P C -> P D -> IsHSet (Functor C D))%type A, B, C: PreCategory PAB: P (A * B) P_comma: forall (S : Functor A C)
(T : Functor B C), P (S / T) s, d, d': (A -> C)^op * (B -> C) m: morphism ((A -> C)^op * (B -> C)) s d m': morphism ((A -> C)^op * (B -> C)) d d'