Re: [HoTT] Identity versus equality

[Nicolai Kraus <nicola...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 5896 bytes --]

In the last paragraph of my message below, the words "deep" and "shallow"
have to be swapped.

On Sun, May 10, 2020 at 5:51 PM Nicolai Kraus <nicola...@gmail.com>
wrote:

> Dear André and everyone,
>
> I feel it's worth pointing out that there are two strategies to express
> "everyday mathematics" in HoTT. In CS-speak, they would probably be
> called "shallow embedding" and "deep embedding". Shallow embedding is
> the "HoTT style", deep embedding is the "pre-HoTT type theory style".
> Shallow means that one uses that the host language shares structure with
> the object one wants to define, while deep means one doesn't. To explain
> what I mean, let's look at the type theoretic definition of a group (a
> 1-group, not a higher group).
>
> Definition using deep embedding: A group is a tuple
> (X,h,e,o,i,assoc,...), where
>    X : Type     -- carrier
>    h : is-0-truncated(X)     -- carrier is set
>    e : X   -- unit
>    o : X * X -> X     -- composition
>    i : X -> X     -- inverses
>    assoc : (h o g) o f = h o (g o f)
>    ... [and so on]
>
> Definition using shallow embedding: A group is a pointed connected 1-type.
>
> Fortunately, these definitions are equivalent (via the Eilenberg-McLan
> spaces construction). But they behave differently when we want to work
> with them or change them. It's easy to change the second definition to
> define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 ,
> arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there
> is a nice way for the first definition. The second definition has better
> computational properties than the first.
>
> When you say this:
>
>  > But I find it frustrating that I cant do my everyday mathematics with
> it.
>  > For example, I cannot  say
>  >
>  > (1) Let X:\Delta^{op}---->Type be a simplicial type;
>
> You are referring to shallow embedding. In everyday mathematics, you
> don't say (1) either. You probably say (1) with "Type" replaced by "Set"
> or by "simplicial set". Both of these can be expressed straightforwardly
> in type theory using only (h-)sets (i.e. embedding deeply).
>
> We strive to use shallow embedding as often as possible for the reasons
> in the above example. But let's assume that we *can* say (1) in HoTT,
> using "Type", because we find some encoding that we're reasonably happy
> with; there's a question which I've asked myself before:
>
> Will we not destroy the advantages of deep (over shallow) embedding if
> we fall back to encodings (and thus destroy the main selling point of
> HoTT)? For me, the justification of still using deep embedding is that
> statements using encodings (e.g. "the universe is a higher category)
> might still imply statements which don't use encodings and are
> interesting. However, if we want to develop a theory of certain higher
> structures for it's own sake, then it's not so clear to me whether it's
> really better to use the HoTT-style deep embedding.
>
> Kind regards,
> Nicolai
>
>
> On 09/05/2020 21:18, Joyal, André wrote:
> > Dear Thomas,
> >
> > You wrote
> >
> > <<In my opinion the currenrly implemented type theories are essentially
> > for proving and not for computing.
> > But if you haven't mechanized PART of equational reasoning it would be
> > much much more painful than it still is.
> > But that is "only" a pragmatic issue.>>
> >
> > Type  theory has very nice features. I wish they could be preserved and
> developped further.
> > But I find it frustrating that I cant do my everyday mathematics with it.
> > For example, I cannot  say
> >
> > (1) Let X:\Delta^{op}---->Type be a simplicial type;
> > (2) Let G be a type equipped with a group structure;
> > (3) Let BG be the classifying space of a group G;
> > (4) Let Gr be the category of groups;
> > (5) Let SType be the category of simplical types.
> > (6) Let Map(X,Y) be the simplicial types of maps X--->Y
> > between two simplicial types X and Y.
> >
> > It is crucial to have (1)
> > For example, a group could be defined to
> > be a simplicial object satisfying the Segal conditions.
> > The classifying space of a group is the colimit of this simplicial
> object.
> > The category of groups can be defined to be
> > a simplicial objects satisfiying the Rezk conditions (a complete Segal
> space).
> >
> > Is there some aspects of type theory that we may give up as a price
> > for solving these problems ?
> >
> >
> > Best,
> > André
> >
> > ________________________________________
> > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
> > Sent: Saturday, May 09, 2020 2:43 PM
> > To: Joyal, André
> > Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey;
> homotopyt...@googlegroups.com
> > Subject: Re: [HoTT] Identity versus equality
> >
> > Dear Andr'e,
> >
> >> By the way, if type theory is not very effective in practice, why do we
> insist that it should always compute?
> >> The dream of a formal system in which every proof leads to an actual
> computation may be far off.
> >> Not that we should abandon it, new discoveries are always possible.
> >> Is there a version of type theory for proving and verifying, less
> >> for computing?
> > In my opinion the currenrly implemented type theories are essentially
> > for proving and not for computing.
> > But if you haven't mechanized PART of equational reasoning it would be
> > much much more painful than it still is.
> > But that is "only" a pragmatic issue.
> >
> >> The notations of type theory are very useful in homotopy theory.
> >> But the absence of simplicial types is a serious obstacle to
> applications.
> > In cubical type theory they sort of live well with cubes not being
> > fibrant... They have them as pretypes. But maybe I misunderstand...
> >
> > Thomas
> >
>
>

[-- Attachment #2: Type: text/html, Size: 7081 bytes --]