[-- 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 --]

[-- Attachment #1: Type: text/plain, Size: 2361 bytes --] While UniMath doesn't use much automation internally, Coq has very rich facilities for it. Using UniMath as a base for your development doesn't prevent you from using e.g. Ltac for automating proof scripts. Even if you decide to develop without using Coq's automation, I would bet you'll save more time by reusing UniMath's extensive development of category theory than you would by using any sort of proof automation. Here are some resources on automation in Coq: - Tutorial: http://adam.chlipala.net/cpdt/html/Match.html - Reference: https://coq.inria.fr/refman/proof-engine/ltac.html On Sun, Jan 6, 2019 at 8:57 AM José Manuel Rodriguez Caballero < josephcmac@gmail.com> 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. > > -- > 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. > -- 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: 3598 bytes --]

The HoTT Coq library (https://github.com/HoTT/HoTT) uses somewhat more automation than UniMath, I believe. In particular, the category theory library that it contains (https://arxiv.org/abs/1401.7694) was developed using many of Chlipala's automation techniques. On Mon, Jan 7, 2019 at 9:58 AM Langston Barrett <langston@galois.com> wrote: > > While UniMath doesn't use much automation internally, Coq has very rich facilities for it. Using UniMath as a base for your development doesn't prevent you from using e.g. Ltac for automating proof scripts. > > Even if you decide to develop without using Coq's automation, I would bet you'll save more time by reusing UniMath's extensive development of category theory than you would by using any sort of proof automation. > > Here are some resources on automation in Coq: > - Tutorial: http://adam.chlipala.net/cpdt/html/Match.html > - Reference: https://coq.inria.fr/refman/proof-engine/ltac.html > > On Sun, Jan 6, 2019 at 8:57 AM José Manuel Rodriguez Caballero <josephcmac@gmail.com> 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. >> >> -- >> 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. > > -- > 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. -- 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.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 --]

[-- Attachment #1: Type: text/plain, Size: 4488 bytes --] > > Juan wrote: > A trivial example of Hott with Lean... In my case, I learned UniMath just from Voevodsky's video lectures at Oxford (I was not there): Point 9 in this link: https://www.math.ias.edu/vladimir/Lectures I am interested to get back to HoTT, after some time focused in Isabelle/HOL, just for pleasure (my serious job is with Isabelle/HOL). What I love of HoTT is the idea of thinking in a topological way about non-topological problems: this is like a video-game for me, not a project, it is something just for fun. Here is an example of one of my theorems in UniMath (a greedy generalization of Euclidean division). As you can see, automation is almost zero in my program. I guess that it will be shorted in Lean or in Coq (using the HoTT library). [Another motivation is that I have the intuition that HoTT is related to the combinatorics of finite fields via the Weil Conjectures, but I need more experience before to formalize this intuition, e.g., given a type, we can express its topological invariants as the number of points on a variety over a finite field and the correspondence is "natural". This may be non-sense.] Unset Automatic Introduction. (** *** Imports *) Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Foundations.PartA. Definition Increasing := fun (f : nat -> nat) => forall n : nat, f n ≤ f (S n). Lemma powerMonotonic : forall f : nat -> nat, Increasing f -> ( forall n k : nat, f n ≤ f (n + k) ). Proof. intros. intros. induction k. rewrite natplusr0. apply (natlehmplusnm 0 (f n) ). change (S k) with (1 + k). rewrite (natpluscomm 1 k). rewrite <- (natplusassoc n k 1). unfold Increasing in X. specialize (X (n + k)). change (S (n + k)) with (1 + (n + k)) in X. rewrite ( natpluscomm 1 (n + k) ) in X. apply (istransnatleh IHk X). Defined. Definition SIncreasing := fun (f : nat -> nat) => forall n : nat, f n < f (S n). Lemma SpowerMonotonic : forall f : nat -> nat, SIncreasing f -> ( forall n k : nat, f n < f (n + k + 1) ). Proof. intros. intros. induction k. rewrite natplusr0. rewrite -> (natpluscomm n 1). change (1 + n) with (S n). unfold SIncreasing in X. specialize (X n). apply X. change (S k) with (1 + k). rewrite (natpluscomm 1 k). rewrite <- (natplusassoc n k 1). unfold SIncreasing in X. specialize (X (n + k + 1)). rewrite -> (natpluscomm (n + k) 1) in X. change (S (1 + (n + k))) with (1 + (1 + (n + k))) in X. rewrite <-( natplusassoc 1 1 (n + k) ) in X. rewrite -> ( natpluscomm (1 + 1) (n + k) ) in X. rewrite -> ( natplusassoc n k (1 + 1) ) in X. rewrite -> ( natplusassoc (n + k) 1 1 ). rewrite -> ( natpluscomm (n + k) 1 ) in IHk. assert (T := istransnatlth (f n) (f (1 + (n + k))) (f (n + (k + (1 + 1)))) ). rewrite -> ( natplusassoc n k (1 + 1) ). apply T. apply IHk. apply X. Defined. Lemma SpowerLargerThanN : forall f : nat -> nat, SIncreasing f -> ( forall n : nat, (f 0) + n ≤ f n ). Proof. induction n. rewrite (natplusr0 (f 0)). apply (natlehmplusnm 0). rewrite <- ( plus_n_Sm (f 0) n). apply (natlehandplusl (f 0 + n) (f n) 1 ) in IHn. change (1 + (f 0 + n)) with (S (f 0 + n)) in IHn. change (1 + f n) with (S (f n)) in IHn. unfold SIncreasing in X. specialize (X n). apply (natlthtolehsn) in X. apply ( istransnatleh IHn X ). Defined. Definition EuclidF := fun (f : nat -> nat) (x : dirprod nat nat) => (f (pr1 x)) + (pr2 x). Definition GreedyEuclid (f : nat -> nat) (isSIncreasing : SIncreasing f) (n : nat) : dirprod nat nat. Proof. intros. induction n as [ | n x]. - intros. apply (dirprodpair (f 0) 0). - induction (natlthorgeh ((f (pr1 x)) + S (pr2 x)) (f (S (pr1 x)))). + apply ( dirprodpair (pr1 x) (S (pr2 x)) ). + apply ( dirprodpair (S (pr1 x)) (0) ). Defined. Lemma GreedyEuclidLem : forall (f : nat -> nat), SIncreasing f -> forall n : nat, hfiber (fun (x : dirprod nat nat) => EuclidF f x) ((f 0) + n). Proof. intros. unfold hfiber. exists (dirprodpair 0 n). unfold EuclidF. simpl. apply idpath. Defined. -- 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: 6178 bytes --]