Write-up of Vladimir's proposal for strict identity types?

[Jason Gross]

Hi,

I find myself talking about a type for judgmental/strict equality without really understanding it.  (For example, I think that all witnesses of strict equality strictly equal, but I don't know how that's proven/enforced.)  Is there a write-up somewhere of Vladimir's proposal, or of experience implementing it?

Thanks,

Jason

[Andrej Bauer]

The notes are at
https://uf-ias-2012.wikispaces.com/file/view/HTS.pdf/410120566/HTS.pdf

The "experience of implementing it" is at
https://github.com/andrejbauer/tt. It is literally hapenning right now
and is not ready for public consumption -- fork at your own risk.

Speaking of which, I am looking for a *simple* lemma that uses the
computational rule for propositional truncation. I want to formalize
it in tt, where I can define propositional truncation (with judgmental
computation rule because tt allows that), but the proof terms need to
be written out in full with bare hands.

With kind regards,

Andrej

> --
> 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/groups/opt_out.

[Michael Shulman]

One problem with the system as formulated there is that it postulates
that an inductive type is fibrant as soon as its arguments are, but
this is not true in all models. Even the empty type is not
necessarily fibrant. One can of course fibrantly replace an inductive
type, but the result will only be able to eliminate into other fibrant
types.

[Jason Gross]

Thanks for the reference!

