Library Modules.Prelims.lib

Some useful lemmas

Among other things:
  • associativity of horizontal composition of natural transformations horcomp_assoc
  • functors from Set preserves epis, assuming the axiom of choice preserves_to_HSET_isEpi
  • isomorphisms of categories transfer initiality
  • if there is a universal arrow from the initial object, then the target category has an initial object initial_universal_to_lift_initial
  • an adjunction whose unit is iso is a coreflection (i.e. the left adjoint is full and faithful) isounit_coreflection
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Epis.

Require Import UniMath.CategoryTheory.HorizontalComposition.

Require Import UniMath.CategoryTheory.categories.HSET.All.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.EpiFacts.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.catiso.

Require Import UniMath.CategoryTheory.Adjunctions.Core.

Local Notation "'SET'" := hset_category.
Local Notation "G □ F" := (functor_composite F G) (at level 35).
Local Notation "F ⟶ G" := (nat_trans F G) (at level 39).
Local Notation "α ∙∙ β" := (horcomp β α) (at level 20).

Tactic Notation "cpre" uconstr(x) := apply (cancel_precomposition x).
Tactic Notation "cpost" uconstr(x) := apply (cancel_postcomposition).

Open Scope cat.

Even true of equivalences
Lemma catiso_initial {C D : precategory} (w : catiso C D) (ini : Initial C) : Initial D.
Proof.
  set (obweq := catiso_ob_weq w).
  use mk_Initial.
  - exact (w ini).
  - use mk_isInitial.
    intro b.
    assert (h := homotweqinvweq obweq b).
    rewrite <- h.
    eapply iscontrweqb.
    + apply invweq.
      use catiso_fully_faithful_weq.
    + apply (pr2 ini).
Defined.

Lemma initial_universal_to_lift_initial {D C : precategory}
      (S : D ⟶ C)
      (c : Initial C)
      {r : D} {f : C ⟦ c, S r ⟧}
      (unif : is_universal_arrow_to S c r f) :
  isInitial _ r.
Proof.
  intro d.
  specialize (unif d (InitialArrow _ _)).
  use iscontrpair.
  - apply (iscontrpr1 unif).
  - intro g.
    cbn.
    apply limits.path_to_ctr.
    apply InitialArrowUnique.
Qed.

hom(X , Y) ~ hom(X , U F Y) ~ hom(F X , F Y)
Lemma isounit_coreflection {C : category}{D : category } {F} (isF : is_left_adjoint (A := C) (B := D) F) :
  is_iso (C := [C , C])
         (unit_from_left_adjoint isF
          : [C,C] ⟦ functor_identity _, F ∙ right_adjoint isF ⟧) -> fully_faithful F.
Proof.
  intro isounit.
  assert (homweq := (adjunction_homsetiso_weq (pr2 isF))).
  assert (isounitpw := is_functor_iso_pointwise_if_iso _ _ _ _ _ _ isounit).
  intros S1 S2.
  eapply isweqhomot; revgoals.
  - unshelve apply weqproperty.
    eapply weqcomp.
    + eapply iso_comp_left_weq.
      use (_ ,, isounitpw S2 ).
    + apply invweq.
      use hom_weq.
      apply (adjunction_homsetiso_weq (pr2 isF)).
  - intro ff.
    cbn.
    unfold φ_adj_inv; cbn.
    rewrite functor_comp.
    rewrite <- assoc.
    etrans;[ apply cancel_precomposition, triangle_id_left_ad|].
    apply id_right.
Defined.



common generalization to maponpaths and toforallpaths

Lemma changef_path {T1 T2 : UU} (f g : T1 → T2) (t1 t2 : T1) :
  f = g -> f t1 = f t2 -> g t1 = g t2.
Proof.
  induction 1; auto.
Qed.

Lemma changef_path_pw {T1 T2 : UU} (f g : T1 → T2) (t1 t2 : T1) :
  (∏ x, f x = g x) -> f t1 = f t2 -> g t1 = g t2.
Proof.
  intro eq.
  induction (eq t1); induction (eq t2); auto.
Qed.

Associativity of horizontal composition of natural transformations
Lemma horcomp_assoc
  : ∏ {B C D E : precategory} {H H' : functor B C}
      {F F' : functor C D} {G G' : functor D E}
      (a : nat_trans H H') (b : nat_trans F F') (c : nat_trans G G') x,
    ((c ∙∙ b) ∙∙ a) x = (c ∙∙( b ∙∙ a)) x.
Proof.
  intros.
  cbn.
  symmetry.
  rewrite functor_comp,assoc. apply idpath.
Qed.

Same as nat_trans_comp_pointwise, but with B = A · A'
Definition nat_trans_comp_pointwise' :
  ∏ (C : precategory) (C' : category) (F G H : ([C, C' , _ ])%Cat)
    (A : ([C, C' , _] ⟦ F, G ⟧)%Cat) (A' : ([C, C' , _] ⟦ G, H ⟧)%Cat) (a : C),
  ((A : nat_trans _ _) a · (A' : nat_trans _ _) a)%Cat = (A · A' : nat_trans _ _)%Cat a
  :=
  fun C C' F G H A A' => @nat_trans_comp_pointwise C C' (homset_property C') F G H A A' _ (idpath _).

Composition in Set category is the usual composition of function
Lemma comp_cat_comp {A B C:hSet} (f : A -> B) (g:B -> C) x :
  g (f x) = compose (C:= SET) f g x.
Proof.
  reflexivity.
Qed.