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

Re:A self-contained, brief and complete formulation of Voevo... by pacala on Thursday March 01, 2018 @11:21PM (#16498982)

Dilettante here: What's interesting about *TT is that people have built mechanical theorem checkers [Coq, Agda, Lean, ...], and people are working on building automated theorem provers based on those programatic foundations.

[ Parent | on HN ]

Re:A self-contained, brief and complete formulation of Voevo... by EtDybNuvCu on Thursday March 01, 2018 @11:23PM (#16498999)

Check out Metamath; we can do this for any serious foundations: http://us.metamath.org/downloads/metamath.pdf

[ Parent | on HN ]

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

Have somebody done it for the more general foundations based on category theory? If I understand correctly, Metamath is a set of tools enabling such a formulation, but not the formulation itself. See ML vs. theorem prover implemented in ML.

[ Parent | on HN ]

Re:A self-contained, brief and complete formulation of Voevo... by mbid on Friday March 02, 2018 @12:37PM (#16503759)

There are some developments, for example "Globular": https://arxiv.org/abs/1612.01093

I don't think there is a proof assistant that's really based on categorical foundations. I'd love to see something like that though.

[ Parent | on HN ]