typeclass instances help

Stream: general

[Bhavik Mehta]

Here's a massively simplified version of where I'm stuck:

import category_theory.adjunction.basic
import category_theory.limits.shapes
import category_theory.limits.over

namespace category_theory
open category limits

universes v u

class exponentiable {C : Type u} [𝒞 : category.{v} C] [bp : has_finite_products.{v} C] (X : C) :=
(is_adj : is_left_adjoint (prod_functor.obj X))

class is_cartesian_closed (C : Type u) [𝒞 : category.{v} C] extends has_finite_products.{v} C :=
(cart_closed : Π (X : C), exponentiable X)

attribute [instance] is_cartesian_closed.cart_closed

variables {C : Type u} [𝒞 : category.{v} C]
include 𝒞

def exp.functor (A : C) [has_finite_products.{v} C] [exponentiable A] : C ⥤ C :=
(@exponentiable.is_adj _ _ _ A _).right

@[reducible]
def star (B : C) [has_binary_products.{v} C] : C ⥤ over B := sorry
def Pi_functor (B : C) [has_finite_limits.{v} C] [exponentiable B] : over B ⥤ C := sorry
def star_adj_pi_of_exponentiable (B : C) [has_finite_limits.{v} C] [exponentiable B] : star B ⊣ Pi_functor B := sorry

section pb
local attribute [instance] over.construct_products.over_binary_product_of_pullback

@[reducible]
def pullback_along [has_pullbacks.{v} C] {A B : C} (f : A ⟶ B) : over B ⥤ over A :=
star (over.mk f) ⋙ (over.iterated_slice_equiv _).functor
end pb

variable (C)

class is_locally_cartesian_closed extends has_finite_limits.{v} C :=
(overs_cc : Π (B : C), is_cartesian_closed (over B))

local attribute [instance] is_locally_cartesian_closed.overs_cc
local attribute [instance] has_pullbacks_of_has_finite_limits
local attribute [instance] has_finite_wide_pullbacks_of_has_finite_limits

variable [is_locally_cartesian_closed.{v} C]

lemma thing {A B : C} (f : A ⟶ B) : is_left_adjoint (pullback_along f) :=
{ right := _ ⋙ _, adj := adjunction.comp _ _ (star_adj_pi_of_exponentiable (over.mk f)) (equivalence.to_adjunction _) }

end category_theory

My issue is that star_adj_pi_of_exponentiable gives a typeclass error (it can't find exponentiable (over.mk f)), but it should be okay since we have that C is LCC, so C/B is CC, and over.mk f is in C/B, so over.mk f should be exponentiable... How can I make this work?

[Reid Barton]

My guess is you have too many instances

[Reid Barton]

You ask about making it work, but first do you know why it doesn't work?

[Bhavik Mehta]

I'm not really sure why it doesn't work. I tried manually giving the instances which should make it work, and it gives this error:

type mismatch at application
  star_adj_pi_of_exponentiable (over.mk f)
term
  is_cartesian_closed.cart_closed (over.mk f)
has type
  @exponentiable (@over C 𝒞 B) (@over.category_1 C 𝒞 B)
    (@is_cartesian_closed.to_has_finite_products (@over C 𝒞 B) (@over.category_1 C 𝒞 B)
       (@is_locally_cartesian_closed.overs_cc C 𝒞 _inst_1 B))
    (@over.mk C 𝒞 B A f)
but is expected to have type
  @exponentiable (@over C 𝒞 B) (@over.category_1 C 𝒞 B)
    (@limits.has_finite_products_of_has_finite_limits (@over C 𝒞 B) (@over.category_1 C 𝒞 B)
       (@over.has_finite_limits C 𝒞 B
          (@has_finite_wide_pullbacks_of_has_finite_limits C 𝒞
             (@is_locally_cartesian_closed.to_has_finite_limits C 𝒞 _inst_1))))
    (@over.mk C 𝒞 B A f)

[Bhavik Mehta]

and here was the instance I put in:

lemma thing {A B : C} (f : A ⟶ B) : is_left_adjoint (pullback_along f) :=
{ right := _ ⋙ _, adj := adjunction.comp _ _ (@star_adj_pi_of_exponentiable _ _ (over.mk f) _ (@is_cartesian_closed.cart_closed _ _ _ (over.mk f))) (equivalence.to_adjunction _) }

[Reid Barton]

Yes, this looks like the sort of issue I suspected

[Reid Barton]

You have too many ways to prove C/B has products

[Bhavik Mehta]

Hmm okay... What sort of thing should I be trying to fix this?

[Bhavik Mehta]

Could I make has_finite_products_of_has_finite_limits not be an instance locally?

[Reid Barton]

I would start by avoiding extends. If that isn't enough, you would have to remove some instances.

[Reid Barton]

You cannot just make any old construction that works in math into an instance because of issues like this.

[Bhavik Mehta]

I'll try removing extends, thanks!

[Bhavik Mehta]

Out of interest, why does that cause problems?

[Reid Barton]

I think there is no substitute for reading the error message and understanding how you got there

[Reid Barton]

In general, using extends is less flexible because you cannot specify the base instance and the "extension" separately.

[Reid Barton]

It might help to translate your definitions back into math as follows:
A CC category is a category with chosen finite products such that each chosen finite product functor X x - has a (chosen) right adjoint.
An LCC category is a category with chosen finite limits such that each slice category C/B is a CC category.

[Reid Barton]

You also know of a way, given chosen finite limits in C, to construct finite products in C/B for each B.

[Reid Barton]

However, your definitions don't require that if you apply this construction to the chosen finite limits of C, you get the chosen finite products of C/B.

[Reid Barton]

(Technically, since you didn't write extends category, I should say something like "A category C is CC if we have chosen finite products for it such that ...", but the category instance is not at issue here.)

[Reid Barton]

If you don't use extends in the definition of is_cartesian_closed then the translation is
"A category C with chosen finite products is CC if for each X, the chosen product functor X x - has a right adjoint"
and now there's a better chance you can make everything coherent

[Bhavik Mehta]

That makes a lot of sense, thanks

[Reid Barton]

This library design problem would be a lot easier if we didn't try to make things constructive, because then everything in sight would be a Prop.