A question about the computability of univalence

[Timothy Carstens]

In trying to understand the statement of the Univalence Axiom I started wondering about two sorts of issues. My guess is that these issues are ruled about by other things, and I was hoping someone could give me a hint as to whether or not that's true.

Let's say that A and B are equivalent types but that the equivalences carry tons of info. For instance, perhaps A(n,k) is the set of all traces up-to k execution steps of the 2-symbol n-state Turing machines (starting on the tape of 0's). Suppose B is similar, but has a factor yanked-out for the Busy Beavers.

Given a 2-symbol n-state TM, after k steps one of three things has happened:

1. The machine halted a few steps ago

2. The machine is halting now

3. The machine hasn't halted yet

So the question is, can I pair this trivial observation with Univalence to build a function which recognizes Busy Beavers? Computability theory says this should not be possible, but I lack the sophistication to recognize what in HoTT is preventing this. Is the impossibility simply that I could never describe the equivalence to Univalence, hence Univalence would never need to supply an identification?

A related line of questions comes up if I use A,B as alternate representations of 3-SAT problems, where A is something like Z/2Z[x_1,...] and B is a sum of 3-SAT solutions and non-satisfiable 3-SAT problems.

Can I view Univalence as a gadget which decides 3-SAT? Is its action on the higher homotopy groups just going to trace out the steps necessary to convert CNF to DNF? This doesn't sound impossible, but it would mean that the practicality of using Univalence may be wrapped-up in questions about the complexity hierarchy.

Forgive me if this is a silly line of questions; I'm really a computer scientist, but I spent enough time in Hatcher, Hartshorne, and Atiyah/MacDonald in grad school to get myself into trouble.

-t

[Jules Jacobs]

Univalence does not give you anything that you did not put in yourself. You put equivalences in, and you get equivalences out, but in the end the ones you get out are the same ones you put in (or compositions thereof).

[Timothy Carstens]

So if f is an equivalence, and I pass it through Univalence and look at the equivalence I get out, it will be f circ f circ ... circ f, m times, for some m? Has anyone written about the amount of work required to figure out such m?

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Timothy Carstens]

Sorry to double-post, but a more subtle interpretation of your response occurred to me. Should I instead be thinking of Univalence as a tool generating words in some presentation? Is my question about the "m" s better phrased as a question about a Dehn function?

[Michael Shulman]

If f is an equivalence, and you pass it through Univalence and look at
the equivalence you get out, it will be f again. I.e. m = 1.

[Timothy Carstens]

Should I walk away with either of these impressions?

1. Univalence is all about the absence of certain equivalences, rather than the ability to magically find a suitable identification.

2. If UA winds up being "computationally effective," and identifications and equivalences are the same thing, then when I execute a proof which uses UA via Curry-Howard, the call to the runtime's UA routine will run in constant-time and constant-memory, since it is indistinguishable from the identity function.

Thank you for your time; I'm sure these are painfully obvious questions, and I'll be sure to give the list a healthy break before returning with more.

-t

[Matt Oliveri]

On Sunday, August 2, 2015 at 6:11:09 PM UTC-4, Timothy Carstens wrote:

Should I walk away with either of these impressions?

1. Univalence is all about the absence of certain equivalences, rather than the ability to magically find a suitable identification.

2. If UA winds up being "computationally effective," and identifications and equivalences are the same thing, then when I execute a proof which uses UA via Curry-Howard, the call to the runtime's UA routine will run in constant-time and constant-memory, since it is indistinguishable from the identity function.

Well UA definitely isn't magic, but it really does "positively" provide identifications in constructive models.

It doesn't seem unreasonable that UA itself would be constant-time and constant-space, but that's an implementation issue. You could ask the authors of existing computational interpretations, like the cubical model(s) how their UA performs.

A good way to think of the UA is that it guarantees that equivalences and identifications between types are essentially the same. The UA provides some "glue code" to convert between them. Maybe identifications and equivalences can be exactly the same in some models. Ask the experts.

The utility of the UA is not so much running UA itself, but that it makes sure that equivalences are essentially as useful as identifications. The J rule, a.k.a. identity elimination, a.k.a. path induction, ensures that constructions respect identifications. Combined with UA, this means constructions respect type equivalences. So for example if you have an equivalence between A and B, then you get an equivalence between (ComplicatedFamily A) and (ComplicatedFamily B) for free, simply by rewriting (A = B) in (ComplicatedFamily _).

I think of the combination of UA and J as a clever sort of wrapper generator, except it works at runtime, which is kinda weird.

Thank you for your time; I'm sure these are painfully obvious questions, and I'll be sure to give the list a healthy break before returning with more.

Since these are beginner questions, it might be better to continue the questioning on the "HoTT Cafe" group.
https://groups.google.com/forum/#!forum/hott-cafe

[Andrej Bauer]

On Mon, Aug 3, 2015 at 12:11 AM, Timothy Carstens <intov...@gmail.com> wrote:
> If UA winds up being "computationally effective," and identifications and
> equivalences are the same thing

This is crucial: UA states that identifications and equivalences are EQUIVALENT.

It does NOT state that they are "the same thing". I think maybe that's
where confusion is arising.

With kind regards,

Andrej

[Michael Shulman]

On Mon, Aug 3, 2015 at 4:49 AM, Andrej Bauer <andrej...@andrej.com> wrote:
> This is crucial: UA states that identifications and equivalences are EQUIVALENT.
>
> It does NOT state that they are "the same thing". I think maybe that's
> where confusion is arising.

That's true for UA as originally stated, but cubical type theories are
trying to make identifications in the universe be equivalences *by
definition*. Right?

[Piyush P Kurur]

On Sun, Aug 02, 2015 at 07:32:54PM -0700, Matt Oliveri wrote:
> On Sunday, August 2, 2015 at 6:11:09 PM UTC-4, Timothy Carstens wrote:
> >
> > Should I walk away with either of these impressions?
> > 1. Univalence is all about the absence of certain equivalences, rather
> > than the ability to magically find a suitable identification.
> > 2. If UA winds up being "computationally effective," and identifications
> > and equivalences are the same thing, then when I execute a proof which uses
> > UA via Curry-Howard, the call to the runtime's UA routine will run in
> > constant-time and constant-memory, since it is indistinguishable from the
> > identity function.
> >
>
> Well UA definitely isn't magic, but it really does "positively" provide
> identifications in constructive models.
>
> It doesn't seem unreasonable that UA itself would be constant-time and
> constant-space, but that's an implementation issue. You could ask the
> authors of existing computational interpretations, like the cubical
> model(s) how their UA performs.

I thought that UA can potentially be computationally intractable
(although still computable). After all the UA says that there is an
equivalence between A and B being equivalent to A and B being equal
but nothing about how computational hard this mapping could be.

This is not precise but: If we take binary and unary nats since there
is an exponential blow up in the input sizes in both form, the proofs
that m + n == n + m when translated from binary to unary can take
exponential time as measured in the input size.

Regards,

ppk

[Timothy Carstens]

This is precisely the kind of thing I was trying to get at.

By analogy to the theory of automatic groups, if UA is going to be computable, then the amount of blow-up which can occur as we relate A to B must (I think?) grow at a computable rate.

With our computer-science hats on, we know that if we pick a problem class, we can relate the set of problem-statements and set of problem-solutions via algorithms. If we word the definitions of these sets correctly, they will be equivalent in some sense. If this sense is compatible with the notion of equivalence in HoTT, then I'd recon UA is at-least a universal Turing machine, since its ability to produce identifications sounds a lot like a machine which emits algorithms for finding solutions to problems.

So I wonder, is there something like an isoperimetric function describing the path spaces? If so, does the growth of these functions tell us anything about the computational power of UA?

I don't know if this is sound or useful reasoning; if it is, then what I'm asking, I suppose, is whether or not the nature of this TM has been studied from a computational perspective. It sounds like the cubical theories might provide a tool for this analysis, so I suppose that's where I should look next.

Thank you all for the discussion, it has given me much to think about.

-t

[Piyush P Kurur]

On Mon, Aug 03, 2015 at 09:07:15PM -0700, Timothy Carstens wrote:
> This is precisely the kind of thing I was trying to get at.
>
> By analogy to the theory of automatic groups, if UA is going to be
> computable, then the amount of blow-up which can occur as we relate A to B
> must (I think?) grow at a computable rate.

The example that I gave is un-interesting mathematically because of
the following.

The proof of 2^42 + 2^43 = 2^43 + 2^42 is the rather un-interestingly
refl. Sure agda takes a rather loooong time to arrive at the proof but
the stuff it prints out is the uninteresting refl. This is true for
any particular values of m and n.

The second point is that, often but not necessarily always, we are not
really interested in the actual proof calculated but in type checking
the program. So I guess the hardness of UA or for that matter the
functions that we write by induction for a lot of cases is
uninteresting.

Regards,

ppk

[Michael Shulman]

I think we're talking about different things. If "UA" means the
operation making an equivalence into an identification, then that can
certainly be constant-space. But *applying* that equivalence to an
*input*, or equivalently transporting across the resulting
identification, can be as slow as you like.

On Mon, Aug 3, 2015 at 8:55 PM, Piyush P Kurur <p...@cse.iitk.ac.in> wrote:

[Matt Oliveri]

On Tuesday, August 4, 2015 at 1:35:38 AM UTC-4, Michael Shulman wrote:

I think we're talking about different things.  If "UA" means the
operation making an equivalence into an identification, then that can
certainly be constant-space.  But *applying* that equivalence to an
*input*, or equivalently transporting across the resulting
identification, can be as slow as you like.

Exactly. I was saying UA itself should be fast. The equivalences it works with may or may not be fast.

If you start with a fast proof that (m + n = n + m) for binary nats, and convert it to a slow proof that (m' + n' = n' + m') for unary nats, this isn't UA's fault. It's because the equivalence between binary and unary nats already includes an exponential-time conversion in both directions. We can write arbitrarily slow programs using univalence, but that doesn't mean univalence is intractable. Similarly, we don't consider for loops intractable just because you can write very slow programs using for loops. The possibility of intractable equivalences does not necessarily mean UA is impractical for programs that you really run. It just means real programs should not feed UA with intractable equivalences.

[Martin Berger]

On 5 August 2015 at 00:28, Matt Oliveri <atm...@gmail.com> wrote:
> I was saying UA itself should be fast

The univalence axiom contains an existential quantifier

For types A, B : U, there is a certain function, idtoeqv : .....

(Lemma 2.10.1 in the HoTT book). In a Curry-Howard interpretation of
the UA axiom, there needs to be a computational mechanism giving
computational content to this existential quantifier. Maybe one could
say that Timothy Carstens's question is about the reasons why this
computational mechanism should be fast?

Martin

[Steve Awodey]

the particular function IdToEquiv is given by an Id-elim.
the only existential quantifier involved is in the definition of IsEquiv(IdToEquiv), but that type is a proposition and so has no computational content.

[Martin Escardo]

On 05/08/15 13:04, Steve Awodey wrote:
> the particular function IdToEquiv is given by an Id-elim.
> the only existential quantifier involved is in the definition of IsEquiv(IdToEquiv), but that type is a proposition and so has no computational content.

I don't think it is entirely accurate to say that if a type is a
proposition then it doesn't have computational content.

For example, UA itself is a proposition, and it does have computational
content in cubicaltt.

But one can give more mundane examples. For example, the following type
is inhabited and is a proposition:

isContr(Sigma(n:N).n is prime
& n is the difference of two squares of primes).

Applying the first projection twice to a term defining an inhabitant of
this type, one computes the number 5.

Martin

[Steve Awodey]

nice example.
S

[Martin Escardo]

I'd like to take the opportunity to emphasize that propositional
truncation ||-|| doesn't erase computational information either.

This time consider the type

||Sigma(n:N).n is prime
& n is the difference of two squares of primes||.

This type is inhabited, and from any term defining an inhabitant, you
again compute the number 5, by first applying ||-||-recursion using the
fact that the untruncated type

