isomorphism vs equality in concrete category

Stream: new members

[Jack J Garzella]

I've been trying to prove the following fact:

Consider the category of Types. This has a (cartesian) monoidal structure, and thus has a left unitor
λ_ A : 𝟙_ (Type u) ⊗ A ≅ A. I'd like to prove that (λ_ A).hom (punit.star,a) = a for all a : A.

Unfortunately, I'm running into an issue: the statement I wrote above won't type check, because the type
𝟙_ (Type u) ⊗ A, which is defined to be 𝟙_ (Type u) \X A is not definitionally equal to the cartesian product 𝟙_ (Type u) \x A. In fact, the one with the big X is isomorphic to the one with the little x, but they aren't definitionally equal.

I can try to fix this by using equiv_rw to make the type checker happy. However, when I try to prove my statement about elements, I have no idea what to do.

In fact, somewhere under the covers, the definition of (λ_ A) comes down to prod.snd, but this is also defined across an isomorphism--in fact, it's the same isomorphism that I'm using equiv_rw on. Lean doesn't seem to know this though.

It feels like there should be a better approach. Can anyone give me some pointers?

Here's the #mwe

import category_theory.closed.cartesian
import category_theory.limits.types
import category_theory.limits.shapes.types
import category_theory.types

noncomputable theory

universes u v

open category_theory
open category_theory.limits
open category_theory.limits.types
open category_theory.concrete_category

instance : monoidal_category (Type u) :=
  monoidal_of_has_finite_products (Type u)

variables {A : (Type u)}

lemma type_prod_iso_monoidal_prod (A B : (Type u)) :
(A ⊗ B) ≅ (A × B)
:= by apply types.binary_product_iso

lemma terminal_iso_punit : 𝟙_ (Type u) ≅ punit
:= by apply terminal_iso

def lcomb_correct_type
: (punit × A) → A :=
begin
  let lcomb := (λ_ A).hom,
  equiv_rw [iso.to_equiv (type_prod_iso_monoidal_prod (𝟙_ (Type u)) A)]
    at lcomb,
  equiv_rw [iso.to_equiv terminal_iso_punit] at lcomb,
  exact lcomb
end

theorem elementwise_lcomb (a : A) : lcomb_correct_type (punit.star,a) = a :=
begin
  have step : lcomb_correct_type = prod.snd,
    begin
      sorry, --???
    end,
  rw [step],
end

[Adam Topaz]

It seems that you defined things in a fairly non-optimal way. For example:

import category_theory.closed.cartesian
import category_theory.limits.types
import category_theory.limits.shapes.types
import category_theory.types

noncomputable theory

universes u v

open category_theory
open category_theory.limits
open category_theory.limits.types
open category_theory.concrete_category

instance : monoidal_category (Type u) :=
  monoidal_of_has_finite_products (Type u)

variables {A : (Type u)}

def punit_prod_iso (A : Type u) :
  (punit : Type u) × A ≅ A :=
(types.binary_product_iso _ _).symm ≪≫ tensor_iso terminal_iso.symm (iso.refl _) ≪≫ (λ_ A)

theorem elementwise_lcomb (a : A) : (punit_prod_iso A).hom (punit.star, a) = a :=
by simp [punit_prod_iso]