transport through trivial bundles

Stream: general

[Scott Morrison]

I find myself needing a few lemmas about parallel transport through trivial bundles. (In the first case, this is literally the case, the later ones are close analogues.)

universes u₁ u₂

@[simp] lemma {u₁ u₂} parallel_transport_for_trivial_bundles {α : Sort u₁} {a b : α} {β : Sort u₂} (p : a = b) (x : β) : @eq.rec α a (λ _, β) x b p = x :=
begin
  induction p,
  simp,
end

@[simp] lemma plift.rec.constant {α : Sort u₁} {β : Sort u₂} (b : β) : @plift.rec α (λ _, β) (λ _, b) = λ _, b :=
begin
  apply funext,
  intros,
  cases x,
  refl,
end

@[simp] lemma ulift.rec.constant {α : Type u₁} {β : Sort u₂} (b : β) : @ulift.rec α (λ _, β) (λ _, b) = λ _, b :=
begin
  apply funext,
  intros,
  cases x,
  refl,
end

[Scott Morrison]

Are these welcome in mathlib? If so, where do they go?

[Scott Morrison]

(These all arise after using cases on hypotheses in fairly harmless ways.)

[Scott Morrison]

I made a PR for this at <https://github.com/leanprover/mathlib/pull/124>.

[Johan Commelin]

This is all going to follow from your transportable stuff later on, I guess...

[Johan Commelin]

I mean, parallel transport in maths is an instance of transport of structure...