Sigma(n:N).n is prime
& n is the difference of two squares of primes

is a proposition, and then applying the first projection.

Of course, you need a type theory in which ||-|| computes, such as
cubicaltt.

Martin

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Jon Sterling]

Martin—Thank you for reiterating this crucial distinction. Nuprl has
long had multiple versions of truncation/squashing which each have a
different effect on the kinds of observations that are possible.

Essentially, we can consider two different kinds of truncation: those
which rule out extensional observations of computational content, and
those which rule out even intensional observations. HoTT's truncation is
the former.

In computational type theory, HoTT-style -1-truncation is implemented
using a quotient, so ||P|| =def= x,y:P // Unit. Inhabitants of this type
are the inhabitants of P, but identified with the trivial relation; so
it is possible to observe which p:P you have, but only inasmuch as your
observation is functional (i.e. it doesn't reveal the value to anyone
who isn't allowed to know it). On the other hand, the kind of squashing
which is most frequently used in Nuprl does actually erase computational
content, thereby ruling out even intensional observations.

This one is defined using the "subset" type: squash(P) =def= {Unit | P}.
It can also be defined using the Image type
(http://wollic.org/wollic2006/nogin-kopylov-slides.pdf), squash(P) =def=
Image(P; λx. <>).

I used to think the various examples of tricky observations of truncated
values were very mysterious, but when you take into account that the
values must "still" be there in any acceptable computational semantics
(whatever that turns out to be), it is perhaps less surprising. The
quotient-style squashing is done by coarsening a type's equivalence
relation, and the subset-style squashing is done by adding a side
condition to the PER of the Unit type.

Does anyone know if any of the HoTT models would admit a squash type
that actually erases computational content?

Best,
Jon

[Andrej Bauer]

There is one further, essential difference between propositional
truncation in HoTT/UF and various forms of "brackets" in type theory
-- but this one is in a different direction.

In HoTT/UF concepts are generally defined in terms of mathematical
content. One may *discover* that a type is contractible, or a
proposition, or a set, and this discovery can be a non-trivial piece
of mathematics. I would call this the "mathematical tradition".

In traditional type theories concepts are generally defined in terms
of structure or form. One does not have to "discover" that something
is the unit type, a bracket type, a squash type, or a Coq-style Prop
-- at worst it is a matter of normalization. I would call this the
"logical tradition" or maybe even the "formalist tradition".

The formalist tradition is very strong in the type-theoretic
community, which of course is not a surprise. I have privately
hypothesized before that if a graduate student presented the
univalence axiom and some of its significant consequences at a
workshop, people would just remember it as an interesting but
non-workable idea which broke normalization and generally did things
"the wrong way". I remember the opposition Steve and I met when we
formulated the bracket types; the first thing almost every type
theorist said was "but you have a judgmental equality as a premise in
one of your elimination rules" I never really found out why that was a
faux pas.

One reason for HoTT/UF having created such excitement in the
type-theoretic community is that it brought in some good old
mathematics.

With kind regards,

Andrej

[Matt Oliveri]

On Wednesday, August 5, 2015 at 11:03:16 AM UTC-4, Jonathan Sterling wrote:

Does anyone know if any of the HoTT models would admit a squash type
that actually erases computational content?

Seems like they would, doesn't it? Using subobjects to do subset-squash? But I don't know.

It seems like axiomatizing types like Nuprl's subset would require breaking from the mold of intensional type theory. In ITT, the same terms are used both as proof terms and computational content. But generally, proof terms need extra stuff that should not be part of the computational content. Like with Nuprl-style subset. The evidence that an element belongs to a subset is not part of the computational content. (So Nuprl-style subset is different from Sigma with an h-proposition.)

[Martin Escardo]

I agree with Andrej, but I think he is being too harsh with logicians:
after all, they came up with all sort of interesting and useful things,
which we are happily using here, including MLTT.

And perhaps all of us here are

x * mathematician + y * logician + z * computer scientist

with x + y + z = 1 (or maybe <=1) and x,y,z>0, with varying weights x,y,z.

And this is what makes things work. None of the three alone suffices to
get things working. The IAS and IHP events, and this list, and all
outcomes from that, are a factual proof.

But the issue of bracket types of all sorts comes up again and again,
and I would like reach clarification of this (I was going to say "once
and for all", but this is too ambitious).

I have a problem, of the sort Andrej alludes to, with erasure of
computational information. NuPrl has its ways, as discussed by Jon, and
so has Agda, and there has been some research on that (which I confess I
am not entirely familiar with).

Let's use the notation "erase X" for such an erasure of the
computational information in X (whatever this may mean).

In all approaches I have seen, it seems to me that erase X and not(not
X) are "observationally" indistinguishable, but not provably equal.

More importantly (mathematically or logically speaking now), what is the
defining property of erase X, before we know how to implement it, for
any reasonable notion of computational erasure?

For comparison, the map X->||X|| is the universal solution to the
problem of turning X into a proposition (a type such that any two of its
elements are Id-equal). Here, before we know how to implement it (e.g.
in cubicaltt), we know what it is supposed to be.

What is the logical/mathematical status of any notion of computational
erasure? What is the specification of erase X before we know how we are
going to implement it?

My guess (prove me wrong!) is that no such specification can distinguish
erase X from not(not X).

In any case, the point is that it is alright to try to erase
computational information, for whatever purpose, but one also has to ask
what its logical or mathematical content is.

Best,
Martin

[Thomas Streicher]

> My guess (prove me wrong!) is that no such specification can distinguish
> erase X from not(not X).

Well, in Set ||X|| is isomorphic to (X->0)->0 but in the effective
topos it is not. Squashing coincides with booleanisation iff the monos
give rise to boolean logic.
So typically, i.e. in non-boolean toposes, squashing is different from
booleanization.

Thomas

[Andrea Vezzosi]

In agda we have (A -> erase B) -> erase (A -> B) but we don't have the
double negation shift.

There is indeed a lack of a specification for erase, it seems we
immediately start talking about judgemental equalities or even actual
erasure to other models of computation.

Best,
Andrea

[Martin Escardo]

What you are saying is that if excluded middle holds, then ||X||=¬¬X.

This can actually be proved in HoTT (and is an exercise of the book).

But the question here is a different one.

Jon asked whether there is a notion of "computatational erasure"
compatible with HoTT (without assuming excluded middle, I presume).

I (perhaps subtly) returned the question to him by asking for a
specification of such a notion, before we can (perhaps) define it.

Martin

[Martin Escardo]

You also have erase X -> ¬¬X in Agda.

But, as far as I can see, you don't have the converse.

However, as far as I can see, there is nothing you can prove about erase
X that you can't prove about ¬¬X, and vice versa.

They seem to be indistinguishable in practice (or observationally
indistinguishable), in the same way that equivalent types, in
intensional MLTT, are observationally indistinguishable before you
postulate univalence. In fact, the consistency of univalence gives the
observational indistinguishability of equivalent types in intensional MLTT.

But here the situation is a bit different, because there is no logical
or mathematical specification of the type erase X (in Agda, or any type
system studied in the literature, as far as I know). I think it is
consistent that erase X is Id-equal to ¬¬X in Agda.

Martin

[Martin Escardo]

Question (not only for you, the author of the above paragraph). Let
"erase" be some form of computational erasure (whose logical or
mathematical status I still don't undertand).

In what you say above, you express the belief that

(i) Sigma(x:X).||A x|| (in HoTT)

is not the same as

(ii) Sigma(x:X).erase(A x) (in NuPrl).

I agree.

There is also

(iii) Sigma(x:X).¬¬(A x) (in both).

What I can't see is the difference between (ii) and (iii). The
difference between (i) and (iii) is clear (unless excluded middle
holds). In particular, as discussed earlier, from the proposition ||A
x|| we may be able to get computational information, as illustrated
earlier, whereas from ¬¬(A x) we can almost never get any computational
information. An exception is when A x is decidable, where we get ¬¬(A
x)->A x. But in this case too, in Agda, we get erase(A x)->A x. What
about NuPrl?

The question, to be repetitive, is what is the difference between (ii)
and (iii) in the absence of excluded middle?

What is the logical/mathematical meaning of the operation "erase"?

That of ¬¬X is clear (namely (X->0)->0), and so is that of ||X||
(essentially forall P. isProp P -> (X->P)->P)). The operation "erase" is
between these two, but it doesn't really have a definition (just an
implementation).

Martin

[Matt Oliveri]

So I guess for Nuprl, erase(X) refers to the subset-squash of X. Then yeah. In particular, erase(A x)->¬¬(A x).

The question, to be repetitive, is what is the difference between (ii)
and (iii) in the absence of excluded middle?

What is the logical/mathematical meaning of the operation "erase"?

That of ¬¬X is clear (namely (X->0)->0), and so is that of ||X||
(essentially forall P. isProp P -> (X->P)->P)). The operation "erase" is
between these two, but it doesn't really have a definition (just an
implementation).

I don't know anything about Agda's erase. As for subset in Nuprl, would it be cheating to refer you to the PER semantics? That is something different from Nuprl's implementation.

Informally, imagine you have a computer program. You can reason about it. But none of that reasoning affects the program. It's already compiled and released, say, but we still have the source code, to figure out how bad we screwed up. Well, do you use intuitionistic logic to reason about it, or classical logic? There's some difference, but in neither case is this going to have any effect at all on the program. That's the difference between erase and ¬¬, sort of. Neither of them have nontrivial computational content, but erase is still intuitionistic.

But Nuprl is not anti-classical, so the real story is more abstract than the computational interpretation. You have some universe of objects that the PERs are relations on. For Nuprl's computational interpretation, this universe is the type of programs in an untyped lambda calculus, up to observational equivalence. In any case, there is some notion of equality for universe elements which is not particular to any given PER. Then each PER picks out some of the universe elements to relate in some way. Call some PER an "observational proposition" (ObsProp) if there's at most one universe element related by that PER. I believe (not sure) that erase(X), the subset-squash of X, is initial among all ObsProps with a map from X. The reason why this should intuitively be something different from (-1)-truncation is that ||X||, considered as something PER-like, may not be an ObsProp. It can relate multiple universe elements, as long as each such element is related to every other. An ObsProp is always an h-prop, but not the other way around. So at the end of the day, subset-squash is about some "more primitive" notion of equality not expressible in intensional type theory. (Assuming the identity type reflects the PER, rather than the raw equality of universe elements.)

[Matt Oliveri]

So if Agda has an erase constructor, and it's considered to preserve strict positivity for inductive definitions, maybe a good "direct" definition of dependent type theory would be as inductive-inductive types, where derivations of judgmental equality are erased when they are used in type and term derivations.

Does that sound any good?

[Thomas Streicher]

> Jon asked whether there is a notion of "computatational erasure"
> compatible with HoTT (without assuming excluded middle, I presume).

well, taking \neg\neg-sheaves would be computational erasure

it may coincide with squashing but only if we are already boolean

Thomas

[Andrej Bauer]

Perhaps Bob Harper can chime in, but I would guess (based on my
ignorance of NuPrl) that you won't get away with PERs. Doesn't NuPrl
have a type of propositions of some sort? How would that be
represented as a PER? An assembly sounds more likely to me.

The difference between a PER and an assembly is that an assembly is
like a per in which a realizer may realize many elements. Thus, for
instance, one can have the assembly of all PERs, or "nabla 2" which is
the assembly of classical truth values. It is the set {0,1} where both
elements are realized by the unit ().

