open import Cat.Functor.Conservative
open import Cat.Functor.Naturality
open import Cat.Functor.Properties
open import Cat.Functor.Bifunctor
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 $F_{i} : C \to D .$ For the rest of this section we will fix a family of functors $F_{i} : C \to D .$

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 $F_{i} : C \to D$ is jointly faithful when: - For any $f, g : C (x, y),$ if $F_{i} (f) = F_{i} (g)$ for every $I,$ then $f = g$

  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 $\hat{C} (よ (A), -),$ indexed by objects of $A :$ this is a restatement of the coyoneda lemma.

Note that every functor $F : I \to [C, D]$ induces a family of functors via the mapping on objects: this family is jointly faithful precisely when $\hat{F} : C \to [I, D]$ is faithful.

  swap-faithful→jointly-faithful
    : (F : Functor K Cat[ C , D ])
    → is-faithful (Flip 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 (Flip F)
  jointly-faithful→swap-faithful F joint p = joint (λ i → p ηₚ i)

Jointly conservative functors🔗

A family of functors $F_{i} : C \to D$ is jointly conservative when: - For $f : C (x, y),$ if $F_{i} (f)$ is an iso for every $i,$ then $f$ 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 $F : I \to [C, D] .$

  swap-conservative→jointly-conservative
    : (F : Functor K Cat[ C , D ])
    → is-conservative (Flip F)
    → is-jointly-conservative (F .F₀)
  swap-conservative→jointly-conservative F reflect-iso isos =
    reflect-iso (invertible→invertibleⁿ (Flip F .F₁ _) isos)

  jointly-conservative→swap-conservative
    : (F : Functor K Cat[ C , D ])
    → is-jointly-conservative (F .F₀)
    → is-conservative (Flip 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 $F : I \to [C, D]$ is jointly full when the functor $\hat{F} : C \to [I, D]$ is full. Explicitly, $F$ is jointly full if a family of morphisms $g_{i} : D (F (i) (x), F (i) (y))$ that is natural in $i$ implies the mere existence of a $f : C (x, y)$ with $F_{i} (f) = g_{i} .$

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 (Flip 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 $F : I \to [C, D]$ is jointly fully faithful when the functor $\hat{F} : C \to [I, D]$ is fully faithful. Explicitly, $F$ is jointly fully faithful if there is an equivalence of natural transformations $\hat{F} (x) \to \hat{F} (y)$ and morphisms $C (x, y) .$

  is-jointly-fully-faithful : Functor K Cat[ C , D ] → Type _
  is-jointly-fully-faithful F = is-fully-faithful (Flip 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 ] (Flip F .F₁ f ≡ α))
      img-is-prop (f , p) (g , q) =
        Σ-prop-path (λ f → Nat-is-set (Flip F .F₁ f) α)
          (faithful (λ i → p ηₚ i ∙ sym (q ηₚ i)))