How about the lemma that functional extensionality (as defined from having || Bool ||), when applied to (fun _ => refl) gives the proof refl that f = f?  The statement of the lemma, in Bruno Barras' Coq with HITs, is short.  Here is the entire file, using the interval rather than truncation of bool (because that's easier to define).  (I don't have a nice proof, though, yet.)

Inductive interval :=

| zero : interval

| one : interval

with paths :=

| seg : zero = one.

Definition ap A B (f : A -> B) x y (p : x = y) : f x = f y

  := match p in (_ = y) return f x = f y with

       | eq_refl => eq_refl

     end.

Definition transport_const A B x y z p

: eq_rect x (fun _ : A => B) y z p

  = y

  := match p as p in (_ = z) return eq_rect x (fun _ : A => B) y z p = y with

       | eq_refl => eq_refl

     end.

Definition funext A (B : A -> Type) (f g : forall a, B a) (H : forall x, f x = g x)

: f = g

  := @ap _ _

         (fun (i : interval) x =>

            fixmatch {h} i with

              | zero => f x

              | one => g x

              | seg => eq_trans (transport_const _ _ _ _ _ _) (H x)

            end)

         _ _

         seg.

Definition funext_refl A B f : @funext A B f f (fun _ => eq_refl) = eq_refl.

-Jason

[Michael Shulman]

On Thu, Mar 6, 2014 at 10:47 AM, Andrej Bauer <andrej...@andrej.com> wrote:

> The notes are at
> https://uf-ias-2012.wikispaces.com/file/view/HTS.pdf/410120566/HTS.pdf

Or (as of now):
http://ncatlab.org/homotopytypetheory/files/HTS.pdf

[Vladimir Voevodsky]

I have a very clear position on this kind of issues.

I see the main goal of the program to be the development of languages, software and training solutions which are needed in order to introduce in mathematics and eventually other sciences routine use of computers for verification and unambiguous dissemination of knowledge.


At this stage what we need is a formal deduction system which as closely as possible approximates the properties of the world of mathematical objects. The fact that Quillen model categories do not reflect these properties means that we should not, on the main line of software development, worry about model categories.


Vladimir.

[Michael Shulman]

Fortunately, there is room inside the subject for people with many
different goals. I think I'm not the only one who feels that it's
important that any foundational system for mathematics -- especially a
constructive one -- supports a flexible semantics allowing the
construction of things like sheaf and realizability models. The point
isn't about Quillen model categories per se -- it might be that there
are other ways to construct models which don't use them, and indeed
model categories are ultimately unsatisfactory because they probably
won't suffice to construct new models of HoTT inside of existing ones.
The point is rather that we should design a system which is flexible
enough to accomodate such models and represent their logic faithfully.

HTS is actually *more* closely tied to model categories than other
type systems are, since it includes explicitly the notion of
"fibrancy". This creates another, deeper, problem, which I've also
recently mentioned on the blog: its semantics are not
homotopy-invariant. Two different model categories that present the
same homotopy theory can nevertheless have distinguishable "internal
languages" in the HTS sense, while this is probably not true of other
type systems in use. Here are a couple of comments that describe what
I'd like to see in a type theory with two equalities:
http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/#comment-21553
http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/#comment-21567

Mike

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

[Vladimir Voevodsky]

On Mar 6, 2014, at 1:47 PM, Andrej Bauer <andrej...@andrej.com> wrote:

> Speaking of which, I am looking for a *simple* lemma that uses the
> computational rule for propositional truncation.

Here is something a bit different but related.

The following should be true in HTS:

forall x y : nat , paths x y -> Id x y

where paths is the univalent and Id the substitutional (strict) identity types.

I have an approximate plan for proving it and tried to do it on paper but it is just a bit too complex for this. It should be a really good test for any implementation.

V.

[Vladimir Voevodsky]

On Mar 7, 2014, at 5:11 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> HTS is actually *more* closely tied to model categories than other
> type systems are, since it includes explicitly the notion of
> "fibrancy".

This is a good point and from the very beginning I felt that this is a hack since the introduction of this notion is guided purely by the ideas of homotopy theory rather than by philosophical or syntactic ideas.

But it is the only potentially workable attempt to combine ``intensive" and ``extensive" features in one type theory which I know of and we should be able to learn from it. And having an implementation should give us a base to try various things and to discover what the actual, as opposed to expected based on general intuition, issues are.

> This creates another, deeper, problem, which I've also
> recently mentioned on the blog: its semantics are not
> homotopy-invariant. Two different model categories that present the
> same homotopy theory can nevertheless have distinguishable "internal
> languages" in the HTS sense, while this is probably not true of other
> type systems in use. Here are a couple of comments that describe what
> I'd like to see in a type theory with two equalities:
> http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/#comment-21553
> http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/#comment-21567

You say that fibrant types are locally but not globally homotopy invariant. I could not find (doing search on "global") the meaning of this distinction on this page. Could you point out an explanation?

V.

[Michael Shulman]

On Sat, Mar 8, 2014 at 10:28 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> This is a good point and from the very beginning I felt that this is a hack since the introduction of this notion is guided purely by the ideas of homotopy theory rather than by philosophical or syntactic ideas.
>
> But it is the only potentially workable attempt to combine ``intensive" and ``extensive" features in one type theory which I know of and we should be able to learn from it. And having an implementation should give us a base to try various things and to discover what the actual, as opposed to expected based on general intuition, issues are.

I like that philosophy. I would be worried if you were proposing HTS
as "the right way to do things", but if it's just an idea to explore
the design space with, then I'm all for it.

> You say that fibrant types are locally but not globally homotopy invariant. I could not find (doing search on "global") the meaning of this distinction on this page. Could you point out an explanation?

What I meant was that one can write down a fibrant type A such that
there are two model categories C and D which present the same homotopy
theory, but such that A is inhabited in the C-model of type theory but
not in the D-model. I admit that I haven't sat down to write out a
particular such A, but I think it's easy to see that such must exist.

Consider, for instance, the model category of simplicial sets, and the
Reedy model category sSet^2 (where 2 is the arrow category) localized
in such a way as to make the codomains of fibrant objects
contractible. These present equivalent homotopy theories, but because
the model categories themselves are different as 1-toposes, and the
non-fibrant types see the underlying ordinary category, one should be
able to write down a non-fibrant type (indeed, a "strict hprop") that
is inhabited in one of them and not in the other. Now just fibrantly
replace it. (Or, if you don't want to include a fibrant-replacement
type former, consider a non-fibrant strict-hprop P and then form
Paths_U(P,1), which exists and is fibrant since the universe U of all
types is fibrant.)

Mike

[Vladimir Voevodsky]

On Mar 8, 2014, at 1:46 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> Consider, for instance, the model category of simplicial sets, and the
> Reedy model category sSet^2 (where 2 is the arrow category) localized
> in such a way as to make the codomains of fibrant objects
> contractible. These present equivalent homotopy theories, but because
> the model categories themselves are different as 1-toposes, and the
> non-fibrant types see the underlying ordinary category, one should be
> able to write down a non-fibrant type (indeed, a "strict hprop") that
> is inhabited in one of them and not in the other. Now just fibrantly
> replace it. (Or, if you don't want to include a fibrant-replacement
> type former, consider a non-fibrant strict-hprop P and then form
> Paths_U(P,1), which exists and is fibrant since the universe U of all
> types is fibrant.)

Paths_U(P,Q) is inhabited for all P and Q because U is contractible.

The first half of your example I do not understand because I am not familiar with properties of Reedy model structures.

Do you have that in your category(ies) the unit is not cofibrant? Because being inhabited is equivalent to there being a morphism from the unit and if the unit is cofibrant and the type is fibrant existence of such a morphism is a property of the homotopy category.

V.

[Michael Shulman]

On Sat, Mar 8, 2014 at 2:08 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> Paths_U(P,Q) is inhabited for all P and Q because U is contractible.

This is true in the simplicial model, and I guess probably in many or
most model categories. Is it provable inside of HTS?

I knew that U is contractible, but apparently I hadn't fully thought
through the consequences. In particular, I see now that one of those
consequences is that there *cannot* be a generic fibrant-replacement
type former: if there were, it would be a map R : U -> U_F, and so by
contractibility of U, every fibrantly-replaced type R(A) would be
equivalent to every other.

Probably you knew this already, since you've thought about this system
a lot more than I have. I was assuming that Peter Lumsdaine's and my
construction of (fibrant) higher inductive types would in particular
yield a fibrant-replacement type former in HTS, but now I see that a
crucial one of the hypotheses of that construction (that the
endofunctor preserves fibrations) is not satisfied in this case.

> Because being inhabited is equivalent to there being a morphism from the unit and if the unit is cofibrant and the type is fibrant existence of such a morphism is a property of the homotopy category.

The unit is cofibrant. The point is rather that, at least under
certain hypotheses, there should be a "fibrant" syntactic type whose
interpretations in the two models do not have the same homotopy type
(even though both are fibrant). The not-necessarily-fibrant fragment
of HTS, interpreted in a model category C, is just the ordinary
1-categorical internal logic of C; in particular, it knows nothing
about the model structure on C. Thus, if two model categories C and D
have underlying categories with different internal logics, there
should be a non-fibrant syntactic type whose interpretation in C is
inhabited but whose interpretation in D is not. (I'm still working on
coming up with a specific example, sorry.)

Then the question becomes just whether given a non-fibrant type A, we
can construct a fibrant one whose inhabitation depends on that of A.
If we had fibrant replacement, this would do the job, but now I see
that we don't. However, I think we could still postulate a fibrant
replacement of any *particular* type in the empty context, since
cartesian product with an arbitrary object preserves acyclic
cofibrations (in simplicial sets, and in at least some other models).
This is admittedly slightly weird, but I think it's enough for the
example of non-invariance.

Mike

[Steve Awodey]

On Mar 10, 2014, at 8:35 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> On Sat, Mar 8, 2014 at 2:08 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>> Paths_U(P,Q) is inhabited for all P and Q because U is contractible.
>
> This is true in the simplicial model, and I guess probably in many or
> most model categories. Is it provable inside of HTS?
>
> I knew that U is contractible, but apparently I hadn't fully thought
> through the consequences. In particular, I see now that one of those
> consequences is that there *cannot* be a generic fibrant-replacement
> type former: if there were, it would be a map R : U -> U_F, and so by
> contractibility of U, every fibrantly-replaced type R(A) would be
> equivalent to every other.

could you spell this out a bit, please?
first off, in what sense is the universe U contractible?
it can’t be a 0-type, so you must mean something else.

thanks,

Steve

[Michael Shulman]

We're talking about the universe of *non-fibrant* types. In the
simplicial model of HTS, this universe is (I believe) represented by
the simplicial set

U_n = { arbitrary simplicial maps with codomain \Delta^n }

(suitably strictified). This happens to be a Kan complex, indeed a
contractible Kan complex. Interpreted in terms of lifting properties,
the latter statement says that U -> 1 is an acyclic fibration, i.e.
that given a simplicial map f : A -> B and a monomorphism g : B -> C,
there is a map h : D -> C such that f is the pullback of h along g.
This is easy; just let h = gf.

HTS assumes that the universe of non-fibrant types is itself fibrant;
it's not clear to me whether it assumes or proves that this universe
is contractible. But it is contractible in the simplicial model, and
the contractibility really is in the usual sense of homotopy type
theory with reference to the "Paths" identity type of HTS.

[Vladimir Voevodsky]

On Mar 10, 2014, at 8:35 PM, Michael Shulman <shu...@sandiego.edu> wrote:

On Sat, Mar 8, 2014 at 2:08 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

Paths_U(P,Q) is inhabited for all P and Q because U is contractible.

This is true in the simplicial model, and I guess probably in many or
most model categories.  Is it provable inside of HTS?

This is a good question. I do not know.

V.

[Vladimir Voevodsky]

On Mar 10, 2014, at 8:35 PM, Michael Shulman <shu...@sandiego.edu> wrote:

The point is rather that, at least under
certain hypotheses, there should be a "fibrant" syntactic type whose
interpretations in the two models do not have the same homotopy type
(even though both are fibrant).  

We are talking about two model categories which have the same homotopy category, right? Are you saying there can be two models which do not agree on fibrant types after the projection to the homotopy category? There can be, but this does not require non-fibrant types.

Or do you mean two models which agree on the Martin-Lof ``core" of the type system but differ on some fibrant types which can not be constructed entirely inside the core? 

The conjecture which is at the very end of my 2013 slides implies that this is impossible: a fibrant type T is an object of the universe of fibrant types U which belongs to the core system. Therefore, according to the conjecture, there is a type T' which belongs to the core and an equivalence T == T'. Therefor the type T is inhabited in a model iff T' is inhabited in a model and the value of the model on T' does not depend on the choice of a model category. 

V.

[Michael Shulman]

On Tue, Mar 11, 2014 at 7:08 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> Are you saying there can be two models which do not agree
> on fibrant types after the projection to the homotopy category? There can
> be, but this does not require non-fibrant types.

What example do you have in mind? I don't think we've formally proven
that any two models of core Martin-Lof type theory in equivalent model
categories agree (up to homotopy) on all types, but it seems likely to
me, and I think Peter Lumsdaine had a good idea for how to approach
proving it.

Mike

[Vladimir Voevodsky]

One model sends U to one univalent universe and another one to another (e.g. bigger) one.

I think this is pretty much all the choice one has for the univalent models but there is this choice.

V.

[Michael Shulman]

Oh, that's uninteresting. I'm saying that even if you fix the values
of all the universes (up to homotopy), then the presence of
non-fibrant types should (under certain other hypotheses) allow you to
construct fibrant types whose interpretations in the two models have
different homotopy types.

[Vladimir Voevodsky]

On Mar 11, 2014, at 12:08 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> Oh, that's uninteresting. I'm saying that even if you fix the values
> of all the universes (up to homotopy), then the presence of
> non-fibrant types should (under certain other hypotheses) allow you to
> construct fibrant types whose interpretations in the two models have
> different homotopy types.

Great. This would refute the conjecture from my talk which would be very interesting.

V.

[Michael Shulman]

I am a little puzzled about this conjecture; I thought the whole point
of HTS was to be able to define things like the (fibrant) type of
semisimplicial types that we *couldn't* do in MLTT?

On Tue, Mar 11, 2014 at 9:16 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

>
> On Mar 11, 2014, at 12:08 PM, Michael Shulman <shu...@sandiego.edu> wrote:
>
>> Oh, that's uninteresting. I'm saying that even if you fix the values
>> of all the universes (up to homotopy), then the presence of
>> non-fibrant types should (under certain other hypotheses) allow you to
>> construct fibrant types whose interpretations in the two models have
>> different homotopy types.
>

[Vladimir Voevodsky]

On Mar 11, 2014, at 12:47 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> I am a little puzzled about this conjecture; I thought the whole point
> of HTS was to be able to define things like the (fibrant) type of
> semisimplicial types that we *couldn't* do in MLTT?

The expression for the core-subsystem object in the conjecture may be very much longer than the expression for the original object. In particular this conjecture would imply that there is a way to define semi-simplicial types without the strict equality but the definition may be too long and convoluted to be of practical use.


V.

[Michael Shulman]

I see, thanks. I've added this conjecture to the open problems list
on the new wiki.

[Jason Gross]

On Sat, Mar 8, 2014 at 1:11 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

The following should be true in HTS:

forall x y : nat , paths x y -> Id x y

where paths is the univalent and Id the substitutional (strict) identity types.

I have an approximate plan for proving it and tried to do it on paper  but it is just a bit too complex for this. It should be a really good test for any implementation.

V.

If I understand correctly, you could prove that forall x y : nat, (Id x y) + ~(paths x y) (where ~A is A -> False), by induction on natural numbers, and this suffices, as follows:

Set Implicit Arguments.

Axiom Id : forall A, A -> A -> Type.

Axiom paths : forall A, A -> A -> Type.

Axiom refl : forall A (a : A), Id a a.

Axiom idpath : forall A (a : A), paths a a.

Axiom not_paths_0_S : forall n, paths 0 (S n) -> False.

Axiom not_paths_S_0 : forall n, paths (S n) 0 -> False.

Axiom Id_S : forall n m, Id n m -> Id (S n) (S m).

Axiom paths_pred : forall n m, paths (S n) (S m) -> paths n m.

Definition nat_dec : forall x y : nat, (Id x y) + (paths x y -> False).

Proof.

  induction x; induction y.

  - left; apply refl.

  - right; apply not_paths_0_S.

  - right; apply not_paths_S_0.

  - destruct (IHx y).

    + left; apply Id_S; assumption.

    + right. intro H. apply paths_pred in H; auto.

Defined.

Definition paths_to_id : forall x y : nat, paths x y -> Id x y.

Proof.

  intros x y H.

  destruct (nat_dec x y).

  - assumption.

  - exfalso; auto.

Defined.

I think the only required interesting bits are that succ and pred respect Id and paths, respectively, and, if I understand HTS correctly, both of these proofs are trivial by the appropriate J rule.

Furthermore, any type which, in Coq, has decidable equality and injective constructors (injective over the paths type), should have this strong form of decidable equality, I think, where we get (Id x y) + (~paths x y).

Did I make any mistakes?

-Jason

      

 

[Vladimir Voevodsky]

I think you did not make any mistakes and I think your argument is very cool!

Vladimir.

[Michael Shulman]

This is cool, but it does depend on assuming that nat is fibrant and
yet can eliminate into non-fibrant types, which I don't think one
should. If nat is not fibrant, then according to HTS it doesn't have
a paths type; while your proof requires inducting over x and y with a
non-fibrant motive (Id x y) + (paths x y -> False).

> --
> 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.

[Vladimir Voevodsky]

On Mar 15, 2014, at 12:27 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> This is cool, but it does depend on assuming that nat is fibrant
> and yet can eliminate into non-fibrant types,

I think that for a system which we need to work with mathematical objects (and in particular to explore other less intuitive systems) this is a completely reasonable assumption.

One may ask if something useful can be gained by having a system without it but this should not slow us down in the development of a system for practical use.

V.

[Michael Shulman]

On Sat, Mar 15, 2014 at 10:17 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> I think that for a system which we need to work with mathematical objects (and in particular to explore other less intuitive systems) this is a completely reasonable assumption.

I'm a little confused, because you've said that you're uncomfortable
with how HTS seems to be just mimicking what happens in a model
category; but it seems to me that the only justification for this
assumption is that it happens accidentally to be the case in the
particular model category of simplicial sets. Surely if mimicking
model categories is undesirable, then mimicking one particular model
category is worse?

Here also is a philosophical argument for why we shouldn't make this
assumption. A fibrant type is one which is "invariant", i.e. whose
elements can be transported across paths and equivalences. I see no a
priori reason to assume that every possible construction of a natural
number is automatically invariant in this way, at least as long as we
are allowing *some* non-invariant constructions in our system.

Mike

[Vladimir Voevodsky]

On Mar 15, 2014, at 1:46 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> On Sat, Mar 15, 2014 at 10:17 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>> I think that for a system which we need to work with mathematical objects (and in particular to explore other less intuitive systems) this is a completely reasonable assumption.
>
> I'm a little confused, because you've said that you're uncomfortable
> with how HTS seems to be just mimicking what happens in a model
> category; but it seems to me that the only justification for this
> assumption is that it happens accidentally to be the case in the
> particular model category of simplicial sets. Surely if mimicking
> model categories is undesirable, then mimicking one particular model
> category is worse?

Not really. This particular category (not “model category” - just category) happens to produce using the notion of a Kan simplicial set *the* homotopy category which is of a central importance for the whole of mathematics. Therefore, using its properties to inform our choices for the practical type system is, from my point of view, reasonable.

The general notion of a model category relates to a field of mathematics (theory of Quillen model categories) which does not have a central position in mathematics as a whole. In fact the self-dual nature of the model categories precludes them from being very useful even for the study of interesting homotopy categories other than *the* homotopy category such as, for example, motivic homotopy categories. Therefore, using the properties of general model categories to inform our choices for the practical type system is, from my point of view, unreasonable.

V.

>
> Here also is a philosophical argument for why we shouldn't make this
> assumption. A fibrant type is one which is "invariant", i.e. whose
> elements can be transported across paths and equivalences. I see no a
> priori reason to assume that every possible construction of a natural
> number is automatically invariant in this way, at least as long as we
> are allowing *some* non-invariant constructions in our system.
>
> Mike
>

[Vladimir Voevodsky]

On Mar 15, 2014, at 1:46 PM, Michael Shulman <shu...@sandiego.edu> wrote:

Here also is a philosophical argument for why we shouldn't make this
assumption.  A fibrant type is one which is "invariant", i.e. whose
elements can be transported across paths and equivalences.  I see no a
priori reason to assume that every possible construction of a natural
number is automatically invariant in this way, at least as long as we
are allowing *some* non-invariant constructions in our system.

I am not sure what you mean by this. We are not talking about some possible construction of natural numbers but about a very particular type nat which is the inductive type with known constructors.

V.

[Vladimir Voevodsky]

(cont.) We can for example define N’ as the type nat \times A where A is some contractible type with many objects which are not strictly equal to each other. Than this N’ will not satisfy the strict decidability (as Jason calls it) nor will it have the property that forall x y : N’, paths x y -> Id x y . 

V.

 

[Michael Shulman]

On Sat, Mar 15, 2014 at 10:55 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> Not really. This particular category (not "model category" - just category)

Once you start talking about fibrant objects, you have to be thinking
of it as a model category (or at least some fragment of the structure
of a model category).

> happens to produce using the notion of a Kan simplicial set *the* homotopy category which is of a central importance for the whole of mathematics.

But there are also plenty of other model categories which produce the
same homotopy category, and in some of which Nat is not fibrant. Why
should we privilege a particular model of the homotopy category?

Additionally, as I've said before, I think even privileging a
particualar homotopy category is a bad idea. Topos theory, set
theory, and constructive mathematics have taught us that it's
important to be able to pass from one "base" mathematical universe to
another.

Mike

[Michael Shulman]

On Sat, Mar 15, 2014 at 10:57 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>> I see no a
>> priori reason to assume that every possible construction of a natural
>> number is automatically invariant in this way, at least as long as we
>> are allowing *some* non-invariant constructions in our system.
>
> I am not sure what you mean by this. We are not talking about some possible
> construction of natural numbers but about a very particular type nat which
> is the inductive type with known constructors.

And why should we believe that every way to define an element of that
particular type is homotopy-invariant? In set theory, there are
plenty of ways to define a natural number that are not
homotopy-invariant, such as "the number of objects of category C".

Mike

[Vladimir Voevodsky]

All these may be true from the perspective of doing mathematics. But I am talking about building software which we can then use to do mathematics.

V.

[Vladimir Voevodsky]

because there is only one way to define an object of nat and it is by iterating application of the constructor S to the constructor O ?

V.

[Michael Shulman]

On Sat, Mar 15, 2014 at 11:16 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> All these may be true from the perspective of doing mathematics. But I am talking about building software which we can then use to do mathematics.

But once we realize that we should do mathematics in a particular way,
then we'd better build our software to support that! What good is it
to have software that doesn't let us do mathematics in the way we want
to do it?

Maybe it would make my position clearer to say the following: if we
could prove that starting from HTS, we could construct other models of
HTS using higher sheaves, realizability, etc., then I would withdraw
any objection. This is the criterion that I think is essential for
whatever type theory(ies) we eventually "settle on". If we had a type
theory with that property, then it wouldn't matter to me if the only
way to "get into that world" from classical set theory was by using
accidental properties of a particular model category like simplicial
sets.

With this in mind, there are two reasons I bring up other model
categories right now. Firstly, we currently don't have *any* type
theories that are known to be closed under the above constructions, so
our only way to obtain other models is by defining higher sheaves etc.
inside of set theory (with model categories) and *then* building a
model of type theory out of them. This is not as good as what I think
we eventually need, but at least it's something, so I don't want to
throw it away. And secondly, I think the behavior of model categories
may suggest to us ways in which the eventual desired "internal"
constructions on models of type theory may behave. In particular, the
fact that nat is not fibrant in many model categories suggests to me
that if we build a higher sheaf model internally to HTS, the nat in
that model might also not naturally be fibrant.

>> And why should we believe that every way to define an element of that
>> particular type is homotopy-invariant? In set theory, there are
>> plenty of ways to define a natural number that are not
>> homotopy-invariant, such as "the number of objects of category C".
>
> because there is only one way to define an object of nat and it is by
> iterating application of the constructor S to the constructor O ?

That's also true in set theory...

[Vladimir Voevodsky]

On Mar 15, 2014, at 2:31 PM, Michael Shulman <shu...@sandiego.edu> wrote:

>>> And why should we believe that every way to define an element of that
>>> particular type is homotopy-invariant? In set theory, there are
>>> plenty of ways to define a natural number that are not
>>> homotopy-invariant, such as "the number of objects of category C".
>>
>> because there is only one way to define an object of nat and it is by
>> iterating application of the constructor S to the constructor O ?
>
> That's also true in set theory...

Yes! The properties of sets are usually quite well (but inconveniently from the computational point of view) captured by the set theory.

Mike, my concerns are with people doing analysis, number theory, differential geometry, physics. It’s them who we need to convince that our system is powerful enough to enable them to build things in the way they are used to but with the additional help of the computers.

For this we need a system which is as strong as possible (in your terms which has as few models as possible) not the other way around.

V.

[Urs Schreiber]

On 3/15/14, Vladimir Voevodsky <vlad...@ias.edu> wrote:

> Mike, my concerns are with people doing analysis, number theory,
> differential geometry, physics. It's them who we need to convince that our

Mike's points would be catering for those who would do differential
geometry and physics synthetically instead of analytically. There is
an argument to be made that that's the more practical way to go about
formalization in these complex fields.

[Michael Shulman]

On Sat, Mar 15, 2014 at 12:53 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> Mike, my concerns are with people doing analysis, number theory, differential geometry, physics. It's them who we need to convince that our system is powerful enough to enable them to build things in the way they are used to but with the additional help of the computers.

If all you want is to let mathematicians build things in the same old
way that they're used to, then why bother with univalence? It seems
to me that extensional type theory, maybe with resizing for props,
would be best for that. The way I see it, the whole point of homotopy
type theory is that it gives us new and *better* ways to do old
things.

I have faith that if we put our effort into developing a system that
is flexible, powerful, and well-designed from a theoretical and
mathematical point of view, it will turn out to be powerful enough for
everyday use by mathematicians. Right now we're still exploring the
design space of homotopy type theories. I think it's a bit premature
to put a lot of effort into convincing analysts, say, that we have a
good system for them to use; it'd be better to wait until we *have* a
really good system, so that they won't need to keep relearning the
system as we improve it.

Mike

[Jacques Carette]

On 2014-03-15 5:29 PM, Michael Shulman wrote:
> I have faith that if we put our effort into developing a system that
> is flexible, powerful, and well-designed from a theoretical and
> mathematical point of view, it will turn out to be powerful enough for
> everyday use by mathematicians.

Might I humbly suggest that you also worry about such a system being
well-designed from a CS and software engineering point of view? If
nothing else, the history of current systems shows very clearly that you
ignore software engineering issues at your own peril.

Furthermore, you might do yourself a favour and learn what has worked
well, and what were the serious mistakes of previous systems, by talking
with the people who have built previous large systems (some of them have
been doing so for decades). Coq and Agda are fantastic foundational
systems, but their standard libraries are *tiny*. Even Gonthier's
"Mathematical Components" library is (at best) medium sized. The
libraries of Mizar, Maple and Mathematica are much (much!) larger, and
still only cover a small fraction of mathematics, and only from a rather
particular perspective.

The community of people who build the "systems for all of mathematics"
tend to meet at CICM [1] each summer. Many of us are extremely excited
about HoTT, because it does fix some fundamental problems in the
foundations. But foundations are just one part of building a usable
system. There are user-interface issues, knowledge management issues,
'scaling' issues, efficiency issues, and so on, to deal with if you hope
to build a system which will be used by a lot of people.

So let me invite all of you to come and chat with us. What you are
doing is extremely interesting to us -- and we might be able to save you
a lot of effort by showing you what else we've learned system building
also entails.

Jacques [now going back to lurker mode]

[1] http://cicm-conference.org/2014/

[Bas Spitters]

Hi Jacques,

Thanks for the invitation.
We are of course thinking about such issues. In fact, many of us precisely are attracted to UF because it solves the issues of the previous generation of (type theory based) proof assistants.

Could you quantify the difference in size between Coq and Mizar developments, perhaps also taking into account that Mizar appears to be more verbose?

BTW: There was a suggestion that MathScheme's "little theories" approach may be able to handle some aspects of transports of structures under isomorphisms, like in UF.

Do you think that is a fair statement?

Best,

Bas

Of course, after going to CICM people can continue through to ITP.
http://www.cs.uwyo.edu/~ruben/itp-2014/

--
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 HomotopyTypeTheory+unsub...@googlegroups.com.

[Michael Shulman]

Dear Jacques,

Thanks for your suggestions! Maybe I misunderstand, but I don't think
there is any conflict between what I said and what you suggest. I was
talking about the design of the foundational system itself, whereas it
sounds to me like you're talking about its implementation. I'm sure
you're absolutely right that anyone implementing any system to
formalize mathematics in could learn a lot from already existing
projects about the software engineering issues involved.

Mike