Presheaf categories are locally cartesian closed.

[finegeometer]

Hi!

I just spent a while proving that presheaf categories are locally cartesian closed. I feel this ought be in the library somewhere, so I'm sharing the code. Feel free to use, modify, or ignore it, at your discretion.

The code is somewhat long, since I struggled to transfer the cartesian closed structure across the equivalence of categories from Cat.Instances.Slice.Presheaf. Is there a better way to do this?

-- This file proves a theorem that is missing from the 1Lab:
-- that presheaf categories are locally cartesian closed.
module Lcc where

open import Cat.Prelude
open import Cat.Functor.Adjoint
open import Cat.Functor.Naturality
import Cat.Functor.Bifunctor as Bifunctor
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
import Cat.Diagram.Exponential as Exp

--------------------------------------------------------------------------------
-- Transferring a cartesian closed structure between different implementations of `has-products` and `Terminal`.

module _ {o ℓ : Level} {C : Precategory o ℓ} {prod₁ prod₂ : has-products C} {term₁ term₂ : Terminal C} where
  private
    module C = Precategory C
    module E₁ = Exp C prod₁ term₁
    module E₂ = Exp C prod₂ term₂
    module P₁ {A} {B} = Product (prod₁ A B)
    module P₂ {A} {B} = Product (prod₂ A B)
    module p₁ {A} {B} = is-product (P₁.has-is-product {A} {B})
    module p₂ {A} {B} = is-product (P₂.has-is-product {A} {B})

  module _ (cc : E₁.Cartesian-closed) where
    map-cc : E₂.Cartesian-closed
    map-cc = E₂.product-adjoint→cartesian-closed (Bifunctor.Right (E₁.[-,-] cc)) λ A → adjoint-natural-isol
      (iso→isoⁿ
        (λ B → ×-Unique (prod₁ B A) (prod₂ B A))
        λ f →
          p₂.⟨ f C.∘ P₂.π₁ , C.id C.∘ P₂.π₂ ⟩ C.∘ p₂.⟨ P₁.π₁ , P₁.π₂ ⟩
          ≡⟨ p₂.⟨⟩∘ _ ⟩
          p₂.⟨ (f C.∘ P₂.π₁) C.∘ p₂.⟨ P₁.π₁ , P₁.π₂ ⟩ , (C.id C.∘ P₂.π₂) C.∘ p₂.⟨ P₁.π₁ , P₁.π₂ ⟩ ⟩
          ≡⟨ ap₂ p₂.⟨_,_⟩
            (sym (C.assoc _ _ _) ∙ ap (f    C.∘_) p₂.π₁∘⟨⟩ ∙ sym p₁.π₁∘⟨⟩)
            (sym (C.assoc _ _ _) ∙ ap (C.id C.∘_) p₂.π₂∘⟨⟩ ∙ sym p₁.π₂∘⟨⟩) ⟩
          p₂.⟨ P₁.π₁ C.∘ p₁.⟨ f C.∘ P₁.π₁ , C.id C.∘ P₁.π₂ ⟩ , P₁.π₂ C.∘ p₁.⟨ f C.∘ P₁.π₁ , C.id C.∘ P₁.π₂ ⟩ ⟩
          ≡⟨ sym (p₂.⟨⟩∘ _) ⟩
          p₂.⟨ P₁.π₁ , P₁.π₂ ⟩ C.∘ p₁.⟨ f C.∘ P₁.π₁ , C.id C.∘ P₁.π₂ ⟩
          ∎)
      (E₁.product⊣exponential cc)

--------------------------------------------------------------------------------
-- Transferring a cartesian closed structure between equivalent categories.
open import Cat.Functor.Equivalence

