Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

November 29, 2011

Internalizing the External, or The Joys of Codiscreteness

Posted by Mike Shulman

This post is essentially a summary of a long discussion between Urs and myself about axiomatizing cohesive (,1)(\infty,1)-toposes in homotopy type theory. But it should be accessible and interesting even if you don’t care about cohesive (,1)(\infty,1)-toposes. I think it yields interesting general conclusions about internalization, type theory, higher modal logic, and the importance of codiscreteness.

Note that practically everything I’m going to say below has been formalized in Coq, and it can be found here.

Suppose we have a forgetful functor U:HSU\colon H \to S, and we want to speak about properties of this functor without “leaving the world of HH”. (The example I particularly have in mind is when S=SetsS=Sets or Gpd\infty Gpd and UU is the direct image functor of the global-sections geometric morphism for a topos or (,1)(\infty,1)-topos.) A clear prerequisite for this is that we can somehow recover SS from data in or on HH, and an obvious way to do this is to assume that UU has either a monadic right adjoint or a comonadic left adjoint. For various reasons, including simplicity, let’s restrict to the case when these adjoints are fully faithful (so they equip HH with “discrete objects” or “codiscrete objects” in the sense used in my last post). Then it’s easy to describe SS and UU purely in terms of data on HH: we simply specify a reflective or coreflective subcategory.

However, now suppose we want to describe this in the internal logic of HH. Roughly speaking, the internal logic is a way of speaking about objects as if they were sets or spaces with “elements”, together with a way to “interpret” or “compile” such language into statements about HH in the usual language of category theory that uses generalized elements. For instance, an assertion in the internal language such as “for any xAx\in A and yBy\in B, there exists a unique (x,y)A×B(x,y)\in A\times B such that …” compiles to the usual definition of a cartesian product: “for any x:UAx\colon U\to A and y:UBy\colon U\to B, there exists a unique (x,y):UA×B(x,y)\colon U\to A\times B such that … “.

In the internal logic of HH, therefore, the objects of HH act like sets (if HH is a 1-topos) or \infty-groupoids (if HH is an (,1)(\infty,1)-topos). The internal logic of a 1-topos is sometimes called its Mitchell-Benabou language, while the internal logic of an (,1)(\infty,1)-topos is (conjecturally) homotopy type theory. From now on, I’ll use the language of the latter; so for instance “type” should be read as referring to an object of HH. (I’ll also slip into the implicit ∞-category theory convention, just because it would be way too cumbersome otherwise.)

Now how do we describe a reflective or coreflective subcategory internally? In the obvious approach, we just say what it means to belong to the subcategory, plus have an operation on the types which serves as the reflector/coreflector, together with a unit/counit satisfying a suitable universal property. In the reflective case, this means we have something like the following axioms.

  • A:TypeinRsc(A):Prop A\colon Type \vdash inRsc(A) \colon Prop . This says that for any type AA, we have a proposition inRsc(A)inRsc(A) (expressing the assertion that AA is in our putative reflective subcategory).
  • A:TypeA:Type A\colon Type \vdash \sharp A \colon Type . This says that for any AA, we have another type A\sharp A (its reflection into the subcategory).
  • A:TypeinRsc(A) A \colon Type \vdash inRsc(\sharp A) . This says that for any AA, the type A\sharp A is in the subcategory.
  • A:Typeη A:AA A \colon Type \vdash \eta_A \colon A \to \sharp A . This says that for any AA, we have a map η A:AA\eta_A \colon A \to \sharp A.
  • A,B:Type,inRsc(B)isEquiv(λg.gη A) A,B \colon Type, inRsc(B) \vdash isEquiv( \lambda g.\; g\circ \eta_A ) . This says that for any types AA and BB, where BB is in the subcategory, precomposing with η A\eta_A yields an equivalence between B AB^{\sharp A} and B AB^A.

