I believe this preprint is the first publication on this topic

- Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman,
*Internal parametricity, without an interval*(arXiv:2307.06448)

In section 6 the authors write

We presented a type theory with internal parametricity, a presheaf model and a canonicity proof. It can be seen as a baby version of higher observational type theory (HOTT). To obtain HOTT, we plan to add the following additional features to our theory: * a bridge type which can be seen as an indexed version of $\forall$, * Reedy fibrancy, which replaces spans by relations, * a strictification construction which turns the isomorphism for $\Pi$ types into a definitional equality (in case of bridge, we also need the same for $\Sigma$), * Kan fibrancy, which adds transport and turns the bridge type into a proper identity type. This would also change the correspondence between $\forall U$ and spans into $\forall U$ and equivalences.

a type theorist

]]>The computational rule for dependent function types was mistakenly referred to as for dependent pair types — seemingly a typo. I also moved it to follow immediately after the rule for (non-dependent) function types.

Nate Yazdani

]]>Thanks, I have added the pointer to the github page: here.

But I leave it to others to edit the paragraph on what this accomplishes, such as whether there is a univalently computing homotopy type checker sitting on that github page.

]]>Just a note,

At the moment this seems to remain a hope, certainly there is currently no proof assistant implementing the principles of higher observational type theory. Ideally the references below would elucidate which questions remain open and which problems remain to be solved.

This is not true anymore. Mike Shulman has implemented a proof assistant in Agda: https://github.com/mikeshulman/ohtt.

]]>Coming back to this thread, prompted by discussion in another thread (here):

The previous idea section of this entry seemed to me to convey essentially no real idea of the topic at hand. Also in view of comment #6 above, I have therefore taken the liberty of deleting it and writing a new Idea-section from scratch: here.

Incidentally, also the technical material in the bulk of the entry seems not to convey much relevant information. But that part I haven’t touched yet.

]]>the added text was originally from the HoTT wiki; I have no idea how accurate it is.

Anonymous

]]>I see, thanks. This would be worth expanding on in the entry.

]]>My understanding is that it really is defined analogous to a relation that is functional, total, injective and surjective, not a bijection. So correspondence in the sense of eg algebraic geometry (ie a span) really is suitable.

]]>The entry was referring (here) to “one-to-one correspondences”, with a broken link. From the context I am assuming that *bijective* correspondences are meant, and so I have fixed the link accordingly. But experts please check. Best to replace “one-to-one” by a proper technical term.

Also, do you really want to point to *correspondence* = *span*? Maybe all of “one-to-one correspondence” needs to be replaced by “bijection”, or something like this.

how about we replace “higher dimensional” with “higher homotopy” ?

hyperlinked “HoTT” (!)

replaced “universe” by “type universe”

maybe “primitive type” would deserve to be hyperlinked

hyperlinked “proof of types” as “proof of types”

hyperlinked “Mike Shulman”

$\;$

By the way, we never had remotely as many edits signed by “Anonymous”. It’s great to see so much activity, and of good quality, too!. But it’s dizzying that all edits carry the same signature. Is this all from a single anonymous contributor? Might I kindly ask that you (all?) choose some pseudonym, so that (you remain anonymous but) we are able to distinguish authors by their signature? Thanks!

]]>Page created, but author did not leave any comments.

Anonymous

]]>