Email Gateway (Aug 22 2022 at 18:32): Email Gateway (Aug 22 2022 at 18:32):From: Joshua Chen <joshua.chen@uni-bonn.de>
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
Email Gateway (Aug 22 2022 at 18:32):From: Lawrence Paulson <lp15@cam.ac.uk>
We already have
lemma card_permutations:
assumes "card S = n"
and "finite S"
shows "card {p. p permutes S} = fact n"
in HOL/Library/Permutations.thy.
Larry
Email Gateway (Aug 22 2022 at 18:32):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Indeed,
lemma card_permutations:
assumes "card S = n"
and "finite S"
shows "card {p. p permutes S} = fact n"
is the set-level truncation (h-level 2) of the theorem proved by Voevodsky
Theorem weqfromweqstntostn ( n : nat ) : ( (⟦n⟧) ≃ (⟦n⟧) ) ≃ ⟦factorial n⟧
which is about homotopy types (a generalization of sets). In traditional
mathematics, card_permutations is enough for all applications. Voevodsky's
homotopy type-theoretic generalization of card_permutations is important
from the point of view of category theory, because of its functoriality.
Nevertheless, theorems like weqfromweqstntostn are just vanguardist
experiments for now.
Kind Regards,
Jose M.
References:
Truncation in type theory:
https://ncatlab.org/nlab/show/n-truncated+object+of+an+%28infinity%2C1%29-category
Voevosky's homotopy type-theoretic approach to combinatorics (Lecture 6,
part 2 in 9. Oxford lectures on UniMath):
https://www.math.ias.edu/vladimir/Lectures
El mar., 18 sept. 2018 a las 14:11, Lawrence Paulson (<lp15@cam.ac.uk>)
escribió:
Last updated: Nov 21 2024 at 12:39 UTC