Show the objects for an equality of morphisms

Stream: general

[Bhavik Mehta]

In the middle of an involved proof, I've got a goal which looks like (pullback.snd ≫ prod.fst) ≫ pullback.snd ≫ prod.snd = pullback.snd ≫ prod.snd ≫ f.hom. Now this is super opaque, though I'm pretty sure the maths proof should be an easy diagram chase. What would be super helpful then is to see the actual objects involved here so it looks a bit more like (pullback.snd ≫ limits.prod.fst) ≫ pullback.snd ≫ (limits.prod.snd : _ ⨯ B ⟶ B) = pullback.snd ≫ (limits.prod.snd : Q f ⨯ f.left ⟶ f.left) ≫ (f.hom : f.left ⟶ B) (ideally some more, but I've just put these in manually. Essentially I'd like something between the default pretty printer and pp.implicit true - is this possible? (of course under an option)

[Reid Barton]

Hmm, if you made a local notation for ≫ with the objects involved explicit, I think the pretty printer would use it over ≫.

[Bhavik Mehta]

This seems promising - how do I make the objects explicit in a notation though?

[Reid Barton]

Just get them involved in the notation

[Bhavik Mehta]

local notation f `% ` A ` %` g := (f : _ ⟶ A) ≫ (g : A ⟶ _)

like this?

[Bhavik Mehta]

That doesn't seem to work for me... Am I missing some priority thing?

[Reid Barton]

hmm

[Reid Barton]

I don't know

[Bhavik Mehta]

I'll make a MWE, one sec

[Bhavik Mehta]

import category_theory.category

open category_theory
universes v u

variables {C : Type u} [𝒞 : category.{v} C]
include 𝒞

local notation f `# ` A ` #` g := (f : _ ⟶ A) ≫ g

example {P Q R S : C} (f : P ⟶ Q) (g : Q ⟶ R) (h : R ⟶ S) : f ≫ g ≫ h = ((f ≫ g) ≫ h) :=
begin

end

[Kevin Buzzard]

notation B ` & ` f `# ` A ` #` g ` & ` C := (f : B ⟶ A) ≫ (g : A ⟶ C)

doesn't work either

[Bhavik Mehta]

A hack which does the job for now: def tag' (n : ℕ) (A B : C) (f : A ⟶ B) : A ⟶ B := f

[Bhavik Mehta]

Then when my goal is pullback m₁ m₂ ⟶ pullback pullback.snd pullback.snd, I can write

[Bhavik Mehta]

change pullback m₁ m₂ ⟶ pullback (tag' 0 _ _ pullback.snd) (tag' 1 _ _ pullback.snd),

[Bhavik Mehta]

which changes the goal to pullback m₁ m₂ ⟶ pullback (tag' 0 (pullback (mem (⊤_ C)) (prod.map (hat (m₂ ≫ prod.lift (𝟙 E) (terminal.from E))) (𝟙 (⊤_ C)))) (E ⨯ ⊤_ C) pullback.snd) (tag' 1 (pullback (mem (⊤_ C)) (prod.map (hat (m₁ ≫ prod.lift (𝟙 E) (terminal.from E))) (𝟙 (⊤_ C)))) (E ⨯ ⊤_ C) pullback.snd), which is more helpful