Presieve of arrows for coproduct inclusions

Stream: maths

[Dagur Asgeirsson]

The inclusion arrows in a coproduct are "obviously" in 1-1 correspondence with the indexing set. I've defined a map from the indexing set to the corresponding Presieve.ofArrows and proved that it's surjective, but I'm running into problems with injectivity. The simp lemma Sigma.mk.inj_iff gives me a heterogenous equality in h below. Is there any way to work with that? Is there a better way to do this?

import Mathlib.CategoryTheory.Sites.Sieves
import Mathlib.CategoryTheory.Limits.Shapes.Products

open CategoryTheory Limits

variable {C α : Type*} [Category C] (Z : α → C) [HasCoproduct Z]

noncomputable
def map : α → Σ(Y : C), { f : Y ⟶ ∐ Z // Presieve.ofArrows Z (fun j ↦ Sigma.ι Z j) f } :=
  fun a => ⟨Z a, (fun j ↦ Sigma.ι Z j) a, Presieve.ofArrows.mk a⟩

lemma surj : Function.Surjective (map Z) :=
  fun ⟨_, ⟨_, hf⟩⟩ ↦ by cases' hf with a _; exact ⟨a, rfl⟩

lemma inj : Function.Injective (map Z) := by
  intro a b h
  simp only [map, Sigma.mk.inj_iff] at h
    -- Gives: h: Z a = Z b ∧
    --   HEq { val := Sigma.ι Z a, property := _ } { val := Sigma.ι Z b, property := _ }
  sorry

[Joël Riou]

In your example, map Z may not be injective. Let us say C is a category with only one object and only one map. This category C has coproducts (e.g. this category is equivalent to the category of sheaves of sets over the empty space). Then, if you take any family Z : α → C, all the injections into the coproduct are the same map, even though α may contain several distinct elements.

[Dagur Asgeirsson]

Thanks! In my application, the category C is Extensive, which is hopefully enough, I'll have to think more about that.

But in general, is heterogenous equality of morphisms in categories at all useful?

[Joël Riou]

Dagur Asgeirsson said:

But in general, is heterogenous equality of morphisms in categories at all useful?

If we can avoid this, it is usually better.