Also, let me point out that the is *no* type theory, however
intensional, in which the terms contain the *entire* derivation. At
the very least judgmenal equalities are not recorded (but see Herman
Guever's work), which is consistent with the philosophy of type
theory: a judgmental equality is supposed to be analytic, or
"self-establishing" (a computer scientist would say "decidable" and
"proof irrelevant", or just "bool").

With kind regards,

Andrej

[Thomas Streicher]

Nuprl is essentially based on Realizability and as I pointed out in
realizability models the difference is between epi/mono factorizations
and \neg\neg-epi/\neg\neg-mono factorizations. These notions make sense
in general models and not only in realizability models.

Of course, these two things can coincide if the category is already boolean.

BTW there arises a question about "squashing" or "propositional reflection".
Typically, it is intended as reflection to subterminals. But maybe that's
not what squashing is in HoTT because there it is reflection to types
"containing at most one element". But that need not mean subterminal it
just means "at most one connected component". If A is a nontrivial group
it validates (Pi x,y:A) Id_A(x,y) but A is certainly not subterminal.
All the discussions about constancy arise from this problem, namely that
being subterminal, i.e. a proposition, cannot be expressed in the language
of type theory.
In the groupoid model "propositional reflection" fails because groups
together with the empty groupoid do NOT form a (full) reflective subcategory
of all groupoids. I doubt this can be overcome by moving to weak higher
dimensional groupoids.

I don't deny the relevance of proposition as a semantical notion but
I think it cannot be expressed in the internal language unless all types
are sets externally.

Thomas

[Matt Oliveri]

On Thursday, August 6, 2015 at 5:13:20 AM UTC-4, Andrej Bauer wrote:

Perhaps Bob Harper can chime in, but I would guess (based on my
ignorance of NuPrl) that you won't get away with PERs. Doesn't NuPrl
have a type of propositions of some sort? How would that be
represented as a PER? An assembly sounds more likely to me.

Hmm. It seems pretty standard to interpret Nuprl's type system using PERs.
http://www.nuprl.org/KB/show.php?ID=726

I don't think there's a primitive type of propositions. You might be able to define one, but I don't know what you have in mind, or the problem you're anticipating.

The difference between a PER and an assembly is that an assembly is
like a per in which a realizer may realize many elements. Thus, for
instance, one can have the assembly of all PERs, or "nabla 2" which is
the assembly of classical truth values. It is the set {0,1} where both
elements are realized by the unit ().

Well alright. But I still can't figure out why an interpretation of Nuprl would use assemblies then. It seems like a feature, not a bug, that a given realizer has at most one mathematical meaning.
 

Also, let me point out that the is *no* type theory, however
intensional, in which the terms contain the *entire* derivation. At

the very least judgmenal equalities are not recorded,

I agree. The distinction between proof term and computational content that I was making was not meant to imply that proof terms are entire derivations. Proof terms, I figure, should have enough information to reconstruct some derivation. But terms in extensional type theory, including Nuprl, do not generally have enough information to reconstruct any derivation. In these systems, the terms can still be faithful representatives of the computational content of a proof though.

What seems to happen in implementations of extensional type theory, is that proof terms end up getting reintroduced some way or another, even though they no longer coincide with the terms that judgmental equality and types depend on. In Nuprl, these were called proof trees. Dan Grayson tried to use LF to encode the proof terms. Your Andromeda seems to have proof terms too, since the annotations that add hints are not part of the mathematical meaning of terms. It's a remarkable property of intensional type theory that the proof terms and "meaning terms" coincide. But it doesn't seem like a terribly useful property, and it's an uncomfortable restriction.

which is consistent with the philosophy of type
theory: a judgmental equality is supposed to be analytic, or
"self-establishing" (a computer scientist would say "decidable" and
"proof irrelevant", or just "bool").

Well I personally don't see why judgmental equality should have to be decidable. And I wouldn't have thought you'd think it should either, since Andromeda is implementing extensional type theory, where judgmental equality is undecidable.

Of course this means proof terms now generally do need evidence for judgmental equality. (This does not affect the original "meaning term".) And that's fine. If we're lucky, the cases that didn't need evidence in intensional type theory still won't need evidence. Equality reflection gives us richer judgmental equality so that we don't need to pollute meaning terms with casts unless they're computationally/mathematically relevant. Only the proof terms get polluted, by instances of the reflection rule. (Or hints, or whatever.)

[Andrej Bauer]

On Thu, Aug 6, 2015 at 12:36 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> However, as far as I can see, there is nothing you can prove about erase
> X that you can't prove about ¬¬X, and vice versa.

It seems like a lot of intuitions about erasure are based on "erasing
programs", so let me just quickly remind everyone how this works in
realizability. Consider a "subset" type

{ x : A | P x }

and let us see what it is in realizability under various
interpretations of erasure of P x. To make the discussion closer to
HoTT-style of thinking, let me factor the type as a dependent type and
propositional truncation:

Σ (x : A) ||P x||_Prp.

Here Prp is some notion of propostion, and || – ||_Prp is reflection
into propositions. Here are three possibilities for Prp, each of which
corresponding to one notion of NuPrl subsets (but I do not know the
terminology well enough to match them):

(a) If all types are propositions, let me write Prp = Type, then ||P
x|| = P x and we are just doing dependent sums, so {x : A | P x} is
the object whose elements are pairs (x,y) with x : A and y : P x. Such
a pair is realized by a pair of realizers (u,v) such that u realizes x
and v realizes y. Equality on the type is equality of pairs.

(b) If we take the HoTT notion of propositions then propositions
correspond to subobjects. This is so because realiability models have
extensional equality. If we are in a topos then we can write Prp = Ω,
i.e., there is a type of propositions (but this type does *not* exist
in PER models). {x : A | P x} is interpreted as the image of the
display map P → A. Concretely, an element of {x : A | P x} is an
element x : A for which there exists a y : P x. Such an x is realized
by a pair (u, v) such that u realizes x and v realizes some y : P x.
Importantly, equality is the equality on A, i.e., we ignore v when
comparing elements.

(c) We could take the ¬¬-stable propositions. In assemblies (but not
in a PER model) these are classified by the object ∇2. It is the set
{0,1} in which both 0 and 1 are realized by the unit (). It is
instructive to think about what are the realized maps A → ∇2. In this
case {x : A | P x} is interpreted as the regular image of the display
map P → A. Concretely, an element of {x : A | P x} is an element x : A
for which there exists y : P x. Such an x is realied by a realizer u,
as in A. Equality is inherited from A.

The Church encoding of propositional truncation

||P x|| := ∏ (q : Prp), (P x → q) → q

coincides with (b) above when we take Prp = Ω and with (c) when we
take Prp = ∇2. We cannot really get (a) this way because of size
issues. Presumably, if we take Prp = U where U is an impredicative
universe, we will get (a), but with reflection into U.

The moral of the story is that in realizability models there are two
non-trivial notions of erasure, (b) and (c) above. When type theorists
think of "dropping proof terms" they speak of (c).

Are there other notions of propositional truncation? Of course, you
could take an Lavwere-Tierney operator j : Ω → Ω and define
j-propositional truncation using the j-stable truth values. But what
would be some interesting examples of a j-operator? Is Jaap van Oosten
listening?

Andrej

[Bas Spitters]

This paper by Peter Aczel contains some variations along these lines:
http://www.cs.man.ac.uk/~petera/russ-praw.ps.gz

[Zhen Lin]

On Thu, 6 Aug 2015 at 18:03 Thomas Streicher <stre...@mathematik.tu-darmstadt.de> wrote:
>
>  
>  Typically, it is intended as reflection to subterminals. But maybe that's
>  not what squashing is in HoTT because there it is reflection to types
>  "containing at most one element". But that need not mean subterminal it
>  just means "at most one connected component". If A is a nontrivial group
>  it validates (Pi x,y:A) Id_A(x,y) but A is certainly not subterminal.

Actually, it does not. A group validates that formula if and only if it is trivial: indeed, an element of that type is a group element g such that, for all pairs (h, k) of group elements, g h = k g; in particular, we may take h = id and k = g^{-1} to get g = id, and then it follows that h = k for all (h, k).

To put it in more groupoid-theoretic terms, an element of that type is a natural isomorphism from the first projection A × A → A to the second projection. As such, a groupoid validates that formula if and only if it is empty or contractible.

[Andrej Bauer]

On Thu, Aug 6, 2015 at 12:20 PM, Matt Oliveri <atm...@gmail.com> wrote:
>> which is consistent with the philosophy of type
>> theory: a judgmental equality is supposed to be analytic, or
>> "self-establishing" (a computer scientist would say "decidable" and
>> "proof irrelevant", or just "bool").
>
>
> Well I personally don't see why judgmental equality should have to be
> decidable. And I wouldn't have thought you'd think it should either, since
> Andromeda is implementing extensional type theory, where judgmental equality
> is undecidable.

I learned this from Bob Harper so perhaps he would be a better person
to explain. But I explain this to myself as follows: in a formalism
there will be *some* notion of self-evident equality (I am skipping
over the somewhat subtle difference between "self-evident" and
"analytic" – I shall use "self-evident" because it is less scary).
Now let judgmental equality be whatever notion of equality is deemed
self-evident. We may then incorporate this notion into type theory by
postulating that we may replace a thing with one that is
self-evidently equal to it. We will be tempted to push the limits of
"self-evident" to obtain a richer system (and to appear to be
smarter), but probably not beyond "decidable".

Since you asked about Andromeda. Type theory with equality reflection
is fun to explore and is mathematically significant, and therefore
worthy of study. But it is also important to understand the
motivations and philosophy behind Martin-Löf type theory, for then one
can respect the "design limitations" imposed on it. Type theory with
equality reflection is not in my mind type theory a la Martin-Löf. It
is not married to computation and constructivism (as a philosophy). It
is more like abstract algebra.

With kind regards,

Andrej

[Matt Oliveri]

I really like how you (Andrej) started, with the different notions of proposition, and their corresponding squash and subset. But I could be confused, because none of your notions of proposition seem like the one behind Nuprl's subset. (c) seems the closest, because the realizers for a subset are just realizers for the original type. But I didn't think Nuprl's subset-squashed propositions are necessarily ¬¬-stable. That would mean ¬¬erase(X)->erase(X)? Also, what's the difference between an element and a realizer? I guess I should've asked that before, when you said what assemblies are. But in Nuprl, the elements of a type simply are realizers.

[Thomas Streicher]

Thanks for pointing that out, I should have known it!

But still I don't see why validity of isProp(A) entails that A is
subterminal. But it says A is equivalent to a subterminal.

Thomas

> > Typically, it is intended as reflection to subterminals. But maybe that's
> > not what squashing is in HoTT because there it is reflection to types
> > "containing at most one element". But that need not mean subterminal it
> > just means "at most one connected component". If A is a nontrivial group
> > it validates (Pi x,y:A) Id_A(x,y) but A is certainly not subterminal.
>
> Actually, it does not. A group validates that formula if and only if it is
> trivial: indeed, an element of that type is a group element g such that,
> for all pairs (h, k) of group elements, g h = k g; in particular, we may
> take h = id and k = g^{-1} to get g = id, and then it follows that h = k
> for all (h, k).
>
> To put it in more groupoid-theoretic terms, an element of that type is a

> natural isomorphism from the first projection A в A ??? A to the second

[Matt Oliveri]

On Thursday, August 6, 2015 at 6:51:43 AM UTC-4, Andrej Bauer wrote:

On Thu, Aug 6, 2015 at 12:20 PM, Matt Oliveri <atm...@gmail.com> wrote:
>> which is consistent with the philosophy of type
>> theory: a judgmental equality is supposed to be analytic, or
>> "self-establishing" (a computer scientist would say "decidable" and
>> "proof irrelevant", or just "bool").
>
> Well I personally don't see why judgmental equality should have to be
> decidable. And I wouldn't have thought you'd think it should either, since
> Andromeda is implementing extensional type theory, where judgmental equality
> is undecidable.

I learned this from Bob Harper so perhaps he would be a better person
to explain. But I explain this to myself as follows: in a formalism
there will be *some* notion of self-evident equality (I am skipping
over the somewhat subtle difference between "self-evident" and
"analytic" – I shall use "self-evident" because it is less scary).
Now let judgmental equality be whatever notion of equality is deemed
self-evident. We may then incorporate this notion into type theory by
postulating that we may replace a thing with one that is
self-evidently equal to it. We will be tempted to push the limits of
"self-evident" to obtain a richer system (and to appear to be
smarter), but probably not beyond "decidable".

I see. That makes sense. I think we are just using "judgmental equality" differently. I just meant the equality specified as a judgement form. Admittedly, that's not a very useful distinction if you have the equality reflection rule.

But it is also important to understand the
motivations and philosophy behind Martin-Löf type theory, for then one
can respect the "design limitations" imposed on it.

That sounds great! Is it easy to do? Is there a "here's why intensional type theory rules" paper?

Type theory with
equality reflection is not in my mind type theory a la Martin-Löf. It
is not married to computation and constructivism (as a philosophy). It
is more like abstract algebra.

That strikes me as a very funny thing to say, since the semantics of Nuprl has been very intuitive to my programmer brain. Perhaps you haven't seen it in the right light, or I haven't seen it in the wrong light. :) Intensional type theory seems like the abstract algebra to me, since it has restrictions which do not seem necessary simply for terms to be correct programs.

