Skip to main content
the forthcoming paper forthcame
Source Link

I'm not sure exactly what you're asking, but the general pattern for "positive" types is to assert that every "structured" display map over the type has a specified structured section. This matches the induction principle of a positive type former in type theory. One then needs to require a sort of "pullback-stability" condition as well in order to model substitution in type theory. A forthcoming paper of Lumsdaine and Warren will describe a general process of "strictification" of "weakly stable" structure in a comprehension category into "strictly coherent" structure in a fully strict structure. (Edit: this paper is now available, as Lumsdaine–Warren 2015 The local universes construction…)

For identity types, the categorical structure is essentially a well-behaved weak factorization system in which the display maps are (or generate) the right class: see for instance this paper.

Edit: One can be more precise about the notion of "structured section", for instance to say that a "strongly homotopy initial object" in a display-map category is an object $X$ such that every display map with codomain $X$ has a section. Since all ordinary categorical left universal properties can be reformulated as initial objects in some category, this gives a way to translate them into an $\eta$-free version as long as the category in question inherits a natural notion of display map (which is generally induced directly from the underlying category of types/contexts). Similarly, a strongly homotopy initial object is "weakly preserved" by a functor if its image under that functor is another strongly homotopy initial object (not necessarily the "chosen" such object in the codomain of the functor, if there is one). Weak stability then means that pullback functors weakly preserve the relevant SHIOs. I think this is as close to a "general pattern" as you can get.

I'm not sure exactly what you're asking, but the general pattern for "positive" types is to assert that every "structured" display map over the type has a specified structured section. This matches the induction principle of a positive type former in type theory. One then needs to require a sort of "pullback-stability" condition as well in order to model substitution in type theory. A forthcoming paper of Lumsdaine and Warren will describe a general process of "strictification" of "weakly stable" structure in a comprehension category into "strictly coherent" structure in a fully strict structure.

For identity types, the categorical structure is essentially a well-behaved weak factorization system in which the display maps are (or generate) the right class: see for instance this paper.

Edit: One can be more precise about the notion of "structured section", for instance to say that a "strongly homotopy initial object" in a display-map category is an object $X$ such that every display map with codomain $X$ has a section. Since all ordinary categorical left universal properties can be reformulated as initial objects in some category, this gives a way to translate them into an $\eta$-free version as long as the category in question inherits a natural notion of display map (which is generally induced directly from the underlying category of types/contexts). Similarly, a strongly homotopy initial object is "weakly preserved" by a functor if its image under that functor is another strongly homotopy initial object (not necessarily the "chosen" such object in the codomain of the functor, if there is one). Weak stability then means that pullback functors weakly preserve the relevant SHIOs. I think this is as close to a "general pattern" as you can get.

I'm not sure exactly what you're asking, but the general pattern for "positive" types is to assert that every "structured" display map over the type has a specified structured section. This matches the induction principle of a positive type former in type theory. One then needs to require a sort of "pullback-stability" condition as well in order to model substitution in type theory. A forthcoming paper of Lumsdaine and Warren will describe a general process of "strictification" of "weakly stable" structure in a comprehension category into "strictly coherent" structure in a fully strict structure. (Edit: this paper is now available, as Lumsdaine–Warren 2015 The local universes construction…)

For identity types, the categorical structure is essentially a well-behaved weak factorization system in which the display maps are (or generate) the right class: see for instance this paper.

Edit: One can be more precise about the notion of "structured section", for instance to say that a "strongly homotopy initial object" in a display-map category is an object $X$ such that every display map with codomain $X$ has a section. Since all ordinary categorical left universal properties can be reformulated as initial objects in some category, this gives a way to translate them into an $\eta$-free version as long as the category in question inherits a natural notion of display map (which is generally induced directly from the underlying category of types/contexts). Similarly, a strongly homotopy initial object is "weakly preserved" by a functor if its image under that functor is another strongly homotopy initial object (not necessarily the "chosen" such object in the codomain of the functor, if there is one). Weak stability then means that pullback functors weakly preserve the relevant SHIOs. I think this is as close to a "general pattern" as you can get.

