Equivalences

[andrejbauer]

Reorganize equivalences so that they use canonical structures. Also think about what to call the various files, it is a bit silly that we have a file called UsefulEquivalences.v.

[jcmckeown]

does "use canonical structures" include meaning to eschew Record in favor of sigT? Or can we ask Matthieu to reimplement Records as sugar for nested dependent sums? because it's troublesome to have FiberEquivalences proved for fibrations but also have to repeat the same proofs for trivially-different record types.

[andrejbauer]

Implementing records as nested sigT would be quite useless. In any case, Mike came up with a tactic which shows that a record is equivalent to a corresponding sigT. And anyhow, I have not had to use these equivalences too often. By the way, the ssreflect branch of HoTT is what you should be looking at. We're soon going to merge it into master. (Don't be alarmed by the branch name, the ssreflect stuff is optional and is not working at the moment.) We're using typeclasses instead of canonical structures. Records are a must for that sort of thing.

[mattam82]

On 16 janv. 2013, at 09:34, Andrej Bauer notifications@github.com wrote:

Implementing records as nested sigT would be quite useless. In any case, Mike came up with a tactic which shows that a record is equivalent to a corresponding sigT. And anyhow, I have not had to use these equivalences too often. By the way, the ssreflect branch of HoTT is what you should be looking at. We're soon going to merge it into master. (Don't be alarmed by the branch name, the ssreflect stuff is optional and is not working at the moment.) We're using typeclasses instead of canonical structures. Records are a must for that sort of thing.

Records are a lot better than sigTs currently because of their use as canonical structures/typeclasses and also regarding type annotations in terms, but this might change with a better treatment of projections and constructors in the kernel (WIP). The nesting issue will not go away though. Indeed it's easy to show that they're iso, and if I we are to eat our own food, anyway, by univalence they're equal.

-- Matthieu

[spitters]

I posted this suggestion a while ago. @Matthieu does that seem feasible?

A record is just a macro generating an inductive type. http://coq.inria.fr/doc/Reference-Manual004.html

One could consider extending this macro to generate both the inductive "record" type and an iterated Sigma-type and a proof that they are equivalent/equal. See also Randy's fundamental paper: http://homepages.inf.ed.ac.uk/rpollack/export/recordsFAC.ps.gz

There is a wish here: http://uf-ias-2012.wikispaces.com/Proof+assistant+wishlist to internalize this macro, the suggestion above may be easier to implement.

On Wed, Jan 16, 2013 at 3:49 AM, Matthieu Sozeau notifications@github.com wrote:

On 16 janv. 2013, at 09:34, Andrej Bauer notifications@github.com wrote:

Implementing records as nested sigT would be quite useless. In any case, Mike came up with a tactic which shows that a record is equivalent to a corresponding sigT. And anyhow, I have not had to use these equivalences too often. By the way, the ssreflect branch of HoTT is what you should be looking at. We're soon going to merge it into master. (Don't be alarmed by the branch name, the ssreflect stuff is optional and is not working at the moment.) We're using typeclasses instead of canonical structures. Records are a must for that sort of thing.

Records are a lot better than sigTs currently because of their use as canonical structures/typeclasses and also regarding type annotations in terms, but this might change with a better treatment of projections and constructors in the kernel (WIP). The nesting issue will not go away though. Indeed it's easy to show that they're iso, and if I we are to eat our own food, anyway, by univalence they're equal.

-- Matthieu

— Reply to this email directly or view it on GitHub.

[mattam82]

Yes, it is feasible, and the other way as well: take a sigma type and derive it's representation as a record. I would generalize this to: take a telescope with a certain number of parameters, derive either the sigma (with projections) or the record type from it. A generic Ltac can do the correspondence proof. Sadly I just don't have time to devote to it, but I can provide guidance to anyone who'd like to write it :)

[jcmckeown]

It's all very well, Matthieu, to say that "in univalence" the two types are identifiable, but the specific identification still has to be made explicit somewhere; it's only canonical w.r.t. the presentation of the Type, but presentations are for the kernel to know, not for the type they present.

Andrej: when I checkout branch ssreflect, am I going to be terribly confused again?

[mikeshulman]

