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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology 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.
   • CommentAuthornLab edit announcer
   • CommentTimeMay 30th 2021
   • PermaLink
   Author: nLab edit announcer
   Format: MarkdownItexPage created, but author did not leave any comments. Anonymous <a href="https://ncatlab.org/nlab/revision/quotient+inductive+type/1">v1</a>, <a href="https://ncatlab.org/nlab/show/quotient+inductive+type">current</a>

   Page created, but author did not leave any comments.

   Anonymous

   v1, current

2. • CommentRowNumber2.
   • CommentAuthorjonsterling
   • CommentTimeMay 11th 2022
   • (edited May 11th 2022)
   • PermaLink
   Author: jonsterling
   Format: MarkdownItexIs it in fact true that the actual partial map classifier is this free omega-cpo? I don't think that is actually what is proved by the cited paper (<https://arxiv.org/pdf/1610.09254.pdf>). What they define in that paper is the free pointed $\omega$-cpo on a type. But the free pointed omega-cpo on a type in the sense of this paper need not be that type's partial map classifier, although I believe in SET they coincide. In particular, the partial map classifier of a type is **always** directed-complete but I think this free $\omega$-cpo (which they define as a kind of free cocompletion under $\omega$-chains and a bottom element) is probably not directed-complete unless I am missing something. If I wanted to show that the actual partial map classifier was the free pointed omega-cpo, I would need to show (in particular) for any two strict omega-continuous maps $h, h' : Lift(A) \to X$, we have $h=h'$ if they agree when restricted to $A$. I would think that to prove this, I would show every element $x:Lift(A)$ is a colimit that is preserved by $h,h'$. The diagram in question is indexed in $1 + \{* \mid x{\downarrow}\}$, and given by the inequality $\bot \leq \eta(x!)$. It is important that the points of this diagram are either $\bot$ or lie in the image of the unit $\eta:A\to Lift(A)$. Such a diagram could be presented by an $\omega$-chain if the law of the excluded middle held, but I don't see how to do it otherwise.

   Is it in fact true that the actual partial map classifier is this free omega-cpo? I don’t think that is actually what is proved by the cited paper (https://arxiv.org/pdf/1610.09254.pdf).

   What they define in that paper is the free pointed $\omega$-cpo on a type. But the free pointed omega-cpo on a type in the sense of this paper need not be that type’s partial map classifier, although I believe in SET they coincide. In particular, the partial map classifier of a type is always directed-complete but I think this free $\omega$-cpo (which they define as a kind of free cocompletion under $\omega$-chains and a bottom element) is probably not directed-complete unless I am missing something.

   If I wanted to show that the actual partial map classifier was the free pointed omega-cpo, I would need to show (in particular) for any two strict omega-continuous maps $h, h' : Lift(A) \to X$, we have $h=h'$ if they agree when restricted to $A$. I would think that to prove this, I would show every element $x:Lift(A)$ is a colimit that is preserved by $h,h'$. The diagram in question is indexed in $1 + \{* \mid x{\downarrow}\}$, and given by the inequality $\bot \leq \eta(x!)$. It is important that the points of this diagram are either $\bot$ or lie in the image of the unit $\eta:A\to Lift(A)$. Such a diagram could be presented by an $\omega$-chain if the law of the excluded middle held, but I don’t see how to do it otherwise.

3. • CommentRowNumber3.
   • CommentAuthorjonsterling
   • CommentTimeMay 11th 2022
   • (edited May 11th 2022)
   • PermaLink
   Author: jonsterling
   Format: MarkdownItexIt seems that it might be possible to repair the claim if $\omega$ were replaced by some completion, such as the "upper naturals". In fact, I would say that the correct definition of an $\omega$-cpo in a topos is _not_ given using the natural numbers object, but are instead defined by iterating the real partial map classifier as in the work of Marcelo Fiore, Gordon Plotkin and John Power <https://homepages.inf.ed.ac.uk/gdp/publications/Cuboidal.pdf>. In particular, in SET it just so happens that the partial map classifier is $-+1$, so if you take the initial algebra of this functor you get $\mathbb{N}$. This does not happen in an arbitrary topos; the correct figure shape for an "$\omega$-chain" is obtained by considering the initial algebra for the real partial map classifier functor.

   It seems that it might be possible to repair the claim if $\omega$ were replaced by some completion, such as the “upper naturals”. In fact, I would say that the correct definition of an $\omega$-cpo in a topos is not given using the natural numbers object, but are instead defined by iterating the real partial map classifier as in the work of Marcelo Fiore, Gordon Plotkin and John Power https://homepages.inf.ed.ac.uk/gdp/publications/Cuboidal.pdf.

   In particular, in SET it just so happens that the partial map classifier is $-+1$, so if you take the initial algebra of this functor you get $\mathbb{N}$. This does not happen in an arbitrary topos; the correct figure shape for an “$\omega$-chain” is obtained by considering the initial algebra for the real partial map classifier functor.

4. • CommentRowNumber4.
   • CommentAuthorjonsterling
   • CommentTimeJul 12th 2022
   • PermaLink
   Author: jonsterling
   Format: MarkdownItexRemove false claim that the partial map classifier coincides with the free pointed omega-cpo in HoTT. <a href="https://ncatlab.org/nlab/revision/diff/quotient+inductive+type/12">diff</a>, <a href="https://ncatlab.org/nlab/revision/quotient+inductive+type/12">v12</a>, <a href="https://ncatlab.org/nlab/show/quotient+inductive+type">current</a>

   Remove false claim that the partial map classifier coincides with the free pointed omega-cpo in HoTT.

   diff, v12, current

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeJul 14th 2022
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe page [[partial map classifier]] also contains the same false claim. Perhaps it would be worth mentioning at both of these pages that there is more than one notion of "partial map", which I think is the source of the confusion. The rest of the page [[partial map classifier]] is about classifiers for the topos-theoretic notion of partial map, where the domain can be an arbitrary subobject, whereas the ADK paper is about a more computational notion of partial map, where the domain is a "computable" subobject and hence can be expected to be characterized in countable terms. Does that seem right to you?

   The page partial map classifier also contains the same false claim.

   Perhaps it would be worth mentioning at both of these pages that there is more than one notion of “partial map”, which I think is the source of the confusion. The rest of the page partial map classifier is about classifiers for the topos-theoretic notion of partial map, where the domain can be an arbitrary subobject, whereas the ADK paper is about a more computational notion of partial map, where the domain is a “computable” subobject and hence can be expected to be characterized in countable terms. Does that seem right to you?

6. • CommentRowNumber6.
   • CommentAuthorjonsterling
   • CommentTimeJul 14th 2022
   • (edited Jul 14th 2022)
   • PermaLink
   Author: jonsterling
   Format: MarkdownItexOh boy... Thank you for noticing that, Mike! I think I agree with your proposed fix, but even if we do that that I feel there is a "missing proof" that this HIT construction actually gives rise to a dominance for which it is **the** partial map classifier. One thing that is leading to confusion here is that this HIT construction is about constructing a pointed omega-cpo in the **order-theoretic** sense --- meaning that the corresponding dominance would be a dominance on the category of (not-necessarily-pointed) omega-cpos, rather than on the category of types (sets, etc.) in which this thing is computed. So this is opening up a big can of worms, and I am wondering if it would be better to simpler **delete** this HIT from the [[partial map classifier]] page, and keep the example on [[quotient inductive type]] only.

   Oh boy… Thank you for noticing that, Mike! I think I agree with your proposed fix, but even if we do that that I feel there is a “missing proof” that this HIT construction actually gives rise to a dominance for which it is the partial map classifier.

   One thing that is leading to confusion here is that this HIT construction is about constructing a pointed omega-cpo in the order-theoretic sense — meaning that the corresponding dominance would be a dominance on the category of (not-necessarily-pointed) omega-cpos, rather than on the category of types (sets, etc.) in which this thing is computed. So this is opening up a big can of worms, and I am wondering if it would be better to simpler delete this HIT from the partial map classifier page, and keep the example on quotient inductive type only.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeJul 14th 2022
   • PermaLink
   Author: Urs
   Format: MarkdownItexSince you kept the exact same reference that the Anonymous OP thought proves the claim you say is wrong, maybe good to be more specific about what that reference really claims. I assume it's about section 3.2 there? I have added ([here](https://ncatlab.org/nlab/show/quotient+inductive+type#FreePointedOmegaCompletePartialOrders)) that pointer (and also added publication data and fixed the publication year), so now the pointer reads [Altenkirch, Danielsson, and Kraus 2017, §3.2](https://ncatlab.org/nlab/show/quotient+inductive+type#ADK2017). <a href="https://ncatlab.org/nlab/revision/diff/quotient+inductive+type/13">diff</a>, <a href="https://ncatlab.org/nlab/revision/quotient+inductive+type/13">v13</a>, <a href="https://ncatlab.org/nlab/show/quotient+inductive+type">current</a>

   Since you kept the exact same reference that the Anonymous OP thought proves the claim you say is wrong, maybe good to be more specific about what that reference really claims. I assume it’s about section 3.2 there? I have added (here) that pointer (and also added publication data and fixed the publication year), so now the pointer reads Altenkirch, Danielsson, and Kraus 2017, §3.2.

   diff, v13, current