module _ {o ℓ : Level}
  {C₁ : Precategory o ℓ} {prod₁ : has-products C₁} {term₁ : Terminal C₁}
  {C₂ : Precategory o ℓ} {prod₂ : has-products C₂} {term₂ : Terminal C₂}
  where
  private
    module E₁ = Exp C₁ prod₁ term₁
    module E₂ = Exp C₂ prod₂ term₂
  module _ (equiv : Equivalence C₂ C₁) (cc : E₁.Cartesian-closed) where

    -- These assumptions are unnecessary, but the proof is longer without them.
    module _ (c₁ : is-category C₁) (c₂ : is-category C₂) where
      open import Cat.Functor.Equivalence.Path
      open Equivalence equiv

      -- This term is uniquely determined, and has bad computational behavior, so I hide its implementation entirely.
      abstract
        equiv-cc : E₂.Cartesian-closed
        equiv-cc = map-cc $ snd $ snd
          $ transport (λ i → Σ _ λ prod → Σ _ λ term → Exp.Cartesian-closed (eqv→path c₂ c₁ _ To-equiv (~ i)) prod term)
          $ _ , _ , cc

--------------------------------------------------------------------------------

open import Cat.Functor.Base
open import Cat.Diagram.Limit.Finite
open import Cat.CartesianClosed.Locally; open Locally-cartesian-closed
open import Cat.Instances.Sets.Complete
open import Cat.Instances.Functor.Limits
open import Cat.Instances.Presheaf.Exponentials
open import Cat.Instances.Slice
open import Cat.Instances.Slice.Presheaf
open import Cat.Instances.Elements

module _ {ℓ : Level} (C : Precategory ℓ ℓ) where
  open import Cat.Instances.Sets
  open import Cat.Functor.Univalence
  lcc-psh : Locally-cartesian-closed (PSh ℓ C)
  lcc-psh .has-is-lex = is-complete→finitely _ $ Functor-cat-is-complete $ Sets-is-complete {ℓ} {ℓ} {ℓ}
  lcc-psh .slices-cc A = equiv-cc
    record { To = slice→total ; To-equiv = slice→total-is-equiv } (PSh-closed (∫ C A))
    (Functor-is-category Sets-is-category) (slice-is-category (Functor-is-category Sets-is-category))

I have verified that this code compiles on Agda 2.8.0, against 1Lab commit fc51a347b48a55ff7d7dedd16211ae99ca5ea561. (This seems to be the last commit compatible with Agda 2.8.0, and I'd rather not deal with the upgrade process.)

[ncfavier]

Is there a better way to do this?

You can use the fact that limits are unique in univalent categories. This will probably compute worse, but computation is going to be bad with this approach anyway because of regularity issues.

With the additions in https://github.com/the1lab/1lab/pull/536, you can write this:

open import Cat.Prelude
open import Cat.Functor.Base
open import Cat.Functor.Equivalence.Path
open import Cat.Functor.Univalence
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Diagram.Exponential
open import Cat.Instances.Sets
open import Cat.Instances.Presheaf.Limits
open import Cat.Instances.Presheaf.Exponentials
open import Cat.Instances.Elements
open import Cat.Instances.Slice.Presheaf
open import Cat.CartesianClosed.Locally

open Locally-cartesian-closed

module _ {ℓ : Level} (C : Precategory ℓ ℓ) where
  lcc-psh : Locally-cartesian-closed (PSh ℓ C)
  lcc-psh .has-is-lex = PSh-finite-limits ℓ C
  lcc-psh .slices-cc A =
    transport
      (sym $ happly-dep
        (happly-dep (ap Cartesian-closed path)
          (is-prop-i1→pathp (Π-is-hlevel² 1 λ _ _ → Product-is-prop PSh-is-cat) _ _))
        (is-prop-i1→pathp (⊤-is-prop _ PSh-is-cat) _ _))
      (PSh-closed (∫ C A))
    where
    path = Precategory-path slice→total slice→total-is-iso
    PSh-is-cat = Functor-is-category Sets-is-category

[finegeometer]

Wow, that's much cleaner! Let me see if I can summarize what you did:

The argument is:

• We have a path between categories.
• Over this path, we have a path between the choices for products and the terminal object, since the type of such things is propositional.
• Therefore, we can transport the cartesian closed structure across this triple of paths.

To make this work, you introduced a new pull request to do the following:

• Add new helper functions and macros for working with paths.
• Prove that Product is propositional.

Do I have that right?