Translating categorical UP reasoning to lean

Stream: mathlib4

[Nicolas Rolland]

In informal categoric reasoning, we often reason via UP.

Say, to prove FF of the embedding Cat A B ⥤ Dist A B, where given functors F G : A ⥤ B we have set isomorphisms
$Nat(F,G) ≃ End~ B(F-,G=) ≃ End ~[B^{op},Set](B(-,F=), B(-,G=))≃ Nat(B(-,F=),B(-,G=))$

The first (and last) equivalence is a "lie" as terminal wedges are only defined up to iso, so Nat(F,G) is not equivalent to "the" end, but is an End. If we naively define abbrev End := Σ w : Wedge F, Limits.IsTerminal w, we actually have a set of ends, all of which are set-isomorphic to each other.

So either Nat(F,G) ∈ End B(F-,G=) or End can be quotiented to get Nat(F,G) ≃ Q(End B(F-,G=))

Is there already some facility in Mathlib for such quotient where every path is an iso ?
Is it the prefered way to deal with UPs ?

How to translate UP reasoning with the least amount of syntactic noise ?

[Scott Carnahan]

If you have two objects in a contractible groupoid, then they admit a unique isomorphism between them. Are you asking how to spell that in mathlib?

[Nicolas Rolland]

I am asking if there is already some syntactic sugar, or boilerplate code, to make Lean expression look like informal category, where such kind of reasoning is everywhere.

It relies on contractible groupoid (+ some isos of, when chaining such groupoids equivalence ), but maybe there is already something plugged in, given how often we reason that way in category.

Or not, and then wouldn't it make sense to have such facility ?