Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorAli Caglayan
   • CommentTimeOct 31st 2018
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItexIn the context of CwF how are universes modelled?

   In the context of CwF how are universes modelled?

2. • CommentRowNumber2.
   • CommentAuthorpcapriotti
   • CommentTimeOct 31st 2018
   • PermaLink
   Author: pcapriotti
   Format: MarkdownItexA universe can be defined to just be a pair $(U, El)$, where $U$ is a type over the terminal object, and $El$ a type over $1.U$. Of course, such a universe is not very useful, as it is not assumed to be closed under type-formers. However, one can prove that a universe determines a new CwF structure on the same category. Define $Ty^U(\Gamma)$ to be the set of morphisms $\Gamma \to 1.U$, and $Tm^U(\Gamma)$ the set of morphisms $\Gamma \to 1.U.El$. Furthermore, the identity functor can be extended to a CwF morphism from this new structure to the original one. Now, if the original CwF has a $\Pi$-type structure, you can ask that the CwF structure induced by $U$ also has a $\Pi$-type structure, and that the corresponding morphism preserves it (i.e. it is a morphism of CwFs-with-$\Pi$-types). This gives a definition of a "universe closed under $\Pi$-types".

   A universe can be defined to just be a pair $(U, El)$, where $U$ is a type over the terminal object, and $El$ a type over $1.U$. Of course, such a universe is not very useful, as it is not assumed to be closed under type-formers.

   However, one can prove that a universe determines a new CwF structure on the same category. Define $Ty^U(\Gamma)$ to be the set of morphisms $\Gamma \to 1.U$, and $Tm^U(\Gamma)$ the set of morphisms $\Gamma \to 1.U.El$. Furthermore, the identity functor can be extended to a CwF morphism from this new structure to the original one.

   Now, if the original CwF has a $\Pi$-type structure, you can ask that the CwF structure induced by $U$ also has a $\Pi$-type structure, and that the corresponding morphism preserves it (i.e. it is a morphism of CwFs-with-$\Pi$-types). This gives a definition of a “universe closed under $\Pi$-types”.

3. • CommentRowNumber3.
   • CommentAuthorAli Caglayan
   • CommentTimeOct 31st 2018
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItexIs it possible to model a cumulative hierarchy of universes? What about things like type families?

   Is it possible to model a cumulative hierarchy of universes? What about things like type families?

