Documentation

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory.

Local Open Scope cat.

Definition indexed_functor_data
           {C : category}
           (Φ Ψ : indexed_cat C)
  : UU
  := ∑ (τ ₀ : ∏ (x : C ), Φ x ⟶ Ψ x ),
     ∏ (x y : C)
       (f : x --> y ),
     nat_z_iso
       (τ ₀ x ∙ (Ψ $ f ))
       ((Φ $ f ) ∙ τ ₀ y).

Definition make_indexed_functor_data
           {C : category}
           {Φ Ψ : indexed_cat C}
           (τ ₀ : ∏ (x : C ), Φ x ⟶ Ψ x)
           (τ ₁ : ∏ (x y : C)
                   (f : x --> y ),
                 nat_z_iso
                   (τ ₀ x ∙ (Ψ $ f ))
                   ((Φ $ f ) ∙ τ ₀ y))
  : indexed_functor_data Φ Ψ
  := τ ₀ ,, τ ₁.

Definition indexed_functor_to_functor
           {C : category}
           {Φ Ψ : indexed_cat C}
           (τ : indexed_functor_data Φ Ψ)
           (x : C)
  : Φ x ⟶ Ψ x
  := pr1 τ x.

Coercion indexed_functor_to_functor : indexed_functor_data >-> Funclass.

Definition indexed_functor_natural
           {C : category}
           {Φ Ψ : indexed_cat C}
           (τ : indexed_functor_data Φ Ψ)
           {x y : C}
           (f : x --> y)
  : nat_z_iso
      (τ x ∙ (Ψ $ f ))
      ((Φ $ f ) ∙ τ y)
  := pr2 τ x y f.

Definition indexed_functor_natural_z_iso
           {C : category}
           {Φ Ψ : indexed_cat C}
           (τ : indexed_functor_data Φ Ψ)
           {x y : C}
           (f : x --> y)
           (xx : Φ x)
  : z_iso ((Ψ $ f ) (τ x xx )) (τ y ((Φ $ f ) xx))
  := nat_z_iso_pointwise_z_iso
       (indexed_functor_natural τ f)
       xx.

Definition indexed_functor_laws
           {C : category}
           {Φ Ψ : indexed_cat C}
           (τ : indexed_functor_data Φ Ψ)
  : UU
  := (∏ (x : C)
        (xx : Φ x ),
      indexed_cat_id Ψ x (τ x xx)
      · indexed_functor_natural τ (identity x) xx
      =
      # (τ x ) (indexed_cat_id Φ x xx ))
     ×
     (∏ (x y z : C)
        (f : x --> y)
        (g : y --> z)
        (xx : Φ x ),
      indexed_cat_comp Ψ f g (τ x xx)
      · indexed_functor_natural τ (f · g) xx
      =
      # (Ψ $ g ) (indexed_functor_natural τ f xx )
      · (indexed_functor_natural τ g) ((Φ $ f ) xx)
      · # (τ z ) (indexed_cat_comp Φ f g xx )).

Definition indexed_functor
           {C : category}
           (Φ Ψ : indexed_cat C)
  : UU
  := ∑ (τ : indexed_functor_data Φ Ψ ), indexed_functor_laws τ.

Definition make_indexed_functor
           {C : category}
           {Φ Ψ : indexed_cat C}
           (τ : indexed_functor_data Φ Ψ)
           (H τ : indexed_functor_laws τ)
  : indexed_functor Φ Ψ
  := τ ,, H τ.

Coercion indexed_functor_to_data
         {C : category}
         {Φ Ψ : indexed_cat C}
         (τ : indexed_functor Φ Ψ)
  : indexed_functor_data Φ Ψ
  := pr1 τ.

Section IndexedFunctorLaws.
  Context {C : category}
          {Φ Ψ : indexed_cat C}
          (τ : indexed_functor Φ Ψ).

  Proposition indexed_functor_id
              {x : C}
              (xx : Φ x)
    : indexed_cat_id Ψ x (τ x xx)
      · indexed_functor_natural τ (identity x) xx
      =
      # (τ x ) (indexed_cat_id Φ x xx ).
  Show proof.

exact (pr12 τ x xx).

  Proposition indexed_functor_comp
              {x y z : C}
              (f : x --> y)
              (g : y --> z)
              (xx : Φ x)
    : indexed_cat_comp Ψ f g (τ x xx)
      · indexed_functor_natural τ (f · g) xx
      =
      # (Ψ $ g ) (indexed_functor_natural τ f xx )
      · (indexed_functor_natural τ g) ((Φ $ f ) xx)
      · # (τ z ) (indexed_cat_comp Φ f g xx ).
  Show proof.

exact (pr22 τ x y z f g xx).

End IndexedFunctorLaws.

Library UniMath.CategoryTheory.IndexedCategories.IndexedFunctor