---
tags: seminar, maths, blute, ottawa, Coalgebras over Lawvere metric spaces
---
# Coalgebras over Lawvere Metric Spaces
Talk at the [Logic Seminar](https://richardblute.ca/logic-seminar-page/) of the University of Ottawa organised by [Richard Blute](http://aix1.uottawa.ca/~rblute/), Feb 2022.
**Abstract:** Coalgebras are a model of dynamic systems that is particularly relevant if generalisations of bisimulation (observational/behavioural equivalence/preorder/metric) are of importance. We survey coalgebras as models of dynamical systems, Lawvere metric spaces, coalgebras over Lawvere metric spaces, hint their motivations in applications to computer science and introduce some of the open mathematical questions in the area.
---
(... draft ...)
---
## Table of Contents
(the writeup contains much more material than the 50min presentation)
- background:
- [coalgebras over sets](https://hackmd.io/@alexhkurz/BJ5ysx-0t)
- [coalgebraic logic over sets](https://hackmd.io/@alexhkurz/rJLXsx-0F)
- [generalizing to ordered sets](https://hackmd.io/@alexhkurz/ryji9lZRY)
- [generalizing from orders to quantales](https://hackmd.io/@alexhkurz/HJlBneW0Y)
- [extending functors to quantale enriched categories](https://hackmd.io/@alexhkurz/r1PK6gW0F)
- the logic of quantale enriched categories
## References
Bill Lawvere: Metric Spaces, Generalized Logic, and Closed Categories, 1973.
[The collected works of F. W. Lawvere](https://github.com/mattearnshaw/lawvere).
G.M. Kelly: Basic Concepts of Enriched Category Theory, Cambridge University Press, Lecture Notes in Mathematics 64, 1982. Also in [TAC Reprints 10, 2005](http://www.tac.mta.ca/tac/reprints/articles/10/tr10abs.html).
Peter Aczel: [Non-well-founded sets](http://www.irafs.org/courses/materials/aczel_set_theory.pdf). CSLI 1988.
Jan J. M. M. Rutten: Relators and Metric Bisimulations. CMCS 1998.
Peter Aczel, Nax Paul Mendler: A Final Coalgebra Theorem. Category Theory and Computer Science 1989
James Worrell: Coinduction for recursive data types: partial orders, metric spaces and Omega-categories. CMCS 2000
Jipsen and Galatos: [RESIDUATED LATTICES OF SIZE UP TO 6](https://math.chapman.edu/~jipsen/finitestructures/rlattices/RLlist3.pdf), 2017
Adriana Balan, Alexander Kurz, Jiri Velebil: [Extending set functors to generalised metric spaces](https://lmcs.episciences.org/5132/pdf), Logical Methods in Computer Science 15 (2019).
...
## Topics that didn't make it into the talk ...
Jan Rutten's theory of [universal coalgebra](https://www.sciencedirect.com/science/article/pii/S0304397500000566?via%3Dihub) that develops the theory of coalgebras parametrically in the functor $T:Set\to Set$
Moss's coalgebraic logic and Pattinson's predicate liftings (dblp for [coalgebraic logic](https://dblp.uni-trier.de/search?q=%20coalgebraic%20logic))
Examples of coalgebras for functors $T:Set\to Set$ other than the powerset functor such as [streams](https://dblp.uni-trier.de/search/publ?q=author:Jan_Rutten:%20stream*), [automata](https://dblp.uni-trier.de/search/publ?q=author:Yde_Venema:%20automat*), languages, Markov chains, certain kind of games, etc
Examples of base categories $\mathcal X$ other than $Set$ or $Pre$ or or $Pos$ or $\Omega$-cat such as various topological spaces, [nominal sets](https://dblp.uni-trier.de/search/publ?q=author:Daniela_Petrisan:%20nominal*), vector spaces, etc
Applications of coalgebras to the semantics of programming languages such as operational semantics of process algebras via [bialgebras](https://dblp.uni-trier.de/search/publ?q=bialgebra*), infinitary lambda-calculus, ...
Applications of coalgebras over Lawvere metric spaces to semantics of programming languages ... [Breugel and Worrell etal](https://dblp.org/search/publ?q=author:James_Worrell_0001:%20author:Franck_van_Breugel:) ... [Dal Lago and Gavazzo etal](https://dblp.org/search/publ?q=author:Ugo_Dal_Lago:%20author:Francesco_Gavazzo:)
...
(the coalgebra community has been prolific, there is so much more out there that I regret now that I started to make a list ... apologies to everybody else)

Smart Contracts Orange County ACM Chapter, Sep 21, 2022 Alexander Kurz Chapman University view online at http://tiny.cc/qibzuz (layout optimized for Brave browser)

3/17/2023Examples of natural deduction proofs that use proof by contradiction aka reductio ad absurdum (RAA). [^RAA] [^or-elim] [^RAA]: The following are not "proper" RAA, but just negation-introduction (ie the proof of a negated statement): > $\neg B$ > ... (here we use some other assumptions we made) > $B$ (now we have a contradiction between $\neg B$ and $B$) $\neg\neg B$ (and we conclude $\neg\neg B$)

3/10/2023Distributed Hash Tables <br> Key Based Routing Selected slides from the talk Building decentralized systems using DHTs (Part 1) by Peter Druschel May 2012 (layout optimized for Brave browser)

2/23/2023$\newcommand{\sem}[1]{[![#1]!]}$ [4] refers to [3] refers to See also the more recent References Anders Kock homepage

2/11/2023
Published on ** HackMD**