-
Notifications
You must be signed in to change notification settings - Fork 324
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[create-pull-request] automated change (#1453)
- Loading branch information
1 parent
79eff4b
commit 446338b
Showing
2 changed files
with
28 additions
and
0 deletions.
There are no files selected for viewing
15 changes: 15 additions & 0 deletions
15
.../isomorphism-invariance-and-isomorphism-reflection-in-type-theory-types-2023.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
--- | ||
title: Isomorphism invariance and isomorphism reflection in type theory (TYPES 2023) | ||
description: | ||
url: http://math.andrej.com/2023/06/15/types-2023-isomorphism-invariance-and-isomorphism-reflection/ | ||
date: 2023-06-14T22:00:00-00:00 | ||
preview_image: | ||
featured: | ||
authors: | ||
- Andrej Bauer | ||
source: | ||
--- | ||
|
||
<p>At <a href="https://types2023.webs.upv.es">TYPES 2023</a> I had the honor of giving an invited talk “On Isomorphism Invariance and Isomorphism Reflection in Type Theory” in which I discussed isomorphism reflection, which states that isomorphic types are judgementally equal. This strange principle is consistent, and it validates some fairly strange type-theoretic statements.</p> | ||
|
||
<p>Here are <a href="http://math.andrej.com/asset/data/TYPES2023-Isomoprhism-invariance-and-reflection.pdf">the slides with speaker notes</a>.</p> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
--- | ||
title: OCaml Weekly News, 25 Jul 2023 | ||
description: | ||
url: https://alan.petitepomme.net/cwn/2023.07.25.html | ||
date: 2023-07-25T12:00:00-00:00 | ||
preview_image: | ||
featured: | ||
authors: | ||
- Caml Weekly News | ||
source: | ||
--- | ||
|
||
<ol><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#1">Ppxlib dev meetings</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#2">Ocamls spotted in the wild</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#3">DkML 2.0.0 Preview Release</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#4">Next priority for OCaml?</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#5">Explorations on Package Management in Dune</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#6">OCamlFormat 0.26.0</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#7">Tarides Office Hours: Benchmark Tooling</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#8">You Can Attend the New OCaml.org Community Meetings</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#9">euler, an arithmetic library for native integers</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#10">DkML Install API 0.4.0</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#11">Liquidsoap 2.2.0 is out! 🎉</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#12">kcas and kcas_data 0.6.1: STM and compositional lock-dree data structures</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#13">ctypes 0.21.1, now with dune support</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#14">Announcing the ocaml-wasm organisation</a></li><li><a href="https://alan.petitepomme.net/cwn/2023.07.25.html#15">Feedback Needed: New "Arrays" Tutorial on OCaml.org</a></li></ol> |