Library UniMath.CategoryTheory.DisplayedCats.Auxiliary
Auxiliary material needed for the development of bicategories, displayed categories, etc, but not specific to these.
Much of this material could probably be moved upstream to the CategoryTheory library and elsewhere
(some of it is already present there).
Contents:
Direct products of precategories should instead be imported from CategoryTheory.PrecategoryBinProduct.
The unit precategory should be imported from CategoryTheory.categories.StandardCategories.
- Notations and tactics
- Direct products of types
- Direct products of precategories
- Discrete precategories
Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.categories.StandardCategories.
Local Open Scope cat.
Local Open Scope type_scope.
Bind Scope cat with precategory_ob_mor.
Bind Scope cat with precategory_data.
Bind Scope cat with precategory.
Bind Scope cat with category.
Many binding sorts for this scope, following the many coercions on categories.
Lemmas of this subsection are either aliases or mild generalisations of existing functions from the UniMath libraries. They differ generally in using projections instead of destructing, making them apply and/or reduce in more situations. The aliases are included just to standardise local naming conventions.
Direct products of types.
Compare pathsdirprod.
Definition dirprod_paths {A B : UU} {p q : A × B}
: pr1 p = pr1 q → pr2 p = pr2 q → p = q.
Proof.
destruct p as [a b], q as [a' b']; apply pathsdirprod.
Defined.
: pr1 p = pr1 q → pr2 p = pr2 q → p = q.
Proof.
destruct p as [a b], q as [a' b']; apply pathsdirprod.
Defined.
Compare total2asstol.
Definition dirprod_assoc {C0 C1 C2 : UU}
: (C0 × (C1 × C2)) → ((C0 × C1) × C2).
Proof.
intros c. exact ((pr1 c ,, (pr1 (pr2 c))) ,, pr2 (pr2 c)).
Defined.
: (C0 × (C1 × C2)) → ((C0 × C1) × C2).
Proof.
intros c. exact ((pr1 c ,, (pr1 (pr2 c))) ,, pr2 (pr2 c)).
Defined.
Identical to dirprodf.
Definition dirprod_maps {A0 A1 B0 B1} (f0 : A0 → B0) (f1 : A1 → B1)
: A0 × A1 → B0 × B1.
Proof.
intros aa. exact (f0 (pr1 aa),, f1 (pr2 aa)).
Defined.
: A0 × A1 → B0 × B1.
Proof.
intros aa. exact (f0 (pr1 aa),, f1 (pr2 aa)).
Defined.
Compare prodtofuntoprod.
Definition dirprod_pair_maps {A B0 B1} (f0 : A → B0) (f1 : A → B1)
: A → B0 × B1.
Proof.
intros a; exact (f0 a,, f1 a).
Defined.
End Dirprod_utils.
: A → B0 × B1.
Proof.
intros a; exact (f0 a,, f1 a).
Defined.
End Dirprod_utils.
Direct products of precategories
Section category_products.
Definition unit_precategory : precategory.
Proof.
use tpair. use tpair.
∃ unit. intros; exact unit.
split; intros; constructor.
simpl; split; try split; intros; apply isProofIrrelevantUnit.
Defined.
Definition unit_functor C : functor C unit_precategory.
Proof.
use tpair. use tpair.
intros; exact tt.
intros F a b; apply identity.
split.
intros x; apply paths_refl.
intros x y z w v; apply paths_refl.
Defined.
Definition ob_as_functor {C : precategory} (c : C) : functor unit_precategory C.
Proof.
use tpair. use tpair.
intros; exact c.
intros F a b; apply identity.
split.
intros; constructor.
intros x y z w v; simpl. apply pathsinv0, id_left.
Defined.
Definition prod_precategory_ob_mor (C D : precategory) : precategory_ob_mor.
∃ (C × D).
intros a b. use (_ × _).
exact ((pr1 a) --> (pr1 b)). exact ((pr2 a) --> (pr2 b)).
Defined.
Definition prod_precategory_data (C D : precategory) : precategory_data.
∃ (prod_precategory_ob_mor C D); split.
split; apply identity.
intros a b c f g.
exact ((pr1 f · pr1 g) ,, (pr2 f · pr2 g)).
Defined.
Definition prod_precategory_is_precategory (C D : precategory)
: is_precategory (prod_precategory_data C D).
Proof.
split; try split; try split; intros.
apply dirprod_paths; simpl; apply id_left.
apply dirprod_paths; simpl; apply id_right.
apply dirprod_paths; simpl; apply assoc.
apply dirprod_paths; simpl; apply assoc'.
Defined.
Definition prod_precategory (C D : precategory) : precategory
:= (_ ,, prod_precategory_is_precategory C D).
Definition prod_precategory_homsets (C D : category)
: has_homsets (prod_precategory_data C D).
Proof.
intros x y. apply isaset_dirprod; apply homset_property.
Qed.
Definition prod_category (C D : category) : category
:= (prod_precategory C D,, prod_precategory_homsets C D).
Arguments prod_precategory (_ _)%cat.
Local Notation "C × D" := (prod_category C D) (at level 75, right associativity) : cat.
Definition prod_category_assoc_data (C0 C1 C2 : category)
: functor_data (C0 × (C1 × C2)) ((C0 × C1) × C2).
Proof.
∃ dirprod_assoc.
intros a b; apply dirprod_assoc.
Defined.
Definition prod_category_assoc (C0 C1 C2 : category)
: functor (C0 × (C1 × C2)) ((C0 × C1) × C2).
Proof.
∃ (prod_category_assoc_data _ _ _). split.
intros c. simpl; apply paths_refl.
intros c0 c1 c2 f g. simpl; apply paths_refl.
Defined.
Definition prod_functor_data {C0 C1 D0 D1 : category}
(F0 : functor C0 D0) (F1 : functor C1 D1)
: functor_data (C0 × C1) (D0 × D1).
Proof.
∃ (dirprod_maps F0 F1).
intros a b.
apply dirprod_maps; apply functor_on_morphisms.
Defined.
Definition prod_functor {C0 C1 D0 D1 : category}
(F0 : functor C0 D0) (F1 : functor C1 D1)
: functor (C0 × C1) (D0 × D1).
Proof.
∃ (prod_functor_data F0 F1); split.
intros c. apply dirprod_paths; apply functor_id.
intros c0 c1 c2 f g.
apply dirprod_paths; apply functor_comp.
Defined.
Definition pair_functor_data {C D0 D1 : category}
(F0 : functor C D0) (F1 : functor C D1)
: functor_data C (D0 × D1).
Proof.
∃ (dirprod_pair_maps F0 F1).
intros a b.
apply dirprod_pair_maps; apply functor_on_morphisms.
Defined.
Definition pair_functor {C D0 D1 : category}
(F0 : functor C D0) (F1 : functor C D1)
: functor C (D0 × D1).
Proof.
∃ (pair_functor_data F0 F1); split.
intros c. apply dirprod_paths; apply functor_id.
intros c0 c1 c2 f g.
apply dirprod_paths; apply functor_comp.
Defined.
End category_products.
Redeclare section notations to be available globally.
For use when proving a goal of the form transportf _ e' y = ?, where ? is an existential variable, and we want to “compute” in y, but expect the result of that computing to itself end with a transported term.
Currently named by analogy with monad binding operation (e.g. Haskell’s >>= ), to which it has a curious formal similarity.
Lemma transportf_bind {X : UU} {P : X → UU}
{x x' x'' : X} (e : x' = x) (e' : x = x'')
y y'
: y = transportf P e y' → transportf _ e' y = transportf _ (e @ e') y'.
Proof.
intro H; destruct e, e'; exact H.
Defined.
{x x' x'' : X} (e : x' = x) (e' : x = x'')
y y'
: y = transportf P e y' → transportf _ e' y = transportf _ (e @ e') y'.
Proof.
intro H; destruct e, e'; exact H.
Defined.
Composition of dependent paths.
NOTE 1: unfortunately, proofs using this seem to typecheck much more slowly than proofs inlining it as etrans plus transportf_bind explicitly — a shame, since proofs with this are much cleaner to read.
NOTE 2: unfortunately there’s a variance issue: this is currently backwards over paths in the base. However, this is unavoidable given that:
If transportf were derived from transportb, instead of vice versa, then we could use transportb on the RHS and this would look much nicer…
- we want the LHS of the input equalities to be an aribtrary term, *not* a transported term, so that proofs can work in “compute left-to-right” style;
- we want an arbitrary transportf on the RHS of the input equalities, so that this lemma can accept whatever the “computation” produces.
Lemma pathscomp0_dep {X : UU} {P : X → UU}
{x x' x'' : X} {e : x' = x} {e' : x'' = x'}
{y} {y'} {y''}
: (y = transportf P e y') → (y' = transportf _ e' y'')
→ y = transportf _ (e' @ e) y''.
Proof.
intros ee ee'.
etrans. apply ee.
apply transportf_bind, ee'.
Defined.
Tactic Notation "etrans_dep" := eapply @pathscomp0_dep.
{x x' x'' : X} {e : x' = x} {e' : x'' = x'}
{y} {y'} {y''}
: (y = transportf P e y') → (y' = transportf _ e' y'')
→ y = transportf _ (e' @ e) y''.
Proof.
intros ee ee'.
etrans. apply ee.
apply transportf_bind, ee'.
Defined.
Tactic Notation "etrans_dep" := eapply @pathscomp0_dep.
A couple of lemmas for giving weak equivalences between subtypes of types
Lemma weq_subtypes'
{X Y : UU} (w : X ≃ Y)
{S : X → UU} {T : Y → UU}
(HS : isPredicate S)
(HT : isPredicate T)
(HST : ∏ x : X, S x ↔ T (w x))
: (∑ x, S x) ≃ (∑ y, T y).
Proof.
apply (weqbandf w).
intros. apply weqiff.
- apply HST.
- apply HS.
- apply HT.
Defined.
Lemma weq_subtypes_iff
{X : UU} {S T : X → UU}
(HS : isPredicate S)
(HT : isPredicate T)
(HST : ∏ x, S x ↔ T x)
: (∑ x, S x) ≃ (∑ x, T x).
Proof.
apply (weq_subtypes' (idweq X)); assumption.
Defined.
End Miscellaneous.