## Stream: general

### Topic: Show the objects for an equality of morphisms

#### Bhavik Mehta (Apr 22 2020 at 16:33):

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 (Apr 22 2020 at 16:35):

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

#### Bhavik Mehta (Apr 22 2020 at 16:38):

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

#### Reid Barton (Apr 22 2020 at 16:39):

Just get them involved in the notation

#### Bhavik Mehta (Apr 22 2020 at 16:40):

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


like this?

#### Bhavik Mehta (Apr 22 2020 at 16:40):

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

hmm

I don't know

#### Bhavik Mehta (Apr 22 2020 at 16:41):

I'll make a MWE, one sec

#### Bhavik Mehta (Apr 22 2020 at 16:45):

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 (Apr 22 2020 at 17:22):

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


doesn't work either

#### Bhavik Mehta (May 01 2020 at 00:33):

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

#### Bhavik Mehta (May 01 2020 at 00:34):

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

#### Bhavik Mehta (May 01 2020 at 00:34):

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

#### Bhavik Mehta (May 01 2020 at 00:34):

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

Last updated: May 11 2021 at 13:22 UTC