Terminal Object Identity

Stream: new members

[Klaus Gy]

Hello, I have some proof like h.isTerminal : IsTerminal h.Ω₀ which I can use to construct an instance of HasTerminal C via h.isTerminal.hasTerminal. But it seems that ⊤_ C is not automatically equal to h.Ω₀. Is that by design? Is there an interface which returns both, an instance of HasTerminal C and a proof of ⊤_ C = h.Ω₀?

[Kenny Lau]

@Klaus Gy That is intentional, because terminal objects are not unique!

[Klaus Gy]

Yes, but since ⊤_ C is some concrete object, why can't I have it be the one I used to construct HasTerminal C?

[Kenny Lau]

#mathlib4 > Why are limits in category noncomputable?

[Klaus Gy]

Thanks!

[Kenny Lau]

I asked a different question, so I got a different answer, but I suspect it is still to prevent diamonds

[Kenny Lau]

basically, you made HasTerminal for category C, brilliant, but now I have another HasTerminal instance for C, and so now our two terminal objects are not defeq! (shocker!)

[Kenny Lau]

(cf. building product from pullback+terminal)

[Klaus Gy]

That's really helpful!