port CategoryTheory.WithTerminal !4#2630

Stream: PR reviews

[Scott Morrison]

@Jannis Limperg, could I request some help with aesop here? The situation is that we frequently have a hypothesis f : star ⟶ of X, where this hom space is just defined as PEmpty. We'd like to have aesop_cat automatically perform case analysis whenever it sees such a hypothesis, but I'm not sure how to request this. Adding a cases rule on PEmpty isn't enough, because it can't see through the definition. Adding an apply rule for PEmpty.elim unsurprisingly runs off the rails.

[Jannis Limperg]

Try adding a forward or destruct rule which concludes False from star ⟶ of X. Then Aesop will close the goal with the next simp.

[Scott Morrison]

Great. Made some improvements to the PR based on this idea.