However, assuming that our type theory has dependent types, an operation on types specified in the internal logic in this way actually gives us more than merely an operation on objects of HH (which is what we had in mind). This is because any operation we have in type theory can automatically be applied in any context. Hence, not only can we say that for every type AA, we have a type A\sharp A, we can also say that for any dependent type x:AP(x):Type x\colon A \vdash P(x) \colon Type we have another dependent type x:AP(x):Type. x\colon A \vdash \sharp P(x) \colon Type. Since dependent types over AA represent objects in the slice category H/AH/A, a type-theoretic operation \sharp actually gives us an operation on every slice category of HH. This should make sense in terms of the vague description of the internal logic I gave above, once you realize that if a “generalized element of AA at stage UU” means a morphism UAU\to A, then a “generalized object of the category at stage UU” can only mean an object of the slice category H/UH/U.

Moreover, this operation on slice categories commutes with pullback, since the pullback of P\sharp P along f:BAf\colon B\to A and the \sharp-image of the pullback of PP along ff are both represented by the same dependent type: y:BP(f(y)):Type y \colon B \vdash \sharp P(f(y)) \colon Type. If we additionally add axioms which appear to say that this operation a reflection or coreflection (as I did above for a reflection), then we are actually describing a reflective or coreflective subcategory of every slice category, for which the (co)reflector commutes with pullback – a (co)reflective subfibration of the codomain fibration.

So how can we eliminate this extra data and get back to talking about a reflective or coreflective subcategory of HH itself? In the coreflective case, we’re pretty sunk (I’ll get back to that case later), but in the reflective case, there is a close relationship between reflective subcategories and reflective subfibrations.

  1. Every reflective subcategory (subject to certain adjoint-functor-theorem-y conditions) gives rise to a factorization system (E,M)(E,M), in which EE is the class of maps inverted by the reflector \sharp, and the reflective subcategory is identified with M/1M/1. The factorization systems which arise from reflective subcategories in this way are precisely those for which EE satisfies two-out-of-three (in which case, of course, the reflective subcategory is the localization at EE); these are called reflective factorization systems.

  2. Every factorization system (E,M)(E,M) gives rise to a pullback-stable system of reflective subcategories of slice categories: the subcategory of H/xH/x is M/xM/x, with the (E,M)(E,M)-factorization being the reflection. A pullback-stable system of reflective subcategories C xH/xC^x \subseteq H/x arises from a factorization system in this way precisely when MM, the class of morphisms f:xyf\colon x\to y which are objects of C xC^x, is closed under composition. The reflectors also commute with pullback (giving a reflective subfibration) precisely when the factorization system itself is pullback-stable.

  3. A reflective factorization system is stable precisely when its corresponding reflective subcategory has a left-exact reflector.

A couple of good references to learn about this stuff are given at the bottom of this page. Thus, we have a diagram of inclusions: reflective subcategories factorization systems systems of reflective subcategories lex-reflective subcategories stable factorization systems reflective subfibrations \array{ \text{reflective subcategories} & \to & \text{factorization systems} & \to & \text{systems of reflective subcategories}\\ \uparrow & & \uparrow & & \uparrow\\ \text{lex-reflective subcategories}& \to & \text{stable factorization systems} & \to & \text{reflective subfibrations} } Recall that the naive internal axioms, which look as though they are describing a reflective subcategory, actually describe a reflective subfibration. Thus, we can augment them to actually describe a lex-reflective subcategory by imposing further axioms ensuring that MM is closed under composition and that EE satisfies two-out-of-three.

It turns out that internally, the class MM consists of the morphisms PAP\to A which represent dependent types x:AP(x):Typex\colon A \vdash P(x) \colon Type for which x,inRsc(P(x))\forall x, inRsc(P(x)). One can prove from this that MM will be closed under composition just when, internally, the types for which inRsc(B)inRsc(B) are closed under dependent sums:

inRsc(A),x.inRsc(P(x))inRsc( x:AP(x)) inRsc(A), \forall x. inRsc(P(x)) \vdash inRsc \left(\sum_{x\colon A} P(x)\right)

Similarly, EE can be characterized internally as the morphisms which represent dependent types x:AP(x):Typex\colon A \vdash P(x) \colon Type for which each P(x)\sharp P(x) is contractible. One can prove from this that EE satisfies two-out-of-three just when, internally, for any map f:ABf\colon A\to B where A\sharp A and B\sharp B are contractible, so is the \sharp of all homotopy fibers of ff.

