Extensionality of globular types

[fredrik-bakke]

Adds a postulate to characterize equality of globular types.

[fredrik-bakke]

It is not presently clear to me whether it is possible to show that equality of globular types as introduced in this PR is equivalent to coinductive equalities of globular types, and therefore equivalences of globular types by univalence.

EDIT: Never mind, I figured it out.

[fredrik-bakke]

The idea of this PR arose from reading the introduction to this paper:

• Formalising inductive and coinductive containers, by Stefanie Damato, Thorsten Altenkirch, and Axel Ljungström (arXiv:2409.02603)

[fredrik-bakke]

Quite a few questions linger with this PR. First and foremost, is the added axiom validated in all ∞-topoi?
I'm currently working on an accompanying contribution showing that globular types and globular diagrams are equivalent, using this axiom.

[EgbertRijke]

I don't think the open question is really open at all. The equality relation you have given is just bisimilation, and for coinductive types in a type theory with function extensionality it is known that bisimilation characterizes the identity type. Basically all you need to know is that the coinductive type is the limit of iterated applications of a polynomial endofunctor to the terminal object, and that identity types of limits are limits of identity types.

[EgbertRijke]

I'd be happy to merge this PR once it passes the checks

[fredrik-bakke]

I don't think the open question is really open at all. The equality relation you have given is just bisimilation, and for coinductive types in a type theory with function extensionality it is known that bisimilation characterizes the identity type. Basically all you need to know is that the coinductive type is the limit of iterated applications of a polynomial endofunctor to the terminal object, and that identity types of limits are limits of identity types.

Oh, well that settles it then :) Thank you for the answer