Our great sponsors
-
redtt
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
-
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
In the case of transpension, it seems like one of the uses is proving something about a path in inductive types by cases on an abstract point along that path. For instance, right now, the way that you prove that a path in A + B is either a path in A or a path in B is to define a family by cases and then transport like here. But I think transpension might let you just do cases on a formal intermediate point directly, which would be much simpler.
NOTE:
The number of mentions on this list indicates mentions on common posts plus user suggested alternatives.
Hence, a higher number means a more popular project.
Related posts
- Austral: A systems language with linear types. (2021)
- Lolita: A tagless, dependently typed, self-aware programming language
- Semgrep – Find bugs and enforce code standards
- Toy autograd engine in OCaml with Apple Accelerate back end
- Application Security - Bridging Frontend and Cybersecurity: What is Application Security?