New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add references to Fiore's paper #32

Merged

eyihluyc merged 1 commit into soas from soas-docs

May 21, 2024

Collaborator

Anatolay commented May 20, 2024 •

edited by pr-codex bot

Loading

PR-Codex overview

This PR introduces formal metatheory of second-order abstract syntax in Lean.

Detailed summary

Added definitions for context, families, and mappings
Implemented context extension, map, rename, copair
Introduced box-coalgebras, weakening, contraction
Defined monoids with internal hom
Included substitution operations and semantic substitution lemma

✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}


          Add references to Fiore's paper

b49ee0d

eyihluyc merged commit 5d14d6f into soas

2 checks passed

eyihluyc deleted the soas-docs branch

May 21, 2024 00:23

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet