Email Gateway (Aug 22 2022 at 18:32): Email Gateway (Aug 22 2022 at 18:32):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Josh wrote
Suggestions,
hints and general comments are always appreciated!
Before passing away, Voevodsky was developing combinatorics from his
univalence axiom, e.g., he proved the well-known theorem which states that
the number of permutations of n elements is the factorial of n. Indeed, in
the UniMath Library we find this theorem (written in Coq):
Theorem weqfromweqstntostn ( n : nat ) : ( (⟦n⟧) ≃ (⟦n⟧) ) ≃ ⟦factorial n⟧.
Link:
https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/StandardFiniteSets.v
So, to prove this theorem in Isabelle will be a nice exercise.
Kind Regards,
Jose M.
Message: 5
Date: Tue, 18 Sep 2018 12:17:05 +0200
From: "Joshua Chen" <joshua.chen@uni-bonn.de>
Subject: [isabelle] HoTT logic release
To: cl-isabelle-users@lists.cam.ac.uk
Message-ID: <web-10744476@be4.uni-bonn.de>
Content-Type: text/plain;charset=iso-8859-1; format="flowed"Dear Isabelle community,
I'm very pleased to announce the first beta release of a
homotopy type theory object logic I've been working on.
This logic implements intensional Martin-Löf type theory
with univalent cumulative Russell-style universes, and is
polymorphic.
Some methods for automating proofs are also provided.Work on this logic is still very much ongoing, for example
higher inductive types have not yet been implemented, and
concatenating equality types is still not automated.
In principle, however, the logic should be able to
formalize much of the first half of the Homotopy Type
Theory book.The logic can be found at
https://github.com/jaycech3n/Isabelle-HoTT. Suggestions,
hints and general comments are always appreciated!Best wishes,
Josh
Last updated: Nov 21 2024 at 12:39 UTC