[Merged by Bors] - refactor(RelCat): use a type synonym for homs#25593
[Merged by Bors] - refactor(RelCat): use a type synonym for homs#25593YaelDillies wants to merge 3 commits intomasterfrom
Conversation
This improves automation and follows the new pattern for concrete categories (although `RelCat` is *not* a concrete category).
PR summary d1c754c26eImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| map_id X := by | ||
| ext x y | ||
| exact Eq.comm | ||
| map_comp {X Y Z} f g := by |
There was a problem hiding this comment.
Is this something that aesop_cat previously couldn't solve, or did we just not ask it to?
There was a problem hiding this comment.
I just tried and no it couldn't:
could not synthesize default value for field 'map_id' of 'CategoryTheory.Functor' using tactics
RelCat.lean:138:36
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
Initial goal:
⊢ ∀ (X : RelCatᵒᵖ), (fun x y ↦ unop (𝟙 X) y x) = 𝟙 (unop X)
Remaining goals after safe rules:
X : RelCatᵒᵖ
⊢ (fun x y ↦ unop (𝟙 X) y x) = 𝟙 (unop X)
It was precisely getting stuck at seeing X → X → Prop through X ⟶ X to apply extensionality.
There was a problem hiding this comment.
Could you mention ext in the description? No need to give the full error.
| @[ext] lemma ext (f g : X ⟶ Y) (h : f.rel = g.rel) : f = g := by | ||
| obtain ⟨R⟩ := f; obtain ⟨S⟩ := g; congr | ||
|
|
||
| @[simp] protected theorem rel_id (X : RelCat.{u}) : rel (𝟙 X) = (· = ·) := rfl |
There was a problem hiding this comment.
I'm curious if simps on the instance generates these, but I'm happy to leave things as is either way.
There was a problem hiding this comment.
Indeed it can, but that means they are outside the Hom namespace. Is that okay?
|
|
||
| open Rel | ||
|
|
||
| attribute [local simp] Rel.comp Rel.inv flip |
There was a problem hiding this comment.
I'd be tempted to wrap these with in just around the declaration that uses them.
There was a problem hiding this comment.
Either that, or apply simp globally
There was a problem hiding this comment.
This is a patch until #25587 is in: After that second PR is merged, they won't be needed anymore 😉
|
bors merge Indeed, this seems to match the pattern being established, and the Thanks! |
This improves automation and follows the new pattern for concrete categories (although `RelCat` is *not* a concrete category).
|
Pull request successfully merged into master. Build succeeded: |
…5593) This improves automation and follows the new pattern for concrete categories (although `RelCat` is *not* a concrete category).
…5593) This improves automation and follows the new pattern for concrete categories (although `RelCat` is *not* a concrete category).
This improves automation and follows the new pattern for concrete categories (although
RelCatis not a concrete category).