Trebor on Nostr: nprofile1q…d6kk0 Ah, so from the perspective of the quotient inductive type, the ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 (nprofile…6kk0) Ah, so from the perspective of the quotient inductive type, the input should be a map f equipped with an inverse to the structure morphism from dom(f) to the pullback of f with itself, and the output is a name in the subobject classifier. If I understand correctly, this applies when all kernel pairs exist?