nLab
isomorphism in a Segal type
Context
Directed homotopy type theory
Contents
Definition
In simplicial type theory, given a Segal type and terms and , a “morphism” (term of hom type) is an isomorphism if there exist morphisms and such that and
The type of all isomorphisms between and in is defined as
References
Last revised on May 21, 2023 at 13:46:02.
See the history of this page for a list of all contributions to it.