isContr(A),isContr(B),f:AB,b:BisContr(hFiber(f,b)) isContr(\sharp A), isContr(\sharp B), f\colon A\to B, b\colon B \vdash isContr(\sharp hFiber(f,b))

This last condition is a special case of saying that \sharp preserves pullbacks, and from it one can prove internally that \sharp preserves all pullbacks – that is, the reflector is lex. In fact, though, even without these latter two conditions, there is a certain amount of lex-ness even to the notion of reflective subfibration. For since the reflector commutes with pullback, so do their right adjoints: the inclusions of the fiberwise subcategories and dependent products. This implies in particular that M/1M/1 is an exponential ideal, and hence \sharp must preserve finite products.

The closure of the subcategory under dependent sums is a somewhat more mysterious condition. However, it admits a very pleasing reformulation. Notice that one consequence of the axiom asserting the universal property of η A\eta_A is that we can factor through it:

  • f:AB,inRsc(B)fact(f):AB f\colon A\to B, inRsc(B) \vdash fact(f)\colon \sharp A \to B . This says that if BB is in the subcategory and f:ABf\colon A\to B, then we have another map fact(f):ABfact(f)\colon \sharp A \to B.
  • f:AB,inRsc(B),a:Afact(f)(η A(a))=f f\colon A\to B, inRsc(B), a\colon A \vdash fact(f)(\eta_A(a)) = f . This says that for A,BA,B and ff as above, and any a:Aa\colon A, we have fact(f)(η A(a))=ffact(f)(\eta_A(a)) = f.

This looks a lot like the “elimination rule” of an inductively defined type, a common notion in type theory. In general, when a type TT is inductively defined by certain constructors, it means that we have various ways to construct elements of TT (perhaps taking as input other elements of TT), and moreover if we have any other type BB together with similar ways to construct elements of BB, there is a specified map from TT to BB preserving the constructors. For instance, the natural numbers are inductively defined by two constructors 0:0\colon \mathbb{N} and s:s\colon \mathbb{N}\to \mathbb{N}.

Here, we seem to be sort-of saying that A\sharp A is inductively defined by η A:AA\eta_A\colon A\to \sharp A, together with a certain vague “sharpness”. In particular, it has an eliminator saying that if BB has a similar constructor f:ABf\colon A\to B together with the same sort of “sharpness” (that is, inRsc(B)inRsc(B)), then we have a specified map fact(f):ABfact(f)\colon \sharp A\to B preserving the constructor η A\eta_A (evidently “preserving sharpness” is a vacuous condition, which makes sense since our subcategory is full).

However, in dependent type theory, inductive types generally also come with dependent eliminators, in which the target type BB is allowed to depend on the inductive type TT. For instance, for the natural numbers this eliminator says that given a dependent type n:B(n):Typen\colon \mathbb{N}\vdash B(n) \colon Type together with an element z B:B(0)z_B\colon B(0) and for every nn an operation s B:B(n)B(s(n))s_B \colon B(n) \to B(s(n)), we have a specified section f:n,B(n)f \colon \forall n, B(n) such that f(0)=z Bf(0)= z_B and s B(f(n))=f(s(n))s_B(f(n)) = f(s(n)). One value of the dependent eliminators is that they allow us to prove uniqueness (up to equality, i.e. paths in homotopy theory) of the morphisms specified by the non-dependent eliminator, by using the dependent eliminator into an equality/path type.

A natural dependent eliminator for \sharp would be the following. Suppose a:AB(a)a\colon \sharp A \vdash B(a) is a type dependent on A\sharp A, suppose we have a section f:a:A,B(η A(a))f\colon \forall a\colon A, B(\eta_A(a)) over AA, and suppose that x:A,inRsc(B(x))\forall x\colon \sharp A, inRsc(B(x)). Then we have a specified section fact(f):x:A,B(x)fact(f)\colon \forall x\colon \sharp A, B(x), such that fact(f)(η A(a))=f(a)\fact(f)(\eta_A(a)) = f(a) for all a:Aa\colon A.