[Peter LeFanu Lumsdaine]

On Thu, Aug 6, 2015 at 1:27 PM, Thomas Streicher <stre...@mathematik.tu-darmstadt.de> wrote:

Thanks for pointing that out, I should have known it!

But still I don't see why validity of isProp(A) entails that A is
subterminal. But it says A is equivalent to a subterminal.

It doesn’t imply that A is subterminal (or even in general equivalent to a subterminal) in the external 1-categorical sense, since that would require uniqueness up to *judgemental* equality, which the propositional equality can’t enforce.

But in the set, groupoid, and simplicial set models, it will correspond to “being equivalent to a subterminal” as you say, because one can use the epi-mono factorisation to get a “definitional squashing”, and this preserves fibrations in those models.  And I’d expect that in general, viewing models of TT as quasi-categories (as constructed by Chris Kapulkin), inhabitedness of “isProp(A)” should correspond precisely to being subterminal in the ∞-categorical sense.  This would I guess be rather non-trivial, and quite interesting, to prove!

–p.

[Thomas Streicher]

> But in the set, groupoid, and simplicial set models, it will correspond to

> ???being equivalent to a subterminal??? as you say, because one can use the
> epi-mono factorisation to get a ???definitional squashing???, and this
> preserves fibrations in those models. And I???d expect that in general,

> viewing models of TT as quasi-categories (as constructed by Chris

> Kapulkin), inhabitedness of ???isProp(A)??? should correspond precisely to
> being subterminal in the ???-categorical sense. This would I guess be rather

> non-trivial, and quite interesting, to prove!

Does one really know how to interpret type theory in \infty-cats.
Where has Kris written up this?

But otherwise I fully agree with you. I rather know how to interpret
type theory in model cats (after splitting). Then isProp(A) holds iff A
is equivalent to a subobject of 1 where "equivalent" refers to weak
equivalence in the sense of the model structure.

Now moving from a model cat to the associated \infty-cat (not at all
trivial BTW) means replacing equality by weak equivalence.
Accordingly, I think one cannot interpret judgemental equality in
\infty-cats! Isn't that a problem?

But there are ways of restoring it since one can find a "representing"
model cat for sufficiently many \infty-cats (see Szumilo's Thesis for
the most developed account in this vein). But there are various
representing model cats.

I tend to think that one can't interpret type theory in \infty-cats
due to this absence of judgemental equality. It is true that one can
trade judgemental and propositional equalities to some extent. But
that's not much investigated since the more judgemental equalities you
have the more convenient it is to use the ensuing type theory.

Thomas

[Jon Sterling]

Andrej,

I hope I am not repeating something which someone else has already
clarified, but Nuprl does not have any distinction between propositions
and types. There is a notation "prop", but this is simply a shorthand
for "univ".

Best,
Jon

[Peter LeFanu Lumsdaine]

On Thu, Aug 6, 2015 at 3:13 PM, Thomas Streicher <stre...@mathematik.tu-darmstadt.de> wrote:
>
> > But in the set, groupoid, and simplicial set models, it will correspond to “being equivalent to a subterminal” as you say, because one can use the epi-mono factorisation to get a “definitional squashing”, and this preserves fibrations in those models.  And I’d expect that in general, viewing models of TT as quasi-categories (as constructed by Chris Kapulkin), inhabitedness of “isProp(A)” should correspond precisely to being subterminal in the ∞-categorical sense.  This would I guess be rather non-trivial, and quite interesting, to prove!

>
> Does one really know how to interpret type theory in \infty-cats.

> Where has Kris written up this?

A lot is certainly still to be worked out, but Chris’s results have made significant progress, enough for a statement like mine above to be completely precise.

The main writeup is “Locally Cartesian Closed Quasicategories from Type Theory”, http://arxiv.org/abs/1507.02648.  Its main results are: let C be a CwA (or contextual category) with the structure to model Σ-types, Id-types, and Π types with the eta rule and functional extensionality.  Then:

(a) there is a quasi-category N_f(C), constructed from C in a fairly concrete way (in particular, allowing objects and maps of C to be viewed as objects and arrows of N_f(C), well-defined up to equivalence) (and moreover N_f(C) is a model for the homotopy coherent nerve of (C, viewed as a category with weak equivalences));

(b) N_f(C) is locally cartesian closed, in the ∞-categorical sense.

He also posted recently on the n-category café about what’s known about the idea that TT should be an internal language for higher categories, and what sorts of things one might hope for: https://golem.ph.utexas.edu/category/2015/07/internal_languages_of_higher_c.html

> Now moving from a model cat to the associated \infty-cat (not at all
> trivial BTW) means replacing equality by weak equivalence.
> Accordingly, I think one cannot interpret judgemental equality in
> \infty-cats! Isn't that a problem?
>

> But there are ways of restoring it since one can find a "representing"
> model cat for sufficiently many \infty-cats (see Szumilo's Thesis for
> the most developed account in this vein). But there are various
> representing model cats.
>
> I tend to think that one can't interpret type theory in \infty-cats
> due to this absence of judgemental equality.

Quite agreed, it’s a highly non-trivial problem!  But I don’t think it’s a non-starter by any means.  The sort of things one could reasonably hope for might be e.g.:

(a) given any lcc quasicategory X, there’s an associated CwA C(X), with Π, Σ, Id-structure as above (maybe constructed via model-categorical presentations of X);

(b) there’s a map ε_X : N_f(C(X)) -> X (a putative co-unit);

(c) maybe ε_X is even an equivalence of quasicategories, or something.

(a) and (b) would I think be enough to justify the statement “type theory [with Σ, Π, Id] can be interpreted in lcc ∞-categories”: it would give a function from (at least) the pure syntax of TT into the objects and arrows of any lccc qcat.  Some form of (c) could moreover justify saying that TT can be used to reason about arbitrary objects, arrows etc. in an lcc ∞-cat.  And obviously one would want to flesh out that picture in lots more ways: do different representing model cats for an lcc qcat give equivalent models of TT, in some sense?  Does the whole thing fit together in an infinity-adjunction?

But in any case, I just want to make the point that the absence (or ill-behavedness) of judgemental equality in quasi-cats isn’t an insurmountable obstacle to interpreting TT in them.  Just like the fact that pullback in LCCC’s isn’t strictly functorial, it’s a technical difficulty that needs to be overcome somehow, but it’s not (hopefully) a deal-breaker.  It tells us that the construction of C(X) from X can’t be as straightforward as the construction of, say, the ETT CwA associated to an LCCC; but that’s ok, and not really awfully surprising.

–p.

[Jon Sterling]

Hi all,

I had mentioned the following off-list, and Martin thought it might be
of interest to the list, so I'm reproducing it here.

With regard to double negation, Bob Constable has been mulling over an
idea of "virtual evidence" for a while now, where he adds a new rule to
computational type theory such that not(not(A)) ==> {x:1 | A}.
http://arxiv.org/abs/1409.0266. Bob spoke a bit about this at OPLSS this
year as well.

Best,
Jon

[Thomas Streicher]

Thanks for the pointers! I find the harder problem to find a
representing model stucture for an \infty topos. Szumilos way of doing
it is quite some progress. But what I don't see is how good the chosen
judgemental equality is. (It is better if more equalities are
judgemental!)

