The HoTT Game
What is the HoTT Game? from thehottgameguide.readthedocs.io The Homotopy Type Theory (HoTT) Game is a project written by mathematicians for mathematicians interested in HoTT and no experience in proof verification, with the aim of introducing cubical agda as a tool for trying out mathematics in HoTT. You can find it here. Much of the content of the game is based on the HoTT book and lectures by Ro
Cubical Agda | Homotopy Type Theory
Last year I wrote a post about cubicaltt on this blog. Since then there have been a lot of exciting developments in the world of cubes. In particular there are now two cubical proof assistants that are currently being developed in Gothenburg and Pittsburgh. One of them is a cubical version of Agda developed by Andrea Vezzosi at Chalmers and the other is a system called redtt developed by my collea
HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics
SQL is the lingua franca for retrieving structured data. Existing semantics for SQL, however, either do not model crucial features of the language (e.g., relational algebra lacks bag semantics, correlated subqueries, and aggregation), or make it hard to formally reason about SQL query rewrites (e.g., the SQL standard’s English is too informal). This post focuses on the ways that HoTT concepts (e.g
Higher Lenses
Lenses are a very powerful and practically useful functional construct. They represent “first class” fields for a data structure. Lenses arose in work on bidirectional programming (for example, in Boomerang), and in Haskell, people have given many different definitions of lenses, but the simplest and easiest to replicate in type theory is probably the one based on getters and setters. Given types
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
A self-contained, brief and complete formulation of Voevodsky’s univalence axiom
A hands-on introduction to cubicaltt
Combinatorial Species and Finite Sets in HoTT
The Lean Theorem Prover
Double Groupoids and Crossed Modules in HoTT
The torus is the product of two circles, cubically
Universal properties without function extensionality
Higher inductive-recursive univalence and type-directed definitions
Homotopy Type Theory should eat itself (but so far, it’s too big to swallow)
The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible
The HoTT Book