Here’s the lovely fact: a reflective subfibration \sharp has a dependent eliminator if and only if the inRscinRsc objects are closed under dependent sums, i.e. it is a factorization system. If we have closure under sums, then we can use the non-dependent eliminator to define a map A x:AB(x)A\to \sum_{x\colon \sharp A} B(x) and nudge it so it becomes a section of BB; while conversely we can define an inverse to η Σ xB(x)\eta_{\Sigma_x B(x)} using the dependent eliminator. Moreover, if we assume that the subcategory is closed under equality/path types, then the dependent eliminator implies not just the non-dependent eliminator (which is obvious) but also its universal property (by eliminating into an equality type).

This gives a very type-theoretic style of thinking about \sharp, which is also very convenient for proving things about sharped objects. We can write convenient tactics in Coq which automatically apply the dependent eliminator and its computation rules to reduce everything to statements about unsharped objects. In a sense, it’s saying that we have a higher-categorical sort of modality: one which acts on objects as well as on propositions. This shouldn’t be too surprising; we know that lex-reflective subcategories of a 1-topos are equivalent to Lawvere-Tierney topologies, which are a traditional sort of modality which acts on propositions. In homotopy type theory, we need to use higher modalities which act on objects because not every sub-(,1)(\infty,1)-topos is a topological localization.

I hope that the foregoing has convinced you that codiscrete objects admit a very nice and convenient axiomatization in the internal logic. Unfortunately, discrete objects don’t admit nearly so nice a description, because the internal logic doesn’t let us dualize the slice categories into co-slices when we want to dualize reflectiveness into coreflectiveness. I don’t know of any general way to construct a coreflective subfibration.

However, if we have codiscrete objects, then they give us a solution for dealing with the discrete objects! Namely, we already have the category SS sitting inside HH as the codiscrete objects, with the functor U:HSU\colon H\to S represented by the reflector \sharp. Thus, we can talk “in SS” “about HH” and still remain inside HH, if we do all of our talking inside the codiscrete objects.

The main player in this approach is Type\sharp Type. Here TypeType is the (or, rather, a) type of types, which represents an object classifier in category theory. You can think of it as like a Grothendieck universe of sorts; but remember that we want it to satisfy the univalence axiom. Thus, Type\sharp Type is the object of SS underlying TypeType – which we can think of as the “external space of objects of HH” – included back into HH as a codiscrete object. The functoriality of \sharp (and the fact that it preserves products) means that any operation on types, which is described in type theory by a function on TypeType, gives rise to a corresponding “externalized” function on Type\sharp Type. For instance, the internal-hom, which takes two types A and B and gives the function-type A -> B, is represented by a function Type×TypeTypeType \;\times\; Type \to Type, and hence gives us a function Type×TypeType\sharp Type \;\times\; \sharp Type \to \sharp Type.

Something is still missing, though. The function Type×TypeType\sharp Type \;\times\; \sharp Type \to \sharp Type is an externalization of the internal-hom operation, which takes two objects of HH and gives us a third object of HH. However, what we really want (in order to talk about HH “externally”) is the external hom, which takes two objects of HH and gives us an object of SS! Thus we need an operation TypeType\sharp Type \to Type which “escapes” from the external world, in a sense, and which should be a version of \sharp itself (since the external-hom is UU applied to the internal-hom).

Magically, we have just such an operation. Recall that the object classifier TypeType comes with a universal map Type˜Type\widetilde{Type} \to Type, of which every (small) map is a pullback in an essentially unique way. The functor \sharp applied to this gives us a map Type˜Type\sharp\widetilde{Type} \to \sharp Type, which therefore has a classifying map escape:TypeTypeescape \colon \sharp Type \to Type. It’s an easy exercise in pasting pullback squares, using the fact that \sharp preserves pullbacks, to show that the composite Typeη TypeTypeescapeTypeType \xrightarrow{\eta_{Type}} \sharp Type \xrightarrow{escape} Type is equivalent to :TypeType\sharp\colon Type \to Type itself. Thus, escape really is “a version of sharp”, and it lets us define the external hom Type×TypeType\sharp Type \;\times\; \sharp Type \to Type by composing the “externalized internal-hom” with escape.