4. • CommentRowNumber4.
   • CommentAuthorspitters
   • CommentTimeOct 31st 2018
   • PermaLink
   Author: spitters
   Format: MarkdownItexThere's also Coquand's definition of [CwU]( https://www.cse.chalmers.se/~coquand/presheaf.pdf) which we also used in our work on [modal type theory](https://arxiv.org/abs/1804.05236). Coquand's notion is stricter then the usual notion and can be interpreted in sheaf categories.

   There’s also Coquand’s definition of CwU which we also used in our work on modal type theory. Coquand’s notion is stricter then the usual notion and can be interpreted in sheaf categories.

5. • CommentRowNumber5.
   • CommentAuthorspitters
   • CommentTimeOct 31st 2018
   • PermaLink
   Author: spitters
   Format: MarkdownItexAnd some more references at [universe](https://ncatlab.org/homotopytypetheory/show/universe).

   And some more references at universe.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeOct 31st 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexIn a CwF, every "term" (element of the presheaf $Tm$) has a unique "type" (element of the presheaf $Ty$), so I think it doesn't really make sense for it to directly model cumulative universes where the *same* term $A$ belongs to both $U_i$ and $U_{i+1}$. (Similarly, since no element of $Tm$ is also an element of $Ty$, it doesn't really make sense for it to model Russell universes, only Tarski ones.) My current opinion (which could change again) is that cumulative universes and Russell universes should be regarded as sugary syntax, like un-annotated lambdas, which get automatically fully-annotated by a typechecking algorithm before being passed to an initiality theorem.

   In a CwF, every “term” (element of the presheaf $Tm$) has a unique “type” (element of the presheaf $Ty$), so I think it doesn’t really make sense for it to directly model cumulative universes where the same term $A$ belongs to both $U_i$ and $U_{i+1}$. (Similarly, since no element of $Tm$ is also an element of $Ty$, it doesn’t really make sense for it to model Russell universes, only Tarski ones.) My current opinion (which could change again) is that cumulative universes and Russell universes should be regarded as sugary syntax, like un-annotated lambdas, which get automatically fully-annotated by a typechecking algorithm before being passed to an initiality theorem.

7. • CommentRowNumber7.
   • CommentAuthorkyod
   • CommentTimeOct 31st 2018
   • PermaLink
   Author: kyod
   Format: MarkdownItexI would expect that cumulativity concerns types $A \to 1$ (and more generally $\Gamma . A \to \Gamma$, arrows obtained by pulling-back $El : Tm \to Ty$ along a representable) rather than "term" $A \in \tilde U_i$. In that context "$\Gamma \vdash A$ is at level $i$" would mean that the morphism $A : y\Gamma \to Ty$ factors through $U_i$ (in the CwF), or alternatively that $\Gamma . A \to \Gamma$ is a pullback of $El_i : \tilde U_i \to U_i$. Cumulativity could be stated as $U_i \to 1$ and $El_i : \tilde U_i \to U_i$ being pullbacks of $El_{i+1} : \tilde U_{i+1} \to U_{i+1}$, no ?

   I would expect that cumulativity concerns types $A \to 1$ (and more generally $\Gamma . A \to \Gamma$, arrows obtained by pulling-back $El : Tm \to Ty$ along a representable) rather than “term” $A \in \tilde U_i$.

   In that context “$\Gamma \vdash A$ is at level $i$” would mean that the morphism $A : y\Gamma \to Ty$ factors through $U_i$ (in the CwF), or alternatively that $\Gamma . A \to \Gamma$ is a pullback of $El_i : \tilde U_i \to U_i$.

   Cumulativity could be stated as $U_i \to 1$ and $El_i : \tilde U_i \to U_i$ being pullbacks of $El_{i+1} : \tilde U_{i+1} \to U_{i+1}$, no ?

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeOct 31st 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI really do think cumulativity is a statement about terms belonging to a universe. There is no syntactic way to say "$A$ is at level $i$" other than "$A$ is a term in the $i$th universe". > Cumulativity could be stated as $U_i \to 1$ and $El_i : \tilde U_i \to U_i$ being pullbacks of $El_{i+1} : \tilde U_{i+1} \to U_{i+1}$, no ? But "being a pullback of" is not a mere property; you have to specify a pullback square. That structure then corresponds to an explicit "lifting" operator in the syntax, which is not what people usually mean by "cumulative".

   I really do think cumulativity is a statement about terms belonging to a universe. There is no syntactic way to say “$A$ is at level $i$” other than “$A$ is a term in the $i$th universe”.

   Cumulativity could be stated as $U_i \to 1$ and $El_i : \tilde U_i \to U_i$ being pullbacks of $El_{i+1} : \tilde U_{i+1} \to U_{i+1}$, no ?

   But “being a pullback of” is not a mere property; you have to specify a pullback square. That structure then corresponds to an explicit “lifting” operator in the syntax, which is not what people usually mean by “cumulative”.

9. • CommentRowNumber9.
   • CommentAuthorkyod
   • CommentTimeOct 31st 2018
   • PermaLink
   Author: kyod
   Format: MarkdownItexFair enough. I am happy with an explicit "lifting" operator in the AST of the compiler, and letting the compiler (or the human reader) elaborate these for me (so that render them as sugar syntax as you pointed out).

   Fair enough. I am happy with an explicit “lifting” operator in the AST of the compiler, and letting the compiler (or the human reader) elaborate these for me (so that render them as sugar syntax as you pointed out).

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 31st 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhich does raise the question of how that elaboration should happen. Does anyone know, is there an algorithm in the literature for compiling Russell universes into Tarski ones and cumulative universes into non-cumulative ones, analogous to bidirectional typechecking algorithms that can automatically annotate abstractions?

    Which does raise the question of how that elaboration should happen. Does anyone know, is there an algorithm in the literature for compiling Russell universes into Tarski ones and cumulative universes into non-cumulative ones, analogous to bidirectional typechecking algorithms that can automatically annotate abstractions?

11. • CommentRowNumber11.
    • CommentAuthorAli Caglayan
    • CommentTimeOct 31st 2018
    • PermaLink
    Author: Ali Caglayan
    Format: MarkdownItex@Mike supposedly [this](http://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf) says that Russels can be modelled with Tarski ones. This is done by taking lifts as coercions. I don't know so much about modelling coercions however.

    @Mike supposedly this says that Russels can be modelled with Tarski ones. This is done by taking lifts as coercions. I don’t know so much about modelling coercions however.

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeOct 31st 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThanks; but there are no details there, only a few lines sketching the translation and a "claim" that it works. I'd like to see a full proof/implementation translating a Russell/cumulative theory into a Tarski/lifting theory.

    Thanks; but there are no details there, only a few lines sketching the translation and a “claim” that it works. I’d like to see a full proof/implementation translating a Russell/cumulative theory into a Tarski/lifting theory.

13. • CommentRowNumber13.
    • CommentAuthorkyod
    • CommentTimeOct 31st 2018
    • PermaLink
    Author: kyod
    Format: MarkdownItex@Mike I don't know any actual algorithm that I could name but you can probably adapt the bidirectional algorithm. In checking mode, you have a judgement $\Gamma \vdash T \Leftarrow A in i \hookrightarrow S : A in j$ that takes as input the context $\Gamma$, the term $T$ the type $A$ and a lower bound $i$ on the universe level and outputs the elaboration $S$ of the term $T$ (with explicit coercions) and the actual universe level $j$. In synthetizing mode you have a judgement $\Gamma \vdash T \Rightarrow S : A in i$ where $\Gamma$ and $T$ are inputs, $S$, $A$ and $i$ outputs. You introduce coercions at the phase change step $$\frac{\Gamma \vdash T \Rightarrow S : A in i\qquad \Gamma \vdash A in i \equiv B in j \hookrightarrow k}{\Gamma \vdash T \Leftarrow B in j \hookrightarrow coe_i^k S : coe_i^k B in k}$$ The conversion judgement $\Gamma \vdash A in i \equiv B in j \hookrightarrow k$ should ensure that $k$ is an upper bound of $i$ and $j$. I have written $B in j$ to mean the type $B$ seen as an element of $U_j$. Is that the kind of algorithm you are looking for ?

    @Mike I don’t know any actual algorithm that I could name but you can probably adapt the bidirectional algorithm. In checking mode, you have a judgement $\Gamma \vdash T \Leftarrow A in i \hookrightarrow S : A in j$ that takes as input the context $\Gamma$, the term $T$ the type $A$ and a lower bound $i$ on the universe level and outputs the elaboration $S$ of the term $T$ (with explicit coercions) and the actual universe level $j$. In synthetizing mode you have a judgement $\Gamma \vdash T \Rightarrow S : A in i$ where $\Gamma$ and $T$ are inputs, $S$, $A$ and $i$ outputs. You introduce coercions at the phase change step

    $$\frac{\Gamma \vdash T \Rightarrow S : A in i\qquad \Gamma \vdash A in i \equiv B in j \hookrightarrow k}{\Gamma \vdash T \Leftarrow B in j \hookrightarrow coe_i^k S : coe_i^k B in k}$$

    The conversion judgement $\Gamma \vdash A in i \equiv B in j \hookrightarrow k$ should ensure that $k$ is an upper bound of $i$ and $j$.

    I have written $B in j$ to mean the type $B$ seen as an element of $U_j$. Is that the kind of algorithm you are looking for ?

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeOct 31st 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, that's the sort of thing I'd like to see written out in detail.

    Yes, that’s the sort of thing I’d like to see written out in detail.