search

b-mehta / topos

Topos theory in lean
56 stars 2 forks source link

Generalise `limit.lift_self_id` etc to cones. #7

Open EdAyers opened 4 years ago

EdAyers commented 4 years ago
b-mehta commented 4 years ago

For with_id_l, here's what the type could look like

lemma pullback.with_id_l' {X Y : C} (f : X ⟶ Y) :
  is_limit (pullback_cone.mk f (𝟙 X) (show f ≫ (𝟙 Y) = (𝟙 X) ≫ f, by simp)) :=