This works amazingly well. In particular, it allows us to express the coreflector for the discrete objects in terms of an operation :TypeType\flat\colon \sharp Type \to \sharp Type, state its universal property, and prove useful things about it. It’s more cumbersome than working purely internally, of course, but as we get more practice we’ll write more helpful tactics and it will get easier. It’s just as easy to additionally assert that the discrete objects are also reflective, with reflector Π\Pi that preserves finite products, thereby obtaining the original desired axiomatization of cohesive (,1)(\infty,1)-toposes. The axiomatization that I’m now satisfied with can be found here.

Let me finish by saying a bit about what we can do if we don’t have codiscrete objects. Remember from last time that there is a universal way to add codiscrete objects, by constructing the scone on a (lex) functor U:HSU\colon H\to S. Thus, if we want to talk about such a functor using internal logic, we can first construct its scone, which contains SS as a lex-reflective subcategory of codiscrete objects.

Moreover, the scone also contains HH as a lex-reflective subcategory, and these two subcategories are complementary open and closed subtoposes. (An open subtopos is determined by a subterminal object PP, and its reflector is AA PA\mapsto A^P; the reflector of the complementary closed subtopos takes AA to the pushout of the two projections of A×PA\times P.) Finally, any topos equipped with a complementary pair of open and closed subtoposes can be obtained as the scone of a functor from the one to the other. Thus, if we axiomatize two lex-reflective subcategories as above and stipulate that they are complementary open and closed subtoposes, we will have an internal logic with which to talk about arbitrary lex functors between toposes. And if we furthermore require that the codiscrete objects (those in the closed subtopos) come with matching discrete ones, this corresponds to asking that UU have a lex left adjoint; thus we have an internal language with which to talk about arbitrary geometric morphisms.

Posted at November 29, 2011 4:58 PM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2466

18 Comments & 3 Trackbacks

Re: Internalizing the External, or The Joys of Codiscreteness

Thanks, Mike, this is most enjoyable!

One question about Cohesive.v:

I understand that the code there characterizes a reflective subcategory “of discrete objects” on top of (and via) the coreflective subcategory “of codiscrete objects”. But it does not yet make these two subcategories be equivalent such as to characterize cohesion proper, or does it?

I would think that there needs to be one more axiom saying that “| discrete:discretecodiscrete\sharp|_{discrete} : discrete \to codiscrete” is an equivalence.

Do you see what I mean? Am I missing some subtlety that makes this automatic now?

Posted by: Urs Schreiber on November 30, 2011 8:18 PM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

I think that’s the purpose of the axioms flat_sharp_is_equiv and sharp_flat_is_equiv here. They’re supposed to say that for any type AA, the maps AA\flat A \to \flat \sharp A and AA\sharp\flat A\to \sharp A are equivalences. I thought we decided that that was the right way to say that the discrete and codiscrete objects were equivalent and that Γ\Gamma respected that equivalence.

Posted by: Mike Shulman on November 30, 2011 11:13 PM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

here.

Ah, I didn’t look into that file!

I thought we decided

Yes, sure, we did.

Posted by: Urs Schreiber on November 30, 2011 11:27 PM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

this is very nice indeed!

The dependent rules for the \sharp-reflection are of course a (sweeping!) generalization of the bracket-types from my old-ish paper with Andrej Bauer:

which did what Mike here does for the special case of epi-mono factorizations in a 1-category. There we explicitly took the point of view that we were axiomatizing such a factorization, associated to a fibered reflective subcategory (namely monomorphisms), as a modal operator in type theory.

In the last section of the paper, we used the model operator to formulate a translation of predicate logic into type theory. We thought of this as the type-theoretic counterpart of (the\flat side of) the modal logic of local maps of toposes (in the paper with Lars Birkedal: Elementary axioms for local maps of toposes).

The idea was to give a translation of predicate logic into modal constructive logic, in the style of the G”odel translation of intuitionistic logic into modal classical logic, but of course different from that, since it works with a “diamond” operator – i.e. a monad – rather than a “box” – i.e. a comonad.

The same idea seems to be working here – of course, on a much wider range of examples. But here, too, there should be an explicit translation of the (non-modal) internal language of the topos of codiscrete objects into the modal logic of the big topos, along with a conservativity theorem for statements of a certain logical form.

Posted by: Steve Awodey on December 1, 2011 1:57 PM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

the link to the paper Propositions as [types] is:

http://andrej.com/papers/brackets_letter.pdf

Posted by: Steve Awodey on December 1, 2011 1:59 PM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

Absolutely! Thanks for pointing that out. (Effective epi, mono) is also the first example I noticed of a factorization system in this context which isn’t a lex-reflective subcategory. (In an (,1)(\infty,1)-topos, not every epi is effective, and it’s the effective ones that go into the factorization system.) There the reflector is the higher inductive type is_inhab (which is of course another incarnation of the bracket operator); see this file. The nn-truncation should also be an example for other values of nn.

Of course, is_inhab also gives us the natural way to interpret in HoTT statements of predicate logic such as “there exists” and “or”, whose type-theoretic counterparts (e.g. dependent sums and coproducts) don’t preserve h-propositions: we interpret x.ϕ(x)\exists x. \phi(x) by isInhab( xϕ(x))isInhab(\sum_x \phi(x)), and so on inductively. This amounts to constructing representing subobjects in the usual internal-logic way. But the translation you and Andrej used seems to be different than this, if I’m reading correctly — you translated using propositions-as-types and then applied the bracket operator only at the very end. Is that right?

Posted by: Mike Shulman on December 3, 2011 7:02 AM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

that’s only when translating a predicate ϕ\phi of first-order logic that’s already known to be a Prop – i.e. from predicate logic into [bracket] types. Otherwise one needs to apply the bracket inside and outside the Sigma: x.A(x)=[Σx.[A(x)]]\exists x. A(x) = [\Sigma x.[A(x)]].
Posted by: steve awodey on December 4, 2011 3:30 AM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

I was looking at page 466 where you define a map 𝕋 \mathbb{T} \xrightarrow{\star} \mathcal{E} using the propositions-as-types interpretation into type theory, which I presume means not using any bracket types. Then you proved some theorems about the single bracket [φ ][\varphi^\star]. I also see the usual interpretation of first-order logic in a Heyting category, there denoted y(φ)y(\varphi) — is that what you were referring to?

Posted by: Mike Shulman on December 4, 2011 6:14 AM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

the translation you’re looking at (in section 6) is for the purpose of proving conservativity of type theory w/o brackets over (a certain fragment of) IFOL. For the general, recursive translation of IFOL into type theory with brackets, see section 5. There, the brackets are used inside formulas to correct those FOL operations that differ from type-theoretic ones (namely, Σ\Sigma and ++).
Posted by: Steve Awodey on December 5, 2011 1:13 AM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

For the general, recursive translation of IFOL into type theory with brackets, see section 5.

Right, thanks. I was looking at section 6 because you mentioned “a conservativity theorem for statements of a certain logical form”; is that not what you had in mind there? Section 5 seems to identify all of IFOL with the corresponding bracket approach, not requiring any particular logical form.

Posted by: Mike Shulman on December 5, 2011 1:28 AM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

It would be nice now to come back to Exercise I and Exercise II and see what to do about them with the new version of the axioms.

I expect that Guillaume’s previous code for Exercise I should have a rather straightforward adaption to the new version of the \flat-operator defined here.

The content of Exercise II was mainly to deduce that \flat preserves homotopy fibers. Since we now have the external hom via \sharp, it would be interesting to first deduce more generally the external hom-isomorphism H(X,A)H(ΠX,A)\mathbf{H}(X, \flat A) \simeq \mathbf{H}(\mathbf{\Pi} X, A).

I may have time to look into such things from Wednesday on…

Posted by: Urs Schreiber on December 2, 2011 6:08 PM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

I wrote:

A natural dependent eliminator for \sharp would be the following. Suppose a:AB(a)a\colon \sharp A \vdash B(a) is a type dependent on A\sharp A, suppose we have a section f:a:A,B(η A(a))f\colon \forall a\colon A, B(\eta_A(a)) over AA, and suppose that x:A,inRsc(B(x))\forall x\colon \sharp A, inRsc(B(x)). Then we have a specified section fact(f):x:A,B(x)fact(f)\colon \forall x\colon \sharp A, B(x), such that fact(f)(η A(a))=f(a)\fact(f)(\eta_A(a)) = f(a) for all a:Aa\colon A.

