@TashiWalde makes a good point that renaming terms such as is-covariant-representable-is-segal to is-covariant-hom-is-segal would be both shorter and more in line with our style guide. I'd be happy to implement this change throughout.
One challenge is that section 8 involves both covariant and contravariant versions of hom. The term is-contravariant-hom-is-segal is no problem but we might have to be careful with the names for a few auxiliary terms, eg the current dhom-representable and dhom-contra-representable.
@TashiWalde makes a good point that renaming terms such as
is-covariant-representable-is-segaltois-covariant-hom-is-segalwould be both shorter and more in line with our style guide. I'd be happy to implement this change throughout.One challenge is that section 8 involves both covariant and contravariant versions of hom. The term
is-contravariant-hom-is-segalis no problem but we might have to be careful with the names for a few auxiliary terms, eg the currentdhom-representableanddhom-contra-representable.