A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom

Re:A self-contained, brief and complete formulation of Voevo... by Jeff_Brown on Friday March 02, 2018 @11:42AM (#16503085)

Is there any obvious application of this in software design?

[ Parent | on HN ]

Re:A self-contained, brief and complete formulation of Voevo... by SolarNet on Friday March 02, 2018 @08:26PM (#16507261)

Type systems.

[ Parent | on HN ]

Re:A self-contained, brief and complete formulation of Voevo... by Jeff_Brown on Friday March 02, 2018 @08:36PM (#16507301)

What will it let me represent that extant type systems don't?

[ Parent | on HN ]

Re:A self-contained, brief and complete formulation of Voevo... by SolarNet on Thursday March 08, 2018 @06:09AM (#16543650)

Nothing. However it will provide a consistent basis for translating a wider variety of systems to existing type systems.

[ Parent | on HN ]