Library UniMath.CategoryTheory.Core.TransportMorphisms

Lemmas on transport of morphisms

Require Import UniMath.Foundations.PartA.
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.

Local Open Scope cat.

Transport source and target of a morphism

Lemma transport_target_postcompose {C : precategory} {x y z w : ob C} (f : x --> y) (g : y --> z)
(e : z = w) :
transportf (precategory_morphisms x) e (f · g) = f · transportf (precategory_morphisms y) e g.
Show proof.

induction e. apply idpath.

Lemma transport_source_precompose {C : precategory} {x y z w : ob C} (f : x --> y) (g : y --> z)
      (e : x = w) :
  transportf (λ x' : ob C , precategory_morphisms x' z) e (f · g) =
  transportf (λ x' : ob C , precategory_morphisms x' y) e f · g.
Show proof.

induction e. apply idpath.

Lemma transport_compose {C : precategory} {x y z w : ob C} (f : x --> y) (g : z --> w) (e : y = z) :
transportf (precategory_morphisms x) e f · g =
f · transportf (λ x' : ob C , precategory_morphisms x' w) (! e) g.
Show proof.

induction e. apply idpath.

Lemma transport_compose' {C : precategory} {x y z w : ob C} (f : x --> y) (g : y --> z) (e : y = w) :
(transportf (precategory_morphisms x) e f )
· (transportf (λ x' : ob C , precategory_morphisms x' z) e g ) = f · g.
Show proof.

induction e. apply idpath.

Lemma transport_target_path {C : precategory} {x y z : ob C} (f g : x --> y) (e : y = z) :
transportf (precategory_morphisms x) e f = transportf (precategory_morphisms x) e g -> f = g.
Show proof.

induction e. intros H. apply H.

Lemma transport_source_path {C : precategory} {x y z : ob C} (f g : y --> z) (e : y = x) :
transportf (λ x' : ob C , precategory_morphisms x' z) e f =
transportf (λ x' : ob C , precategory_morphisms x' z) e g -> f = g.
Show proof.

induction e. intros H. apply H.

Lemma transport_source_target {X : UU} {C : precategory} {x y : X} (P : ∏ (x' : X ), ob C)
      (P' : ∏ (x' : X ), ob C) (f : ∏ (x' : X ), (P x') --> (P' x')) (e : x = y) :
  transportf (λ (x' : X ), (P x') --> (P' x')) e (f x) =
  transportf (λ (x' : X ), precategory_morphisms (P x') (P' y)) e
             (transportf (precategory_morphisms (P x)) (maponpaths P' e) (f x)).
Show proof.

rewrite <- functtransportf. unfold pathsinv0. unfold paths_rect. induction e.
apply idpath.

Lemma transport_target_source {X : UU} {C : precategory} {x y : X} (P : ∏ (x' : X ), ob C)
      (P' : ∏ (x' : X ), ob C) (f : ∏ (x' : X ), (P x') --> (P' x')) (e : x = y) :
  transportf (λ (x' : X ), (P x') --> (P' x')) e (f x) =
  transportf (precategory_morphisms (P y)) (maponpaths P' e)
             (transportf (λ (x' : X ), precategory_morphisms (P x') (P' x)) e (f x)).
Show proof.

rewrite <- functtransportf. unfold pathsinv0. unfold paths_rect. induction e.
apply idpath.

Lemma transport_source_target_comm {C : precategory} {x y x' y' : ob C} (f : x --> y) (e1 : x = x')
      (e2 : y = y') :
  transportf (λ (x'' : ob C ), precategory_morphisms x'' y') e1
             (transportf (precategory_morphisms x) e2 f) =
  transportf (precategory_morphisms x') e2
             (transportf (λ (x'' : ob C ), precategory_morphisms x'' y) e1 f).
Show proof.

induction e1. induction e2. apply idpath.

Transport a morphism using funextfun

Definition transport_source_funextfun {X : UU} {C : precategory_ob_mor} (F F' : X -> ob C)
           (H : ∏ (x : X ), F x = F' x) {x : X} (c : ob C) (f : F x --> c) :
  transportf (λ x0 : X → C , x0 x --> c) (funextfun F F' H) f =
  transportf (λ x0 : C , x0 --> c) (H x) f.
Show proof.

exact (@transportf_funextfun X (ob C) (λ x0 : C, x0 --> c) F F' H x f).

Definition transport_target_funextfun {X : UU} {C : precategory_ob_mor} (F F' : X -> ob C)
           (H : ∏ (x : X ), F x = F' x) {x : X} {c : ob C} (f : c --> F x) :
  transportf (λ x0 : X → C , c --> x0 x) (funextfun F F' H) f =
  transportf (λ x0 : C , c --> x0) (H x) f.
Show proof.

use transportf_funextfun.

Lemma transport_mor_funextfun {X : UU} {C : precategory_ob_mor} (F F' : X -> ob C)
           (H : ∏ (x : X ), F x = F' x) {x1 x2 : X} (f : F x1 --> F x2) :
  transportf (λ x : X → C , x x1 --> x x2) (funextfun F F' H) f =
  transportf (λ x : X → C , F' x1 --> x x2)
             (funextfun F F' (λ x : X , H x))
             (transportf (λ x : X → C , x x1 --> F x2)
                         ((funextfun F F' (λ x : X , H x))) f).
Show proof.

induction (funextfun F F' (λ x : X, H x)).
apply idpath.

Transport of is_iso

Lemma transport_target_is_iso {C : precategory} {x y z : ob C} (f : x --> y) (H : is_iso f)
(e : y = z) : is_iso (transportf (precategory_morphisms x) e f).
Show proof.

induction e. apply H.

Lemma transport_source_is_iso {C : precategory} {x y z : ob C} (f : x --> y) (H : is_iso f)
(e : x = z) : is_iso (transportf (λ x' : ob C , precategory_morphisms x' y) e f).
Show proof.

induction e. apply H.

Induced precategories

Definition induced_precategory (M : precategory) {X:Type} (j : X -> ob M) : precategory.
Show proof.

  use tpair.
  - use tpair.
    + exact (X,, λ a b , precategory_morphisms (j a) (j b)).
    + split;cbn.
      * exact (λ c , identity (j c)).
      * exact (λ a b c , @compose M (j a) (j b) (j c)).
  - repeat split; cbn.
    + exact (λ a b , @id_left M (j a) (j b)).
    + exact (λ a b , @id_right M (j a) (j b)).
    + exact (λ a b c d , @assoc M (j a) (j b) (j c) (j d)).
    + exact (λ a b c d , @assoc' M (j a) (j b) (j c) (j d)).

Lemma has_homsets_induced_precategory (M : category) {X:Type} (j : X -> ob M)
: has_homsets (induced_precategory M j).
Show proof.

intros a b.
apply M.

Definition induced_category (M : category) {X:Type} (j : X -> ob M) : category
:= make_category _ (has_homsets_induced_precategory M j).