Skip to content

Commit

Permalink
docs(README): Link to paper as published in ITP'23
Browse files Browse the repository at this point in the history
  • Loading branch information
phijor committed Jul 30, 2023
1 parent 862ac9a commit 709600e
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
# Final Coalgebras of Analytic Functors in Homotopy Type Theory
# Constructive Final Semantics of Finite Bags

![Type Checking](https://github.com/phijor/agda-cubical-multiset/actions/workflows/typecheck.yaml/badge.svg)
[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)
[![License: CC BY 4.0](https://img.shields.io/badge/License-CC_BY_4.0-lightgrey.svg)](https://creativecommons.org/licenses/by/4.0/)
[![DOI: 10.4230/LIPIcs.ITP.2023.20](https://img.shields.io/badge/DOI-10.4230%2FLIPIcs.ITP.2023.20-085DA6.svg?logo=DOI)](https://doi.org/10.4230/LIPIcs.ITP.2023.20)
[![Software Heritage Archive](https://archive.softwareheritage.org/badge/origin/https://github.com/phijor/agda-cubical-multiset/)](https://archive.softwareheritage.org/browse/origin/?origin_url=https://github.com/phijor/agda-cubical-multiset)


Expand All @@ -22,6 +23,9 @@ some constructions are intrinsically classical, in the sense that they are equiv
Nevertheless, a type satisfying the universal property of the final coalgebra can be constructed in HoTT employing the groupoid-based definition of finite bags.
We conclude by discussing generalizations of our constructions to the wider class of analytic functors.

The full paper is avaiable at [10.4230/LIPIcs.ITP.2023.20](https://doi.org/10.4230/LIPIcs.ITP.2023.20)
as part of [LIPIcs, Volume 268, ITP 2023](https://www.dagstuhl.de/dagpub/978-3-95977-284-6).

## Formalization in Agda

Claims in the paper have been formalized in a library that lives under `Multiset/`.
Expand Down

0 comments on commit 709600e

Please sign in to comment.