added 989 characters in body
Source Link
Mike Shulman
  • 66.7k
  • 7
  • 162
  • 368

I'm not sure exactly what you're asking, but the general pattern for "positive" types is to assert that every "structured" display map over the type has a specified structured section. This matches the induction principle of a positive type former in type theory. One then needs to require a sort of "pullback-stability" condition as well in order to model substitution in type theory. A forthcoming paper of Lumsdaine and Warren will describe a general process of "strictification" of "weakly stable" structure in a comprehension category into "strictly coherent" structure in a fully strict structure.

For identity types, the categorical structure is essentially a well-behaved weak factorization system in which the display maps are (or generate) the right class: see for instance this paper.

Edit: One can be more precise about the notion of "structured section", for instance to say that a "strongly homotopy initial object" in a display-map category is an object $X$ such that every display map with codomain $X$ has a section. Since all ordinary categorical left universal properties can be reformulated as initial objects in some category, this gives a way to translate them into an $\eta$-free version as long as the category in question inherits a natural notion of display map (which is generally induced directly from the underlying category of types/contexts). Similarly, a strongly homotopy initial object is "weakly preserved" by a functor if its image under that functor is another strongly homotopy initial object (not necessarily the "chosen" such object in the codomain of the functor, if there is one). Weak stability then means that pullback functors weakly preserve the relevant SHIOs. I think this is as close to a "general pattern" as you can get.

I'm not sure exactly what you're asking, but the general pattern for "positive" types is to assert that every "structured" display map over the type has a specified structured section. This matches the induction principle of a positive type former in type theory. One then needs to require a sort of "pullback-stability" condition as well in order to model substitution in type theory. A forthcoming paper of Lumsdaine and Warren will describe a general process of "strictification" of "weakly stable" structure in a comprehension category into "strictly coherent" structure in a fully strict structure.

For identity types, the categorical structure is essentially a well-behaved weak factorization system in which the display maps are (or generate) the right class: see for instance this paper.

I'm not sure exactly what you're asking, but the general pattern for "positive" types is to assert that every "structured" display map over the type has a specified structured section. This matches the induction principle of a positive type former in type theory. One then needs to require a sort of "pullback-stability" condition as well in order to model substitution in type theory. A forthcoming paper of Lumsdaine and Warren will describe a general process of "strictification" of "weakly stable" structure in a comprehension category into "strictly coherent" structure in a fully strict structure.

For identity types, the categorical structure is essentially a well-behaved weak factorization system in which the display maps are (or generate) the right class: see for instance this paper.

Edit: One can be more precise about the notion of "structured section", for instance to say that a "strongly homotopy initial object" in a display-map category is an object $X$ such that every display map with codomain $X$ has a section. Since all ordinary categorical left universal properties can be reformulated as initial objects in some category, this gives a way to translate them into an $\eta$-free version as long as the category in question inherits a natural notion of display map (which is generally induced directly from the underlying category of types/contexts). Similarly, a strongly homotopy initial object is "weakly preserved" by a functor if its image under that functor is another strongly homotopy initial object (not necessarily the "chosen" such object in the codomain of the functor, if there is one). Weak stability then means that pullback functors weakly preserve the relevant SHIOs. I think this is as close to a "general pattern" as you can get.

Source Link
Mike Shulman
  • 66.7k
  • 7
  • 162
  • 368

I'm not sure exactly what you're asking, but the general pattern for "positive" types is to assert that every "structured" display map over the type has a specified structured section. This matches the induction principle of a positive type former in type theory. One then needs to require a sort of "pullback-stability" condition as well in order to model substitution in type theory. A forthcoming paper of Lumsdaine and Warren will describe a general process of "strictification" of "weakly stable" structure in a comprehension category into "strictly coherent" structure in a fully strict structure.

For identity types, the categorical structure is essentially a well-behaved weak factorization system in which the display maps are (or generate) the right class: see for instance this paper.