Re: [HoTT] The best proof assistant for HoTT from the point of view of automation

[Juan Ospina <jospina65@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1776 bytes --]



On Sunday, January 6, 2019 at 11:57:57 AM UTC-5, José Manuel Rodriguez 
Caballero wrote:
>
> 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.
>



A trivial example of Hott with Lean 


import homotopy.cylinder
open cylinder
check cylinder_rel 
check cylinder
check base
check top
check seg
constants {A B : Type} (f : A → B)
constant {c : A}
variables {g : A -> A}


example (c : A) : base f (f (g c))  = top f (g c) :=
begin
  rewrite seg
end
 

-- 
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 #1.2: Type: text/html, Size: 3411 bytes --]