Actually, as I think about this further, a more natural dependent eliminator for \sharp would require that inRsc( x:AB(x))inRsc\left(\sum_{x\colon \sharp A} B(x)\right) rather than x:A,inRsc(B(x))\forall x\colon \sharp A, inRsc(B(x)).

This matches the hypotheses of the dependent eliminator for ordinary inductive types better. For instance, the dependent eliminator for \mathbb{N} doesn’t require that every fiber B(x)B(x) is equipped with a point and an endomorphism; rather it requires that the total space n:B(n)\sum_{n\colon \mathbb{N}} B(n) is equipped with a point and and endomorphism lying over those of \mathbb{N} (thus z Bz_B lies over 0:0\colon \mathbb{N} and s Bs_B lies over s:s\colon \mathbb{N}\to\mathbb{N}). Since “sharpness” is vacuously preserved by morphisms, the corresponding hypothesis here would really be that x:AB(x)\sum_{x\colon \sharp A} B(x) “has sharpness” rather than that each fiber B(x)B(x) does.

Moreover, this more natural dependent eliminator actually holds in any reflective subfibration. It’s just that it’s not nearly so useful as the version which only requires each B(x)B(x) to lie in the subcategory, which obviously follows from it in case the subcategory is closed under dependent sums.

Posted by: Mike Shulman on December 5, 2011 6:51 AM | Permalink | Reply to this
Read the post Basic Ideas of Homotopy Axiomatic Cohesion
Weblog: The n-Category Café
Excerpt: Slides for a course on basic ideas of axiomatic cohesion in homotopy type theory.
Tracked: December 6, 2011 7:26 PM

Re: Internalizing the External, or The Joys of Codiscreteness

I have a question on the axioms for cohesive homotopy type theory and then a more general question on homotopy type theory.

First, to which extent does your code so far invoke the univalence axiom?

(I include links to this and other terms in the following for the convenience of others who might be reading this.)

More precisely, to which extent does the code depend on univalence more directly than via function extensionality?

Here the more general questions:

What is known about models for homotopy type theory without univalence, but with an interval type? I would imagine that it is considerably easier to find models for intensional type theory without univalence but with a (non-trivial) interval. Is that true?

Finally: I see type theorists raise their eyebrows when faced with the information that higher inductive types destroy “canonicity”, the fact that the computer is able to reduce all terms to normal form and thus effectively compute.

My question is: would it be correct to think of the situation as follows?:

We know that higher inductive types present concrete higher homotopy types. Hence if we were able to program a computer in such a way that it both handles higher inductive types while at the same time exhibiting “canonicity”, it would sound as if we had built a computer that can effectively compute homotopy groups, in particular of spheres. But nobody expects this to be possible. Hence nobody should be surprised that higher inductive types ruin “canonicity”.

Is this a reasonable way to think about the situation?

Posted by: Urs Schreiber on December 9, 2011 7:38 PM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

My question is: would it be correct to think of the situation as follows?:

We know that higher inductive types present concrete higher homotopy types. Hence if we were able to program a computer in such a way that it both handles higher inductive types while at the same time exhibiting “canonicity”, it would sound as if we had built a computer that can effectively compute homotopy groups, in particular of spheres. But nobody expects this to be possible. Hence nobody should be surprised that higher inductive types ruin “canonicity”.

Is this a reasonable way to think about the situation?

I don’t think so.

First of all, there is an algorithm to compute all homotopy groups of spheres (see this MO question). It’s just that the complexity of the algorithm is too big to compute many homotopy groups of spheres.

Then, canonicity does not mean that Coq will be able to compute automatically all homotopy groups of spheres (for example, we have canonicity for MLTT but this does not automatically give a program for factoring big numbers).

What canonicity means (I think) is that is you can define a closed (without environment) term t of type T, then t is definitionally equal to a constructor of T applied to something else. For example if n : nat is an arbitrary term, then (after reduction) n should be either 0 or S n' where n' : nat (with the univalence axiom this is false, we can easily construct natural numbers that are not definitionally equal to a standard natural number).

Posted by: Guillaume Brunerie on December 9, 2011 8:56 PM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

there is an algorithm to compute all homotopy groups of spheres