There is one drawback anyway: an "object classifier: is turned into a
weak universe `a la Tarski. That's cumbersome but certainly better
than what one might expect a priori!
And in particular important cases one even gets strong universes.

My impression is that many people neglect judgemental equality which
is understandable because it is just a tool. I mean when you use a system
it always works in the background and you don't really see it. (But you
would feel it very painfully if it were absent!) But computational
meaning is essentially given by judgemental equality or rather by the
intersection of all judgemental equalities induced by all models which
admit one.

Thomas

[Martin Escardo]

On 06/08/15 16:08, Jon Sterling wrote:
> I had mentioned the following off-list, and Martin thought it might be
> of interest to the list, so I'm reproducing it here.

Thanks.

> With regard to double negation, Bob Constable has been mulling over an
> idea of "virtual evidence" for a while now, where he adds a new rule to
> computational type theory such that not(not(A)) ==> {x:1 | A}.
> http://arxiv.org/abs/1409.0266. Bob spoke a bit about this at OPLSS this
> year as well.

Good. This paper says that it is consistent that erase X is ¬¬X,
in the *absence* of excluded middle, which was my intuition.

We do have erase X -> ¬¬X always.

But Constable postulates ¬¬X -> erase X (where erase X is written
{Unit|X} and called a refinement type) in that paper (and I emphasize
that excluded middle doesn't follow from that).

What is erase X in the absence of Constable's postulate?

A realizability semantics of erase was discussed in this list (and it is
mentioned in Constable's paper).

But what can we say *internally* in type theory about erase X?

In MLTT, ||X|| (if it exists) is the propositional reflection of X,
where a proposition is a type in which any two elements are Id-equal.

We can write the following specification of ||X||, where I use R for
||X|| in MLTT.

isPropReflection R X = isProp R * (X->R)
* Pi(P:U). isProp P -> (X->P) -> (R->P)

The propositional reflection R of X need not exist in MLTT. But we can
say what it is, up to pointwise isomorphism (which is just
bi-implication in the case of propositions).

MLTT may not in general have propositional reflections for all types.
But it does for some types. For example, if there is a function f:X->X
such that fx=fy for all x:X, then X has a propositional reflection,
namely the type Sigma(x:X).fx=x of fixed points of f. This is the case
if X is empty or if X has a given point. Then non-trivial examples
exist: for example, for any f:N->N, the type Sigma(n:N).fn=0 has a
propositional reflection in MLTT, before we know whether it is empty of
inhabited.

Moreover, we have ||X||->¬¬X. However, if we postulate the converse, we
get excluded middle. This is another way of seeing that ||X|| is very
different from erase X.

Is it possible to complete the following internal definition of
computational erasure, before we know whether it exists?

isErasure E X = ?

Moreover, once we have completed it, can we give examples, as above for
propositional reflection, where an erasure of X exists without having to
extend the type theory with an erasure construction? Well, we should
have the following trivial examples at least: An erasure of the empty
type if the empty type. An erasure of any type that has an element is
the unit type.

Best,
Martin

[Jon Sterling]

With regard to defining "isErasure" internally, I do not know if this
can be done in ETT or MLTT, but it can be done in Nuprl's computational
type theory (the difference between CTT and ETT lies essentially in the
semantics of the presuppositions of judgments in the meaning
explanation, where they are relaxed in the former).

Let "A =ext= B" mean that A and B are extensionally equal as types (i.e.
they denote the same partial equivalence relations). In Nuprl, it is
defined using the equality types, something like "eq(A; M; N) <=> eq(B;
M; N)". Crucially, Nuprl's relaxed presuppositions allow this to be a
well-formed proposition even in case it is false, whereas in MLTT or
ETT, this is only wellformed in case it is true. Then, we can say

isErasure E X =def= (X -> E =ext= unit) /\ ((not X) -> E =ext= void).

Perhaps this isn't quite the definition you want, since it actually just
expresses a particular kind of erasure (where inhabitants are replaced
with Ax, the sole inhabitant of Unit); you could of course come up with
some other trivial term MyAx and express a new version of isErasure that
was based on that. Can anyone think of a way to express a more general
predicate, which does not fix in advance the intensional identity
trivial inhabitant? I am not sure it is possible, but it would be
interesting...

Best,
Jon

[Martin Escardo]

On 06/08/15 17:06, Jon Sterling wrote:
> Then, we can say
>
> isErasure E X =def= (X -> E =ext= unit) /\ ((not X) -> E =ext= void).

Looks like E = ¬¬X should always satisfy this, but I don't know the
precise details of the rules of CTT.

Let's take this definition in HoTT as an experiment and see what
happens:

isErasure E X = (X -> E=1) * (¬X -> E=0).

First, with E = ¬¬X this amounts to

(X -> (¬¬X)=1) * (¬X -> (¬¬X)=0)

which is true in HoTT, using functional and propositional
extensionality.

So ¬¬X is an erasure of X according to this notion.

But this is not the only erasure, that is, we don't have

isErasure E X -> E = ¬¬X.

Indeed, the type E=||X|| also satisfies isErasure E X, as this amounts
to

(X -> ||X||=1) * (¬X -> ||X||=0)

which again is true by extensionality.

So, according to this definition, ¬¬X and ||X|| are both (in general
different) erasures of X. But anything between ||X|| and ¬¬X will also
be an erasure, for example a certain type "populated X" that we
considered in a paper on anonymous existence with Kraus, Altenkirch
and Coquand.

Hence this (in its HoTT modification) doesn't uniquely define a notion
of erasure.

But that maybe is fine. Constable's paper wishes to settle with ¬¬(-).

But then I don't see why one would like to have both erase X and ¬¬X
if they are logically equivalent...

Best wishes,
Martin

[Michael Shulman]

On Thu, Aug 6, 2015 at 3:34 AM, Andrej Bauer <andrej...@andrej.com> wrote:
> Are there other notions of propositional truncation? Of course, you
> could take an Lavwere-Tierney operator j : Ω → Ω and define
> j-propositional truncation using the j-stable truth values. But what
> would be some interesting examples of a j-operator?

One particular j that is always definable in type theory is the open
subtopos corresponding to some fixed hprop P:

j(X) := (P -> X).

Another one that is definable with HIT colimits is the analogous
closed subtopos:

j(X) := P +_{P×X} X.

HIT localizations also allow defining a j that localizes at any family
of hprops, i.e. universally sends them all to 1. If you start with
the family of ¬¬-closed hprops, you get just ¬¬ this way. Some other
interesting-looking examples come from taking the family of fibers of
some injective function that is classically an isomorphism, such as
N+1 -> N_oo, or R_C -> R_D.

[Robert Harper]

I find this discussion of time and space complexity strange.  Neither MLTT nor the HoTT variant have any inherent computational meaning.  In particular, they do not have an operational semantics to which one could assign costs.  So what does it mean to talk about terms being "fast" or "small", much less what influence univalence might have on the complexity of terms?

Having said that, I think the gist here has been that the "cost" of univalence is whatever it is in the sense that the equivalence you put in is the equivalence you get out when you use transport, for example.  If a computational meaning is given to terms, then uses of transport would have a cost determined by the cost of executing the particular equivalence to move a value from one fiber of a family to another.

On Tuesday, August 4, 2015 at 7:28:18 PM UTC-4, Matt Oliveri wrote:

On Tuesday, August 4, 2015 at 1:35:38 AM UTC-4, Michael Shulman wrote:

I think we're talking about different things.  If "UA" means the
operation making an equivalence into an identification, then that can
certainly be constant-space.  But *applying* that equivalence to an
*input*, or equivalently transporting across the resulting
identification, can be as slow as you like.

Exactly. I was saying UA itself should be fast. The equivalences it works with may or may not be fast.

If you start with a fast proof that (m + n = n + m) for binary nats, and convert it to a slow proof that (m' + n' = n' + m') for unary nats, this isn't UA's fault. It's because the equivalence between binary and unary nats already includes an exponential-time conversion in both directions. We can write arbitrarily slow programs using univalence, but that doesn't mean univalence is intractable. Similarly, we don't consider for loops intractable just because you can write very slow programs using for loops. The possibility of intractable equivalences does not necessarily mean UA is impractical for programs that you really run. It just means real programs should not feed UA with intractable equivalences.

On Mon, Aug 3, 2015 at 8:55 PM, Piyush P Kurur <p...@cse.iitk.ac.in> wrote:
> On Sun, Aug 02, 2015 at 07:32:54PM -0700, Matt Oliveri wrote:
>> On Sunday, August 2, 2015 at 6:11:09 PM UTC-4, Timothy Carstens wrote:
>> >
>> > Should I walk away with either of these impressions?
>> > 1. Univalence is all about the absence of certain equivalences, rather
>> > than the ability to magically find a suitable identification.
>> > 2. If UA winds up being "computationally effective," and identifications
>> > and equivalences are the same thing, then when I execute a proof which uses
>> > UA via Curry-Howard, the call to the runtime's UA routine will run in
>> > constant-time and constant-memory, since it is indistinguishable from the
>> > identity function.
>> >
>>
>> Well UA definitely isn't magic, but it really does "positively" provide
>> identifications in constructive models.
>>
>> It doesn't seem unreasonable that UA itself would be constant-time and
>> constant-space, but that's an implementation issue. You could ask the
>> authors of existing computational interpretations, like the cubical
>> model(s) how their UA performs.
>
> I thought that UA can potentially be computationally intractable
> (although still computable). After all the UA says that there is an
> equivalence between A and B being equivalent to A and B being equal
> but nothing about how computational hard this mapping could be.
>
> This is not precise but: If we take binary and unary nats since there
> is an exponential blow up in the input sizes in both form, the proofs
> that m + n == n + m when translated from binary to unary can take
> exponential time as measured in the input size.

[Robert Harper]

Yes, but the mathematical tradition doesn't account for computational content.  In NuPRL this aspect is foremost, and thus there is an important distinction between the two forms of squashing described by Jon (and, apparently, there's now a third).  The difference lies in controlling the computational content (what happens when you run things).  In formal type theory there is no inherent computational content, and these distinctions become irrelevant or less important, I think.  I sense that this is related to previous discussions about the surprising "computational content" (largely fictional thus far) of certain proofs.  In our patch theory paper we talk about the computational content of maps into a contractible type, all of which are equivalent and trivial from a mathematical point of view.

On Wednesday, August 5, 2015 at 1:16:21 PM UTC-4, Andrej Bauer wrote:

There is one further, essential difference between propositional
truncation in HoTT/UF and various forms of "brackets" in type theory
-- but this one is in a different direction.

In HoTT/UF concepts are generally defined in terms of mathematical
content. One may *discover* that a type is contractible, or a
proposition, or a set, and this discovery can be a non-trivial piece
of mathematics. I would call this the "mathematical tradition".

In traditional type theories concepts are generally defined in terms
of structure or form. One does not have to "discover" that something
is the unit type, a bracket type, a squash type, or a Coq-style Prop
-- at worst it is a matter of normalization. I would call this the
"logical tradition" or maybe even the "formalist tradition".

The formalist tradition is very strong in the type-theoretic
community, which of course is not a surprise. I have privately
hypothesized before that if a graduate student presented the
univalence axiom and some of its significant consequences at a
workshop, people would just remember it as an interesting but
non-workable idea which broke normalization and generally did things
"the wrong way". I remember the opposition Steve and I met when we
formulated the bracket types; the first thing almost every type
theorist said was "but you have a judgmental equality as a premise in
one of your elimination rules" I never really found out why that was a
faux pas.

One reason for HoTT/UF having created such excitement in the
type-theoretic community is that it brought in some good old
mathematics.

With kind regards,

Andrej

[Robert Harper]

Writing #A for the subsingleton, it is immediate that #A -> ~~A, and I believe that Mark Bickford told me earlier this summer that the converse is essentially Markov's Principle in general form.  It stands to reason because both ~~A and #A are at most inhabited, and if ~~A is inhabited one could in NuPRL postulate that it gives #A without disrupting anything, precisely because we know in advance what the realizer will be.  (A similarly clever trick is used to postulate bar induction in NuPRL, and from it to derive a realizer for bar recursion.)

On Wednesday, August 5, 2015 at 7:34:51 PM UTC-4, Martín Escardó wrote:

On 05/08/15 21:21, Matt Oliveri wrote:

> On Wednesday, August 5, 2015 at 11:03:16 AM UTC-4, Jonathan Sterling wrote:
>
>     Does anyone know if any of the HoTT models would admit a squash type
>     that actually erases computational content?
>
>
> Seems like they would, doesn't it? Using subobjects to do subset-squash?
> But I don't know.

The question, to be repetitive, is what is the difference between (ii)
and (iii) in the absence of excluded middle?

What is the logical/mathematical meaning of the operation "erase"?

That of ¬¬X is clear (namely (X->0)->0), and so is that of ||X||
(essentially forall P. isProp P -> (X->P)->P)). The operation "erase" is
between these two, but it doesn't really have a definition (just an
implementation).

Martin

[Robert Harper]

Yes, I agree with this.  Formal type theory is not inherently computational; NuPRL is inherently computational.  Thus in NuPRL it is both important and possible to discuss explicitly computational concepts such as exceptions (used to prove Brouwer's continuity principle), non-termination (used to ensure universality), and various notions of suppression of computational content.  In the very earliest days we used double-negation for squashing, but it's long since been the case that other forms of squashing are required.  If anyone cares, the "poster child" for squashing was the specification of a function that, given a finite sequence of naturals containing zero, find the first zero in the sequence.  The "obvious" spec admits a constant-time algorithm --- double-negation was used to suppress the unintended information in the premise so that a linear-time algorithm would be forced.  (And note that the concept of time makes sense in NuPRL, which it does not in MLTT.)

So I guess for Nuprl, erase(X) refers to the subset-squash of X. Then yeah. In particular, erase(A x)->¬¬(A x).

The question, to be repetitive, is what is the difference between (ii)
and (iii) in the absence of excluded middle?

What is the logical/mathematical meaning of the operation "erase"?

That of ¬¬X is clear (namely (X->0)->0), and so is that of ||X||
(essentially forall P. isProp P -> (X->P)->P)). The operation "erase" is
between these two, but it doesn't really have a definition (just an
implementation).

I don't know anything about Agda's erase. As for subset in Nuprl, would it be cheating to refer you to the PER semantics? That is something different from Nuprl's implementation.

Informally, imagine you have a computer program. You can reason about it. But none of that reasoning affects the program. It's already compiled and released, say, but we still have the source code, to figure out how bad we screwed up. Well, do you use intuitionistic logic to reason about it, or classical logic? There's some difference, but in neither case is this going to have any effect at all on the program. That's the difference between erase and ¬¬, sort of. Neither of them have nontrivial computational content, but erase is still intuitionistic.

[Robert Harper]

NuPRL does not have a type of propositions, and never has.  We have always subscribed to the philosophy that whether a type expresses a proposition or not is entirely in the mind of the beholder.  One tends to have a propositional attitude (so to speak) towards certain types in certain situations, but there is nothing inherent about a type that makes it a proposition.  Our view was that this is consistent with one of Brouwer's main points, which is that propositions are not hprop's (to use an anachronism), precisely because of disjunction and existence.

[Robert Harper]

I don't see anything wrong with a single realizer being the realizer of many things.  It is a synthetic judgment whether or not a realizer realizes a type/proposition.  For example, in NuPRL axiom realizes all equalities, and * realizes all squashed (in the subsingleton sense) types.  No problem afaik, or did I miss the point?

Of course, being a synthetic judgment, the realization judgment in NuPRL is not at all decidable, nor should it be.  It's a source of great expressive power that it not be the case.  Tactic trees, as they are called, are the explorable records of a proof derivation in a manner not much different from how one explores derivations in Coq --- it is a script that must be executed to understand what is going on, and you can do that exploration incrementally.

[Martin Escardo]

On 07/08/15 00:43, Robert Harper wrote:
> Yes, I agree with this. Formal type theory is not inherently
> computational; NuPRL is inherently computational. Thus in NuPRL it is
> both important and possible to discuss explicitly computational concepts
> such as exceptions (used to prove Brouwer's continuity principle),

I wonder how Brouwer's continuity principle is formulated in NuPrl.

Thanks,
Martin

[Robert Harper]

As Thomas pointed out, NuPRL is based on realizability.  It can be seen as an amped-up version of HEO, because realization is interpreted extensionally.  The equality judgment is then just the expression of the equality associated to the type, and one would not expect that to be decidable in general.  I think it is important to separate the "colon" from the "epsilon".  Formal type theory has a "colon", which is a fancy context-sensitive syntax for terms; computational type theory has an "epsilon", which is extensional realizability.  Once one separates the two clearly, there is less temptation to criticize one for not being the other.

[Robert Harper]

Type theory with "equality reflection" is most certainly "a la Martin-Loef" --- from his Constructive Mathematics and Computer Programming paper.  But computational type theory is not MLTT+ER+UIP.  For one thing ER and UIP are about "colon" and "\equiv", and not about "epsilon" and "=".  But when interpreted in the latter sense, they are true for the NuPRL type theory.  But that is not particularly important; it's the smoke, not the engine.

[Jon Sterling]

Martin,

Re Brouwer's continuity principle, the relevant paper is here:
http://www.nuprl.org/html/Nuprl2Coq/continuity.pdf by Vincent Rahli &
Mark Bickford. The result is of course related to yours, but I think
that seeing it in CTT makes it a bit more clear why one would never
expect the unsquashed version to be true in ITT; the use of exceptions,
which goes back for ages (but is new in CTT) is also very elegant.

Best,
Jon

[Martin Escardo]

On 07/08/15 01:00, Jon Sterling wrote:
> Martin,
>
> Re Brouwer's continuity principle, the relevant paper is here:
> http://www.nuprl.org/html/Nuprl2Coq/continuity.pdf by Vincent Rahli &
> Mark Bickford. The result is of course related to yours, but I think
> that seeing it in CTT makes it a bit more clear why one would never
> expect the unsquashed version to be true in ITT; the use of exceptions,
> which goes back for ages (but is new in CTT) is also very elegant.

Thanks. I saw that paper, actually, but my lack of background on NuPrl
prevents me from fully understanding it. (This whole discussion is
useful for that.)

What form of squashing is used there?

Thanks,
Martin

> Best,
> Jon
>
>
>
> On Thu, Aug 6, 2015, at 04:53 PM, Martin Escardo wrote:
>>
>>
>> On 07/08/15 00:43, Robert Harper wrote:
>>> Yes, I agree with this. Formal type theory is not inherently
>>> computational; NuPRL is inherently computational. Thus in NuPRL it is
>>> both important and possible to discuss explicitly computational concepts
>>> such as exceptions (used to prove Brouwer's continuity principle),
>>
>> I wonder how Brouwer's continuity principle is formulated in NuPrl.
>>
>> Thanks,
>> Martin
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Robert Harper]

sub-singleton, i believe, but that’s off the top of my head.

bob

> You received this message because you are subscribed to a topic in the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/HomotopyTypeTheory/5snMdo3LnP8/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to HomotopyTypeThe...@googlegroups.com.

[Jon Sterling]

To build on Bob's comments, with regard to equality reflection, I would
add that from a Brouwerian point of view you have to understand it in
the same way that any of the (other) elimination rules are understood,
which is to say that it does not express a logical consequence from
premise to conclusion, but rather a material consequence from the
demonstration (experience) of the premise to the demonstration of the
conclusion.

That is to say, all of mathematics is closed under the equality
reflection "rule"; this is also of course the level at which the Bar
Theorem must be understood, since the premise is not merely the various
conditions (sc. R is a decidable bar, A is hereditary upwards, and R is
a subspecies of A), but rather the fact that the subject *has
experienced* the truth of those conditions. The elimination rules of
type theory (or at least its verificationist subsystem) are *theorems*
in the same transcendental sense that the Bar Theorem is.

The Nuprl System is a formal approximation of a type theory with
hypothetical judgment as material consequence; because it is not really
known how to implement such a hypothetical judgment in a practical way,
logical consequence is used instead, and then the deficiency is patched
over by the explicit addition of elimination rules and various induction
principles into the (formal) system. The addition of the weak Bar
Induction principle to Nuprl's formal system is justified in the same
way that the inclusion of elimination rules is justified, which is, by a
transcendental argument about what must be the case in order for the
subject to have experienced the premises.


Martin -- I believe that the Rahli/Bickford paper discussed both kinds
of squashing. The quotient-style squashing (where computational content
is preserved) is written using the lefthand half of a downward arrow,
and the subset-style squash (where computational content is obliterated)
is written with the full downward arrow. The subsingleton squashing is
crucial to their project, since the whole point is to have an operation
which computes the modulus of continuity (so you need to preserve
computational content), but at the same time to prevent anyone from
making an observation that discerns an intensional difference between
two algorithms (since the modulus of continuity is a property of
algorithms, not of functions).

Best,
Jon

On Thu, Aug 6, 2015, at 05:00 PM, Robert Harper wrote:
> Type theory with "equality reflection" is most certainly "a la
> Martin-Loef"
> --- from his Constructive Mathematics and Computer Programming paper.
> But

> computational type theory is *not* MLTT+ER+UIP. For one thing ER and UIP

[Martin Escardo]

On 06/08/15 11:43, Bas Spitters wrote:
> This paper by Peter Aczel contains some variations along these lines:
> http://www.cs.man.ac.uk/~petera/russ-praw.ps.gz

Thanks for sending this link, Bas, which implicitly has the following.

If one defines

Prp = Sigma(P:U).isProp P

and logic

true false : Prp

_∧_ _∨_ _⇒_ : Prp → Prp → Prp

∀ ∃ : {X : U} → (X → Prp) → Prp

as in the HoTT book (where ∨ and ∃ are the propositional reflections
of + and Σ), then one can *prove* that

false = ∀ r. r
p ∧ q = ∀ r. (p ⇒ q ⇒ r) ⇒ r
p ∨ q = ∀ r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
∃ p = ∀ r. (∀ x. p(x) ⇒ r) ⇒ r

which are the definitions in the calculus of constructions.

But there is a difference with CoC, namely that the axiom of
description holds here: for any set X and any p:X→Prp,

(∃! p) = true → Σ(x : X). p(x)=true,

as emphasized by Thierry.

I have proved these two claims in Agda:
http://www.cs.bham.ac.uk/~mhe/impredicativity/logic.html
http://www.cs.bham.ac.uk/~mhe/impredicativity/description.html

Martin

[Gershom B]

On August 5, 2015 at 9:56:14 AM, Martin Escardo (m.es...@cs.bham.ac.uk) wrote:
> ||Sigma(n:N).n is prime & n is the difference of two squares of primes||.
>
> This type is inhabited, and from any term defining an inhabitant,
> you again compute the number 5, by first applying ||-||-recursion
> using the fact that the untruncated type
>
> Sigma(n:N).n is prime & n is the difference of two squares of primes
>
> is a proposition, and then applying the first projection.
>
> Of course, you need a type theory in which ||-|| computes, such
> as cubicaltt.

As an exercise in learning Lean, I coded up a similar example there (using a simpler proposition — that there exists a natural greater than or equal to five and also less than or equal to five), and truncation also sufficiently computed to yield a result.

The code listing follows:

- - - - 

import types.nat types.sigma hit.trunc

open nat sigma is_trunc trunc eq prod

definition isFive : ℕ -> Type.{0} := λ x, prod (5 ≤ x) (x ≤ 5)

definition fiveIsFive : sigma isFive := sigma.mk 5 (prod.mk (le.refl 5) (le.refl 5))

definition isFive.elim {n : ℕ} (x : isFive n) : 5 = n := prod.rec le.antisymm x

definition isFiveIsContr : is_contr (sigma isFive) :=
is_contr.mk fiveIsFive
(λ x, sigma_eq
    (sigma.rec_on x (λ n p, isFive.elim p))
    (sigma.rec_on x (λ n p, pathover_of_tr_eq (prod_eq (is_hprop.elim _ _) (is_hprop.elim _ _)))))

definition isFiveIsTr : is_hprop (sigma isFive) := @is_trunc_of_is_contr _ _ (isFiveIsContr)

definition isFiveTr : trunc -1 (sigma isFive) := tr fiveIsFive

definition elimFromTrunc : ℕ := pr1 (@trunc.elim _ _ _ isFiveIsTr (λ x, x) isFiveTr)

eval elimFromTrunc -- yields 5

Cheers,
Gershom

[Matt Oliveri]

I was just talking about what performance I figure you'd get from a sensible implementation of HoTT. I had said before that that performance is an implementation issue.

On Thursday, August 6, 2015 at 7:25:06 PM UTC-4, Robert Harper wrote:

I find this discussion of time and space complexity strange.  Neither MLTT nor the HoTT variant have any inherent computational meaning.  In particular, they do not have an operational semantics to which one could assign costs.  So what does it mean to talk about terms being "fast" or "small", much less what influence univalence might have on the complexity of terms?

Having said that, I think the gist here has been that the "cost" of univalence is whatever it is in the sense that the equivalence you put in is the equivalence you get out when you use transport, for example.  If a computational meaning is given to terms, then uses of transport would have a cost determined by the cost of executing the particular equivalence to move a value from one fiber of a family to another.

On Tuesday, August 4, 2015 at 7:28:18 PM UTC-4, Matt Oliveri wrote:

On Tuesday, August 4, 2015 at 1:35:38 AM UTC-4, Michael Shulman wrote:

I think we're talking about different things.  If "UA" means the
operation making an equivalence into an identification, then that can
certainly be constant-space.  But *applying* that equivalence to an
*input*, or equivalently transporting across the resulting
identification, can be as slow as you like.

Exactly. I was saying UA itself should be fast. The equivalences it works with may or may not be fast.

[...]

[Matt Oliveri]

On Thursday, August 6, 2015 at 7:51:36 PM UTC-4, Robert Harper wrote:

I don't see anything wrong with a single realizer being the realizer of many things.  It is a synthetic judgment whether or not a realizer realizes a type/proposition.  For example, in NuPRL axiom realizes all equalities, and * realizes all squashed (in the subsingleton sense) types.  No problem afaik, or did I miss the point?

Yes, but that's still one element realized in each type. My understanding is that assemblies let you have one realizer realize multiple elements of the same type. Like () realizing both 0 and 1 in the same assembly, ∇2. I personally find that unintuitive. I'm fine with Nuprl's having a realizer belong to multiple types.

Of course, being a synthetic judgment, the realization judgment in NuPRL is not at all decidable, nor should it be.  It's a source of great expressive power that it not be the case.  Tactic trees, as they are called, are the explorable records of a proof derivation in a manner not much different from how one explores derivations in Coq --- it is a script that must be executed to understand what is going on, and you can do that exploration incrementally.

Completely agree.

[Matt Oliveri]

On Thursday, August 6, 2015 at 11:48:19 AM UTC-4, Martín Escardó wrote:

But what can we say *internally* in type theory about erase X?

In MLTT, ||X|| (if it exists) is the propositional reflection of X,
where a proposition is a type in which any two elements are Id-equal.

We can write the following specification of ||X||, where I use R for
||X|| in MLTT.

isPropReflection R X = isProp R * (X->R)
                     * Pi(P:U). isProp P -> (X->P) -> (R->P)

[...]

Is it possible to complete the following internal definition of
computational erasure, before we know whether it exists?

isErasure E X = ?

What I was getting at in an earlier message is that I think you could say
isErasure E X = ObsProp E * (X->E)
        * Pi(P:U). ObsProp P->(X->P)->(E->P)

The problem is that ObsProp seems to be inexpressible (in MLTT), but informally (ObsProp T) says that T is a subsingleton, up to observational equivalence.

ObsProp might be expressible in Nuprl, but I'm not sure. Nuprl's equality does not always coincide with observational equivalence, and that might mess things up when asking about an arbitrary type.

[Matt Oliveri]

On Thursday, August 6, 2015 at 1:10:45 PM UTC-4, Martín Escardó wrote:

On 06/08/15 17:06, Jon Sterling wrote:
> Then, we can say
>
> isErasure E X =def= (X -> E =ext= unit) /\ ((not X) -> E =ext= void).

Looks like E = ¬¬X should always satisfy this, but I don't know the
precise details of the rules of CTT.

Let's take this definition in HoTT as an experiment and see what
happens:

isErasure E X = (X -> E=1) * (¬X -> E=0).

The problem with this translation is that type equivalence in HoTT is not as strict as PER equivalence. The latter is more like extensional equality of material sets. Your translation defines something sensible, but not what I think Jon was getting at. My attempt at isErasure using ObsProp should actually be weaker than Jon's, since it would allow any realizer as the sole element of an inhabited erasure.

Hence this (in its HoTT modification) doesn't uniquely define a notion
of erasure.

But that maybe is fine. Constable's paper wishes to settle with ¬¬(-).

But then I don't see why one would like to have both erase X and ¬¬X
if they are logically equivalent...

Except they don't seem to be logically equivalent necessarily. Only once you assume ¬¬X->erase(X).

[Steve Awodey]

On Aug 6, 2015, at 5:03 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:

On Thu, Aug 6, 2015 at 3:13 PM, Thomas Streicher <stre...@mathematik.tu-darmstadt.de> wrote:
>

> > But in the set, groupoid, and simplicial set models, it will correspond to “being equivalent to a subterminal” as you say, because one can use the epi-mono factorisation to get a “definitional squashing”, and this preserves fibrations in those models.  And I’d expect that in general, viewing models of TT as quasi-categories (as constructed by Chris Kapulkin), inhabitedness of “isProp(A)” should correspond precisely to being subterminal in the ∞-categorical sense.  This would I guess be rather non-trivial, and quite interesting, to prove!

>
> Does one really know how to interpret type theory in \infty-cats.

> Where has Kris written up this?

A lot is certainly still to be worked out, but Chris’s results have made significant progress, enough for a statement like mine above to be completely precise.

The main writeup is “Locally Cartesian Closed Quasicategories from Type Theory”, http://arxiv.org/abs/1507.02648.  Its main results are: let C be a CwA (or contextual category) with the structure to model Σ-types, Id-types, and Π types with the eta rule and functional extensionality.  Then:

(a) there is a quasi-category N_f(C), constructed from C in a fairly concrete way (in particular, allowing objects and maps of C to be viewed as objects and arrows of N_f(C), well-defined up to equivalence)

Perhaps I’m mistaken, but I thought that the construction of Szumilo that is being used does *not* result in a qcat with the objects and maps of C as the 0- and 1-simplices.  Is that somehow hidden in the phrase “allowing … to be viewed as …, well-defined up to equivalence”? 

Steve

(and moreover N_f(C) is a model for the homotopy coherent nerve of (C, viewed as a category with weak equivalences));

(b) N_f(C) is locally cartesian closed, in the ∞-categorical sense.

He also posted recently on the n-category café about what’s known about the idea that TT should be an internal language for higher categories, and what sorts of things one might hope for: https://golem.ph.utexas.edu/category/2015/07/internal_languages_of_higher_c.html

> Now moving from a model cat to the associated \infty-cat (not at all
> trivial BTW) means replacing equality by weak equivalence.
> Accordingly, I think one cannot interpret judgemental equality in
> \infty-cats! Isn't that a problem?
>

> But there are ways of restoring it since one can find a "representing"
> model cat for sufficiently many \infty-cats (see Szumilo's Thesis for
> the most developed account in this vein). But there are various
> representing model cats.
>
> I tend to think that one can't interpret type theory in \infty-cats
> due to this absence of judgemental equality.

Quite agreed, it’s a highly non-trivial problem!  But I don’t think it’s a non-starter by any means.  The sort of things one could reasonably hope for might be e.g.:

(a) given any lcc quasicategory X, there’s an associated CwA C(X), with Π, Σ, Id-structure as above (maybe constructed via model-categorical presentations of X);

(b) there’s a map ε_X : N_f(C(X)) -> X (a putative co-unit);

(c) maybe ε_X is even an equivalence of quasicategories, or something.

(a) and (b) would I think be enough to justify the statement “type theory [with Σ, Π, Id] can be interpreted in lcc ∞-categories”: it would give a function from (at least) the pure syntax of TT into the objects and arrows of any lccc qcat.  Some form of (c) could moreover justify saying that TT can be used to reason about arbitrary objects, arrows etc. in an lcc ∞-cat.  And obviously one would want to flesh out that picture in lots more ways: do different representing model cats for an lcc qcat give equivalent models of TT, in some sense?  Does the whole thing fit together in an infinity-adjunction?

But in any case, I just want to make the point that the absence (or ill-behavedness) of judgemental equality in quasi-cats isn’t an insurmountable obstacle to interpreting TT in them.  Just like the fact that pullback in LCCC’s isn’t strictly functorial, it’s a technical difficulty that needs to be overcome somehow, but it’s not (hopefully) a deal-breaker.  It tells us that the construction of C(X) from X can’t be as straightforward as the construction of, say, the ETT CwA associated to an LCCC; but that’s ok, and not really awfully surprising.

–p.

[Andrej Bauer]

Your examples are of a single realizer participating in *different*
types, but I am asking whether it is possible to have two different
elements of *the same type* which share a realizer. Is there such a
thing? Probably this question does not even make sense because in
NuPRL the elements of a type *are* the realizers, so you've got PERs
built in.

You can't have a universe in a PER model, at least not a very decent
one. You could of course have a type of *codes* of types, but that's
not really a reasonable universe, as there are lots of PERs without
codes. (This is not a criticism, just an observation.)

With kind regards,

Andrej

[Peter LeFanu Lumsdaine]

On Fri, Aug 7, 2015 at 10:21 AM, Steve Awodey <awo...@cmu.edu> wrote:
>
> The main writeup is “Locally Cartesian Closed Quasicategories from Type Theory”, http://arxiv.org/abs/1507.02648.  Its main results are: let C be a CwA (or contextual category) with the structure to model Σ-types, Id-types, and Π types with the eta rule and functional extensionality.  Then:
>
> (a) there is a quasi-category N_f(C), constructed from C in a fairly concrete way (in particular, allowing objects and maps of C to be viewed as objects and arrows of N_f(C), well-defined up to equivalence)
>
> Perhaps I’m mistaken, but I thought that the construction of Szumilo that is being used does *not* result in a qcat with the objects and maps of C as the 0- and 1-simplices.  Is that somehow hidden in the phrase “allowing … to be viewed as …, well-defined up to equivalence”?

Absolutely, yes — sorry, I didn’t mean to try to hide that.  The 0-cells of N_f(C) can be seen as “resolutions of objects of C”: precisely, a 0-cell of N_f(C) is a semi-simplicial object in C,

C0 <= C1 <≡ C2 …

which is (a) Reedy-fibrant, and (b) such that each of the individual maps C_n -> C_m is a weak equivalence.

Type-theoretically, this can be unwound to be equivalent to “a type equipped with semi-simplicial identity types”: that is, a sequence

C0 : Type

C1 : C0 -> C0 -> Type 

C2 : (x y z:C) -> (C1 x y) -> (C1 y z) -> (C1 x z) -> Type

(the Reedy-fibrant s-s object), together with “reflexivity” terms, and the induction principles for each C_i as an inductive family generated by these reflexivity terms, with “computation” rules holding just up to propositional equality.

Since we can construct s-s id-types over any type, we have a canonical way to view any object of C as a 0-cell of C; and any two systems of s-s id-types over a type are canonically equivalent.

The situation with 1-cells is similar, but harder to write in plain text because the diagrams are 2-dimensional :-)

(NB I’m relying here on having strong Sigma-type, i.e. with the definitional eta-rule, so that every context is judgementally isomorphic to a type.  Without those, we would have to say “context” not type in all the above; it should all still work essentially the same way, I think, but iirc Chris’ paper assumes strong Sigma-types throughout, so I’m following that here.)

–p.

[Robert Harper]

Yes, in NuPRL the elements of a type are (equivalence classes of) realizers.

In NuPRL types are terms so there is no coding involved when forming a universe. In fact there are no types per se, just elements of some universe.

Bob

/RH/

[Thomas Streicher]

On Fri, Aug 07, 2015 at 10:27:08AM -0400, Robert Harper wrote:
> Yes, in NuPRL the elements of a type are (equivalence classes of) realizers.
>
> In NuPRL types are terms so there is no coding involved when forming a universe. In fact there are no types per se, just elements of some universe.

Ah, in NuPRL you change the realizers on the fly! What Andrej and I
are more familiar is realizability over a pca A fixed in advance. And
then the universes one usually constructs there have a trivial realizability
structure, i.e. are of the form \Delta(X), e.g. X = PER(A).

Thomas

[Martin Escardo]

On 07/08/15 04:21, Gershom B wrote:
> On August 5, 2015 at 9:56:14 AM, Martin Escardo (m.es...@cs.bham.ac.uk) wrote:
>> ||Sigma(n:N).n is prime & n is the difference of two squares of primes||.
>>
>> This type is inhabited, and from any term defining an inhabitant,
>> you again compute the number 5, by first applying ||-||-recursion
>> using the fact that the untruncated type
>>
>> Sigma(n:N).n is prime & n is the difference of two squares of primes
>>
>> is a proposition, and then applying the first projection.
>>
>> Of course, you need a type theory in which ||-|| computes, such
>> as cubicaltt.
>
> As an exercise in learning Lean, I coded up a similar example there
> (using a simpler proposition — that there exists a natural greater
> than or equal to five and also less than or equal to five), and
> truncation also sufficiently computed to yield a result.

Nice. Your example is actually equal to mine, assuming univalence. :-)

But not because you compute 5 too.

Notice one thing you can't do with univalence.

In both your example and mine, you compute 5 by applying the first
projection twice.

But the type we are talking about is equal to the unit type 1
too. However, we can't compute 5 by applying the first projection
twice to 1, as of course this doesn't even type check.

I think this (obvious) observation is behind the trouble a number of
people have with univalence.

Martin

[Martin Escardo]

On 07/08/15 00:57, Robert Harper wrote:
> As Thomas pointed out, NuPRL is based on realizability.

Is this just the intended interpretation of NuPRL terms, or the only
possible interpretation of NuPRL terms?

But also: realizability, as I understand it, is a relation between
computational and mathematical objects. (The realizer r realizes the
mathematical object m, written r |= m.)

Here it seems that there are no mathematical objects given in advance
for us to check whether NuPRL realizes them. Rather, it seems, the
mathematical objects are built from realizers (very much like in ZFC we
can build zero as {}, one as {{}}, two as {{{}}} etc., or else choose an
entirely different coding, such as {}, {{}}, {{},{{}}}}, among other
accidental ones).

This seems to be a crucial difference with MLTT, which defines
mathematical objects by their structural properties rather than by their
particular representations by realizers. And yet, it is still able to
compute (by design). In fact, MLTT can be seen as a functional
programming language.

But, more, importantly, it can also be primarily seen as a foundation of
constructive mathematics in which the objects are given by what we can
do with them, rather than by their accidental codings.

HoTT adds extensionality principles to MLTT, and new ways of building
objects by structural properties.

I would say that the daring aspect of HoTT (as alluded to by Andrej) is
that what is considered primary is not how we compute with the new HoTT
objects and principles (which is currently being ellucidated e.g. by the
cubicaltt effort), but rather what their structural properties are.

Martin

> --
> You received this message because you are subscribed to the Google
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to HomotopyTypeThe...@googlegroups.com

> <mailto:HomotopyTypeThe...@googlegroups.com>.

> For more options, visit https://groups.google.com/d/optout.

[Jon Sterling]

Martin,

MLTT in its post-1986 incarnation does not have computational content in
the same sense as it did in the versions starting with "Constructive
Mathematics and Computer Programming" in 1979. It may be used as a
functional programming language only inasmuch as you may post facto fix
the theory and observe a way to direct the judgmental equalities so as
to form a confluent normalization procedure. So it's more of a
metamathematical trick then it is a real example of computational
content...

MLTT in the 1979 style is very similar to Nuprl-style type theory, with
some technical differences; namely the equality of types (in Nuprl it is
intensional, whereas in MLTT it was extensional), and the semantics of
presuppositions (in Nuprl they are relaxed).

Best,
Jon

> email to HomotopyTypeThe...@googlegroups.com.

[Martin Escardo]

Jon: I am surprised to hear that intensional MLTT, being a strongly
normalizing system (even for open terms, as opposed to MLTT with
equality reflection) doesn't have computational content. Best wishes, Martin

[Andrej Bauer]

On Sat, Aug 8, 2015 at 1:59 AM, Robert Harper <bobh...@gmail.com> wrote:
> Brouwer's position was that formalisms are mathematics, and hence cannot constitute mathematics.

Does the "hence" presuppose that "it cannot be mathematics all the way
down"? (I may agree that it is not mathematics all the way down, I am
just asking how one gets to the conclusion.)

[Thomas Streicher]

On Fri, Aug 07, 2015 at 11:53:43PM +0100, Martin Escardo wrote:
> Jon: I am surprised to hear that intensional MLTT, being a strongly
> normalizing system (even for open terms, as opposed to MLTT with
> equality reflection) doesn't have computational content. Best wishes, Martin

I don't take sides but can explain the different views

normalization reduces under the lambda but functional languages don't
and certainly is less efficient

in realizability you may take an untyped functional language as your pca
that's the NuPRL view

NuPRL is certainly related to realizability but in what I have read
the style of exposition is of a kind that it lacks the precision a
logician or category theorist would like

my impression is that they don't have pers but rather subsets and
don't notice when they really use assemblies as in case of the universes

Thomas

[Jon Sterling]

Thomas,

I have a couple of questions.

1. In what sense does Nuprl's semantics not use PERs but rather subsets?
I am not sure I understand how it would be possible to use subsets
instead of PERs since this would not give a proper account of equality &
functionality. Are you saying this based on an analysis of Stuart
Allen's set-theoretic semantics?

2. When did the notion of "assembly" arise in mathematics wrt.
realizability? I have only seen it in modern, technical accounts of
realizability (but would be various interested to hear that it dated
back to Kleene). Nuprl is based directly Kleene's realizability (indeed,
even though he based everything on Gödel codes in his published work,
Constable tells me that Kleene originally worked everything out with
lambda terms), and it may be that their account of realizability has not
kept pace with the modern changes of definition.

3. Could you elaborate on the issue of Nuprl's universes? I must admit
that the explanation of Nuprl's universes became a bit complicated in
order to support the intensional equality that they imposed, and I'm
curious if this is related to what you said.

Best,
Jon

[Robert Harper]

I think so, if I understand you correctly.  Formalisms are mathematical objects, so mathematics is prior to the formalisms.  It cannot be formalisms all the way down, so Brouwer, as I interpret him, sought other forms of foundations based on the creating subject and a basal understanding of computation.

[Martin Escardo]

Bob,

Thanks for your explanation of your view.

I don't want to put words in your mouth (so tell me off if I am wrong):
you seem to say that computation comes first and then mathematics is
derived from it.

I think I have a constructive soul, but my view is that mathematics
comes first and defines and explains computation by mathematically
proving things about it. (I mean: there are physical computers
independently of mathematics. But when we explain what they do, this is
a mathematical expression. And, historically, the design of physical
computers comes from mathematical and logical ideas, which are rather
detached from traditional physics, even though knowledge of physics is
ultimately needed to build a computer.)

MLTT (of its intensional varieties) is attractive to me because it is
compatible both with computation (but is not based on computation
according to your view) and with a non-constructive view of the world
(but is not based on a non-constructive view either).

Anyway, I think we have clarified our respective views, and I respect
yours.

Martin







On 08/08/15 00:59, Robert Harper wrote:
> Martin,
>
> I think you're exactly affirming Jon's point. It's a bit of
> metamathematics to equip certain circumscribed forms of ITT with a
> normalization procedure deciding definitional equality. But the
> metamathematics in question is a bit of mathematics that cannot be
> formulated in ITT itself, undermining the claim that ITT or suchlike is
> foundational. Brouwer's position was that formalisms /are/ mathematics,

> and hence cannot constitute mathematics.
>

> The judgments of ITT have no meaning; they are inductively defined by
> some rules. It has no intrinsic/necessary computational content; that
> some versions admit a normalization procedure is neither here nor there.
> To me this diverges from Brouwer's conception, which of course one is
> free to do. But what I find nice about this viewpoint is that
> computation lies at the foundation from which one develops things like
> formal systems and their models, among many many other things.
>
> NuPRL is probably the most well-developed and faithful realization (pun
> intended) of Brouwer's program. The realizers are lambda terms (modulo
> what amounts to an untyped observational equivalence), as are the types
> they realize. You start with an operational semantics (which,
> emphatically, is not normalization). This induces an operational
> equivalence, upon which one imposes an interpretation of types as
> partial equivalence relations. As such it is a theory of truth, and not
> a theory of proof, as I think I've mentioned before on this list. It is
> most emphatically not the formalism called ETT, as I remarked yesterday.
>
> Best,
> Bob

> <javascript:>
> >>> <mailto:HomotopyTypeThe...@googlegroups.com
> <javascript:>>.

> >>> For more options, visit https://groups.google.com/d/optout

> <https://groups.google.com/d/optout>.

> >>
> >> --
> >> Martin Escardo
> >> http://www.cs.bham.ac.uk/~mhe
> >>
> >> --
> >> You received this message because you are subscribed to the
> Google Groups
> >> "Homotopy Type Theory" group.
> >> To unsubscribe from this group and stop receiving emails from it,
> send an
> >> email to HomotopyTypeThe...@googlegroups.com

> <javascript:>.

> >> For more options, visit https://groups.google.com/d/optout

> <https://groups.google.com/d/optout>.

[Thomas Streicher]

> 1. In what sense does Nuprl's semantics not use PERs but rather subsets?
> I am not sure I understand how it would be possible to use subsets
> instead of PERs since this would not give a proper account of equality &
> functionality. Are you saying this based on an analysis of Stuart
> Allen's set-theoretic semantics?

that was just an impression I got from the discussion
but Bob said it was based on pers and he must know

I didn't study the NuPRL papers too much for reasons I mentioned

> 2. When did the notion of "assembly" arise in mathematics wrt.
> realizability? I have only seen it in modern, technical accounts of
> realizability (but would be various interested to hear that it dated
> back to Kleene). Nuprl is based directly Kleene's realizability (indeed,
> even though he based everything on Gödel codes in his published work,
> Constable tells me that Kleene originally worked everything out with
> lambda terms), and it may be that their account of realizability has not
> kept pace with the modern changes of definition.

I learnt about assemblies from Martin Hyland's talk in September 1985
where he presented Moggi's work on semantics of system F via the
category of modest sets internal to the category of assemblies (see
Martin's "A small complete category").

You need assemblies only for universes and that's why they weren't
considered before.

> 3. Could you elaborate on the issue of Nuprl's universes? I must admit
> that the explanation of Nuprl's universes became a bit complicated in
> order to support the intensional equality that they imposed, and I'm
> curious if this is related to what you said.

You can model universes in modest sets if U is a set of codes. This
was done by Beeson in some paper in the 80s. I didn't like the coding
involved and was looking for something more natural (see Chapter 2 of
my book, more precisely Def.2.8). There U is the set of all pers
endowed with the trivial realizability structure.

So as you incline the NuPRL people were rather considering universes
`a la Beeson. Those validate structural recursive definitions over the
universe whereas the one Andrej and I favour don't.

