types-23
A formalisation of generalised containers in Cubical Agda
Science Score: 54.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
✓CITATION.cff file
Found CITATION.cff file -
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
○DOI references
-
✓Academic publication links
Links to: sciencedirect.com -
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (4.4%) to scientific vocabulary
Last synced: 9 months ago
·
JSON representation
·
Repository
A formalisation of generalised containers in Cubical Agda
Basic Info
- Host: GitHub
- Owner: stefaniatadama
- Language: Agda
- Default Branch: main
- Size: 46.9 KB
Statistics
- Stars: 3
- Watchers: 1
- Forks: 0
- Open Issues: 0
- Releases: 0
Created over 3 years ago
· Last pushed over 2 years ago
Metadata Files
Readme
Citation
README.md
Revisiting Containers in Cubical Agda
Supplementary artefacts for TYPES 2023. Typechecked using Agda 2.6.3 and Cubical v0.5. Written by Stefania Damato & Thorsten Altenkirch.
- Containers.agda: Definition of generalised containers, the category $\underline{\mathbf{Cont}}$ of generalised containers, and the container extension functor ⟦_⟧ mapping generalised containers to functors.
- ContainersProofs.agda: Two proofs of the central result that the container extension functor ⟦_⟧ is full and faithful. One follows the proof given in Containers: Constructing strictly positive types, and the other is a new presentation of the previous proof that makes explicit the use of the Yoneda lemma. We have proved this result for the case of generalised containers, which are parameterised by an arbitrary category $\underline{\mathbf{C}}$ and give rise to functors of type $\underline{\mathbf{C}} \to \underline{\mathbf{Set}}$.
- InductiveContainers.agda: (WIP) Formalisation of the proofs that ordinary container functors are closed under fixed points, i.e. container functors are closed under initial algebras and terminal coalgebras. Proofs taken from Containers: Constructing strictly positive types.
- IndexedGeneralised.agda: Proof that indexed containers are a special case of generalised containers.
An HTML rendering of this code can be found here.
Owner
- Name: Stefania Damato
- Login: stefaniatadama
- Kind: user
- Company: University of Nottingham
- Website: stefaniatadama.com
- Repositories: 5
- Profile: https://github.com/stefaniatadama
PhD student
Citation (citation.cff)
cff-version: 1.2.0
message: "If you use this software, please cite it as below."
authors:
- family-names: Damato
given-names: Stefania
title: "A formalisation of generalised containers in Cubical Agda"
version: 0.1
date-released: 2023-06-23