I committed the tactic I wrote that Andrej referred to (to Andrej's fork, since mine is hopelessly stuck in the dark ages):

https://github.com/andrejbauer/HoTT/blob/9dacc54b0b411b85a7c32c7009bdd66085191243/theories/types/Record.v

I'm very much still a novice at Ltac, so suggestions and improvements (or totally different approaches) would be verywelcome.

On Wed, Jan 16, 2013 at 2:17 AM, Matthieu Sozeau notifications@github.comwrote:

Yes, it is feasible, and the other way as well: take a sigma type and derive it's representation as a record. I would generalize this to: take a telescope with a certain number of parameters, derive either the sigma (with projections) or the record type from it. A generic Ltac can do the correspondence proof. Sadly I just don't have time to devote to it, but I can provide guidance to anyone who'd like to write it :)

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/34#issuecomment-12312121.

[JasonGross]

I was looking at https://github.com/andrejbauer/HoTT/blob/9dacc54b0b411b85a7c32c7009bdd66085191243/theories/types/Record.v, and noted that you comment on line 14 that, "Since Coq doesn't automatically define recursors for records, the following placeholder has to be a match over the record type. But we can't write that match without knowing the record constructors, and having the tactic caller pass them in doesn't seem to be enough. So we leave this term to be defined with tactics instead." Have you encountered the pattern let (x, y) := foo in bar which, I think, automatically desugars to the appropriate match over any record type with two projections?

[JasonGross]

Here's a tactic that works:

Ltac issig fibration record pr1 pr2 :=
  refine (BuildEquiv _ _ (fun u => record u.1 u.2)
    (isequiv_adjointify _
      (fun v => existT fibration (pr1 v) (pr2 v))
      (fun v => let (x, y) return (record (pr1 v) (pr2 v) = v) := v in 1)
      (fun u =>
        match u return
          (existT fibration
            (pr1 (record (u.1) (u.2)))
            (pr2 (record (u.1) (u.2))))
          = u with
          existT x y => 1
        end))).

I'm trying to figure out what your adjointifying comment means, and I'll probably also look at speeding up the last tactic that you comment is slow.

[mikeshulman]

Ah, we've been working in parallel. Thanks for the suggestion: I got it working, without adjointify: https://github.com/mikeshulman/HoTT/blob/record/theories/types/Record.v But now the analogous issig3 version actually fails (after spinning for a very long time)! I must be doing something wrong.

[mikeshulman]

Oh, duh, we need three destructs for a triply nested sigma type. Still doesn't explain why it takes forever.

[JasonGross]

I suspect that it's spinning for a long time either on typeclass resolution or something like that. A trick I often use when I want a term but don't know what it is, but want to know it's type is let T := fresh in let t := fresh in evar (T : Type); evar (t : T); subst T and then I use ts instead of holes.

[mikeshulman]

After a lot of help from Jason, these tactics seem to be working fairly well, without adjointify. The 4-component one is still a bit slow, but at least it's not ridiculous.

[jcmckeown]

Incidentally, for these equivalences, are you identifying a rec (pr1 : t1 ; pr2 : t2 pr1; pr3 :t3 pr1 pr2 ) with sig t1 (t => sig (t2 t1) (s => t3 t1 s)) or with sig (sig t1 (t => t2 t)) (s => t3 s.1 s.2)) ??

[mikeshulman]

The former.

On Wed, Feb 6, 2013 at 10:17 AM, jcmckeown notifications@github.com wrote:

Incidentally, for these equivalences, are you identifying a rec (pr1 : t1 ; pr2 : t2 pr1; pr3 :t3 pr1 pr2 ) with sig t1 (t => sig (t2 t1) (s => t3 t1 s)) or with sig (sig t1 (t => t2 t)) (s => t3 s.1 s.2)) ??

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/34#issuecomment-13186535.

[mikeshulman]

I suggest we continue discussion of the various points raised here at other appropriate places (if necessary). We're already using Records via typecasses, and there is an issue "Port UsefulEquivalences" that can include deciding what to rename it or where to put its contents. There's also an issue "Complete types/Record" that can include deciding whether to improve the Record tactics further, or whether there is a better approach.