One cannot say what is the right notion they are just different. But I
never saw too much use in inductive universes because in mathematics
one doesn't want to preform induction over syntactic objects, it's too
intensional as you said.

Thomas

[Matt Oliveri]

On Sunday, August 9, 2015 at 7:13:33 AM UTC-4, Thomas Streicher wrote:

> 3. Could you elaborate on the issue of Nuprl's universes? I must admit
> that the explanation of Nuprl's universes became a bit complicated in
> order to support the intensional equality that they imposed, and I'm
> curious if this is related to what you said.

You can model universes in modest sets if U is a set of codes. This
was done by Beeson in some paper in the 80s. I didn't like the coding
involved and was looking for something more natural (see Chapter 2 of
my book, more precisely Def.2.8). There U is the set of all pers
endowed with the trivial realizability structure.

So as you incline the NuPRL people were rather considering universes
`a la Beeson. Those validate structural recursive definitions over the
universe whereas the one Andrej and I favour don't.

One cannot say what is the right notion they are just different. But I
never saw too much use in inductive universes because in mathematics
one doesn't want to preform induction over syntactic objects, it's too
intensional as you said.

Although Nuprl's semantics do indeed support structural recursion on universes, the type theory actually doesn't allow it. I think there's a different explanation for why Nuprl has stuck with PERs.

Nuprl seems to have the philosophy that elements of types simply are realizers. As Andrej, pointed out, this rules out assemblies. It's a philosophy that makes sense for typed programming languages, but it's not just philosophy. By ruling out assemblies, Nuprl's type system enjoys the property that observationally equivalent elements (equal realizers) are equal (as elements). This allows Nuprl to sometimes reason safely about programs without considering their type. I can't think of any good examples of what that's useful for off the top of my head, but Nuprl would be very different without it.

So using type codes as realizers for universe elements isn't so much because you want to actually use the type codes, but that you need something nontrivial to avoid giving up untyped reasoning. Another option might be to distinguish regular types from "unrealized" types, where you cannot reason about elements via their realizers. So then universes could be unrealized types. But that sounds awfully heavy just to avoid some type codes.

I have to admit though, it feels kind of inelegant to have type codes and not really use them.

[Robert Harper]

I largely, not entirely agree with Matt.  You /do/ want types as codes because types can be and are computed.  No special provision is required to have the type "if b then N else Z" or suchlike.  In NuPRL everything starts out as a program, including types. 

Universes have types as elements, not "codes for types".   There is considerable freedom to choose what equality of elements of the universe is.  Back in 1984/5 we were experimenting with structural universe elim's, and decided for the book to allow for this by defining equality in a universe structurally.  This is only a choice.  One could instead say that two elements are equal in U iff they index the same PER, ie if their elements and equality is the same.  Having a choice is better than not having a choice, and I can see merits in both views.  Perhaps by now NuPRL has changed in this respect; I'm not up to date. 

Thomas, I don't think I get what you mean in saying that NuPRL is not based on PER's, and even less what you mean by saying that it really uses assemblies (because I don't know about them at all).

Bob

/RH/

--
You received this message because you are subscribed to a topic in the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/HomotopyTypeTheory/5snMdo3LnP8/unsubscribe.
To unsubscribe from this group and all its topics, send an email to HomotopyTypeThe...@googlegroups.com.

[Thomas Streicher]

> Thomas, I don't think I get what you mean in saying that NuPRL is not based on PER's, and even less what you mean by saying that it really uses assemblies (because I don't know about them at all).

Ok, so NuPRL is based on PER's over an UNTYPED programming language.
Since this language contains constructors for names of types in the universe
one may consider universes as pers. It's an interesting option to identify
names when they denote the same per.

The reason why some people like me didn't consider this option was
that it doesn't give rise to impredicative universes.

Thomas