Ah, thanks. I wasn’t aware of that.

we have canonicity for MLTT but this does not automatically give a program for factoring big numbers

Certainly there is a simple program that factors any number: the one that simply tries all possible factors. It’s just not efficient. But it would seem to easily have an implementation in MLTT, no?

What canonicity means […]

Thanks. I have this rough understanding, too, I’d just like to get a better idea of what it means for “us in practice” if it fails. Why is it that (from the little experience I had with such people in person) traditional type theorists seem worried about losing it, while homotopy type theorist seem not to be worried? (Maybe that’s a confused question. Any reply that reduces my confusion on this point in any way is highly appreciated.)

Posted by: Urs Schreiber on December 9, 2011 9:34 PM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

to which extent does the code depend on univalence more directly than via function extensionality?

One place where I certainly used univalence is to prove that the subcategory is replete, by changing an equivalence into a path and transporting along that path. However, one could simply add repleteness as an additional axiom in the definition of a reflective subfibration.

Beyond that, there were a few uses of univalence that were just due to laziness, which I have now expunged. Thus, aside from repleteness, univalence is not necessary until we get to anything that explicitly refers to the universe. That includes the proof referred to here that lex-reflective subcategories contain their own universes, as well as most stuff involving Type\sharp Type in the file Codiscrete.v and beyond. But for the basic theory of reflective subfibrations, stable factorization systems, and lex-reflective subcategories, univalence should not be necessary if we assume function extensionality and repleteness.

Thanks for giving me the impetus to figure that out; I’m happy to know that.

I would imagine that it is considerably easier to find models for intensional type theory without univalence but with a (non-trivial) interval.

Yes. Any well-behaved WFS in a LCCC gives you a model of DTT with identity types, and if the LCCC is additionally a model category, then a cylinder object of the terminal object gives you an interval type. (This is a special case of a forthcoming theorem of Peter Lumsdaine and myself about general HITs.)

Posted by: Mike Shulman on December 9, 2011 9:46 PM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

Thanks, Mike!

So but this means, if I understand you right, that even though you could remove use of univalence for a large bit of the internal theory of subcategories, it is still entirely crucial for cohesion. Right?

I was just getting worried today when I heard that apparently Voevodsky is on record as having said that he is beginning to think that Kan complexes is the only univalent model. (?!)

Posted by: Urs Schreiber on December 9, 2011 10:06 PM | Permalink | Reply to this

Re: Internalizing the External, or The Joys of Codiscreteness

I was just getting worried today when I heard that apparently Voevodsky is on record as having said that he is beginning to think that Kan complexes is the only univalent model.

Well, literally speaking, we do have models other than “the” model in Kan complexes. The groupoid model contains one univalent universe (the groupoid of sets). Any slice category of a univalent model is easily seen to be univalent. We can restrict the universe in Kan complexes in various ways, such as by considering only nn-types for some nn. And now we have one general way to make new models from old, although it doesn’t yet give us anything new from the models we already have.

Personally, I would go strong odds that Voevodsky is wrong, and that at least some other (,1)(\infty,1)-toposes model univalent type theory. There are other people working in HoTT who agree with me as well. Moreover, if it turns out that not all (,1)(\infty,1)-toposes model univalent type theory, I feel that this can only be because of coherence issues: the only thing that makes it hard is that substitution in type theory is too strict. And there do exist type theories that have less strict substitution, so it seems plausible to me that by weakening the type theory underlying HoTT we could obtain models in all (,1)(\infty,1)-toposes. Less strict type theories are more of a pain to work with, but that could be partly because no one has been strongly motivated to develop good tools for them yet. So I don’t think that we need to worry too much.

Posted by: Mike Shulman on December 9, 2011 10:20 PM | Permalink | Reply to this
Read the post Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
Weblog: The n-Category Café
Excerpt: A survey article on the formalization of aspects of quantum gauge field theory in the formal language of cohesive homotopy type theory.
Tracked: August 20, 2012 7:53 AM
Read the post Freedom From Logic
Weblog: The n-Category Café
Excerpt: Towards a way of doing homotopy type theory informally, and a new opinion regarding propositions as types.
Tracked: November 10, 2012 2:55 AM

Post a New Comment