open import Cat.Functor.Conservative
open import Cat.Functor.Naturality
open import Cat.Functor.Properties
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Reasoning

module Cat.Functor.Joint where

private variable
o h oβ hβ iβ : Level
C D K : Precategory o h
Idx : Type iβ
open Functor
open _=>_


# Families of functorsπ

This module generalizes properties of functors (fullness, faithfulness, conservativity, etc.) to families of functors For the rest of this section we will fix a family of functors

Swap : Functor K Cat[ C , D ] β Functor C Cat[ K , D ]
Swap F .Fβ c .Fβ k = F .Fβ k .Fβ c
Swap F .Fβ c .Fβ f = F .Fβ f .Ξ· c
Swap F .Fβ c .F-id = F .F-id Ξ·β c
Swap F .Fβ c .F-β f g = F .F-β f g Ξ·β c
Swap F .Fβ f .Ξ· k = F .Fβ k .Fβ f
Swap F .Fβ f .is-natural x y g = sym (F .Fβ g .is-natural _ _ f)
Swap F .F-id = ext Ξ» k β F .Fβ k .F-id
Swap F .F-β f g = ext Ξ» k β F .Fβ k .F-β f g

module _
{oc βc od βd}
{C : Precategory oc βc}
{D : Precategory od βd}
where
private
module C = Cat.Reasoning C
module D = Cat.Reasoning D


A family of functors is jointly faithful when: - For any if for every then

  is-jointly-faithful : (Idx β Functor C D) β Type _
is-jointly-faithful Fα΅’ =
β {x y} {f g : C.Hom x y} β (β i β Fα΅’ i .Fβ f β‘ Fα΅’ i .Fβ g) β f β‘ g


The canonical example of a family of jointly faithful functors are the family of hom-functors indexed by objects of this is a restatment of the coyoneda lemma.

Note that every functor induces a family of functors via the mapping on objects: this family is jointly faithful precisely when is faithful.

  swap-faithfulβjointly-faithful
: (F : Functor K Cat[ C , D ])
β is-faithful (Swap F)
β is-jointly-faithful (F .Fβ)
swap-faithfulβjointly-faithful F faithful p = faithful (ext p)

jointly-faithfulβswap-faithful
: (F : Functor K Cat[ C , D ])
β is-jointly-faithful (F .Fβ)
β is-faithful (Swap F)
jointly-faithfulβswap-faithful F joint p = joint (Ξ» i β p Ξ·β i)


## Jointly conservative functorsπ

A family of functors is jointly conservative when: - For if is an iso for every then is an iso.

  is-jointly-conservative : (Idx β Functor C D) β Type _
is-jointly-conservative Fα΅’ =
β {x y} {f : C.Hom x y} β (β i β D.is-invertible (Fα΅’ i .Fβ f)) β C.is-invertible f


We can also rephrase joint-conservativity as a property of a diagram

  swap-conservativeβjointly-conservative
: (F : Functor K Cat[ C , D ])
β is-conservative (Swap F)
β is-jointly-conservative (F .Fβ)
swap-conservativeβjointly-conservative F reflect-iso isos =
reflect-iso (invertibleβinvertibleβΏ (Swap F .Fβ _) isos)

jointly-conservativeβswap-conservative
: (F : Functor K Cat[ C , D ])
β is-jointly-conservative (F .Fβ)
β is-conservative (Swap F)
jointly-conservativeβswap-conservative F reflect-iso isos =
reflect-iso (Ξ» i β is-invertibleβΏβis-invertible isos i)


## Jointly full functorsπ

A diagram of functors is jointly full when the functor is full. Explicitly, is jointly full if a family of morphisms that is natural in implies the mere existence of a with

Note that joint fullness must be a property of a diagram of functors, due to the naturality constraint. This

module _
{oc βc od βd ok βk}
{C : Precategory oc βc}
{D : Precategory od βd}
{K : Precategory ok βk}
where
private
module C = Cat.Reasoning C
module D = Cat.Reasoning D
module K = Cat.Reasoning K

  is-jointly-full : Functor K Cat[ C , D ] β Type _
is-jointly-full F = is-full (Swap F)

jointly-full-fibre
: β {x y}
β (F : Functor K Cat[ C , D ])
β is-jointly-full F
β (gα΅’ : β i β D.Hom (F .Fβ i .Fβ x) (F .Fβ i .Fβ y))
β (β {i j} (f : K.Hom i j) β gα΅’ j D.β F .Fβ f .Ξ· x β‘ F .Fβ f .Ξ· y D.β gα΅’ i)
β β[ f β C.Hom x y ] (β i β F .Fβ i .Fβ f β‘ gα΅’ i)
jointly-full-fibre F joint-full gα΅’ gα΅’-nat =
β₯-β₯-map (Ξ£-mapβ Ξ» p i β p Ξ·β i) (joint-full (NT gα΅’ Ξ» i j f β gα΅’-nat f))


## Jointly fully faithful functorsπ

A diagram of functors is jointly fully faithful when the functor is fully faithful. Explicitly, is jointly faully faithful if there is an equivalence of natural transformations and morphisms

  is-jointly-fully-faithful : Functor K Cat[ C , D ] β Type _
is-jointly-fully-faithful F = is-fully-faithful (Swap F)


If a diagram of functors is jointly fully and jointly faithful, then it is jointly fully faithful.

  jointly-full+jointly-faithfulβjointly-ff
: (F : Functor K Cat[ C , D ])
β is-jointly-full F
β is-jointly-faithful (F .Fβ)
β is-jointly-fully-faithful F
jointly-full+jointly-faithfulβjointly-ff F full faithful {x} {y} .is-eqv Ξ± =
is-propββis-contr img-is-prop $β₯-β₯-elim (Ξ» _ β img-is-prop) (Ξ£-mapβ (Ξ» p β ext p))$
jointly-full-fibre F full (Ξ» i β Ξ± .Ξ· i) (Ξ» f β Ξ± .is-natural _ _ f)
where
img-is-prop : is-prop (Ξ£[ f β C.Hom x y ] (Swap F .Fβ f β‘ Ξ±))
img-is-prop (f , p) (g , q) =
Ξ£-prop-path (Ξ» f β Nat-is-set (Swap F .Fβ f) Ξ±)
(faithful (Ξ» i β p Ξ·β i β sym (q Ξ·β i)))