CatDat

Implication Details

Assumptions: essentially discrete

Conclusions: groupoidthin

This is an equivalence.

Reason: This is trivial.