Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] The best proof assistant for HoTT from the point of view of automation
@ 2019-01-06 16:57 José Manuel Rodriguez Caballero
  2019-01-07 17:58 ` Langston Barrett
  2019-01-08  1:06 ` Juan Ospina
  0 siblings, 2 replies; 5+ messages in thread
From: José Manuel Rodriguez Caballero @ 2019-01-06 16:57 UTC (permalink / raw)
  To: HomotopyTypeTheory

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

Hello,
  After reading the (beautiful) paper

Paredes, Belén. "Boson-Lattice Construction for Anyon Models." arXiv
preprint arXiv:1804.01605 (2018).
https://arxiv.org/pdf/1804.01605.pdf

I was rather motivated to explore modular tensor categories:
https://ncatlab.org/nlab/show/modular+tensor+category

using a proof assistant. My preferred proof assistant is Isabelle/HOL,
because of the hight level of automation, but I am not sure that simple
type theory is the best formal system to work with modular tensor
categories. As far as I know, HoTT has been used in order to formalize
category theory in a rather successful way. In my case, I programmed a
little bit in UniMath (Coq), but thee automation was almost zero (maybe
there is some automation, but I did not know how to use it, everything that
I learned in computer sciences was self-taught).

So, I wonder in which proof assistant HoTT can be used with a maximum of
automation.

Kind Regards,
José M.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 5+ messages in thread

end of thread, other threads:[~2019-01-08  1:55 UTC | newest]

Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-01-06 16:57 [HoTT] The best proof assistant for HoTT from the point of view of automation José Manuel Rodriguez Caballero
2019-01-07 17:58 ` Langston Barrett
2019-01-07 20:57   ` Michael Shulman
2019-01-08  1:06 ` Juan Ospina
2019-01-08  1:54   ` José Manuel Rodriguez Caballero

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).