Disjoint union of fin's

Stream: Is there code for X?

[Adam Topaz]

Hi everyone. I'm looking for the statement that fin (a + b) is the disjoint union of fin a and fin b, in terms of the universal property of the disjoint union. Specifically, I'm looking for the following definitions and theorems, and I hope mathlib has something similar which I can use:

def inl {a b : ℕ} : fin a → fin (a + b) := λ x, ⟨x.1, by {cases x, linarith}⟩

def inr {a b : ℕ} : fin b → fin (a + b) := λ x, ⟨a + x.1, by {cases x, linarith}⟩

def sum {a b : ℕ} {T : Type*} (f : fin a → T) (g : fin b → T) : fin (a + b) → T :=
  λ x, if h : x.1 < a then f ⟨x.1,h⟩ else g ⟨x.1 - a, (nat.sub_lt_left_iff_lt_add $ not_lt.mp h).mpr x.2⟩

theorem suml {a b : ℕ} {T : Type*} (f : fin a → T) (g : fin b → T) :
  (sum f g) ∘ inl = f := sorry

theorem sumr {a b : ℕ} {T : Type*} (f : fin a → T) (g : fin b → T) :
  (sum f g) ∘ inr = g := sorry

theorem sum_unique {a b : ℕ} {T : Type*} (f : fin a → T) (g : fin b → T) (h : fin (a + b) → T):
  h ∘ inl = f → h ∘ inr = g → h = sum f g := sorry

[Scott Morrison]

There is src#sum_fin_sum_equiv

[Scott Morrison]

Which has an equivalence, although no lemmas saying what the equivalence actually does. :-(

[Adam Topaz]

That should be good enough! Thanks!

[Scott Morrison]

If you feel like PRing some extra material around that definition, that would be great. :-)

[Adam Topaz]

Sure, i could do that. Is there no theorem which proves the universal property of sum/product assuming an equivalence with a sum/product?