generated-deloopings
Science Score: 44.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
-
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (3.4%) to scientific vocabulary
Last synced: 6 months ago
·
JSON representation
·
Repository
Basic Info
- Host: GitHub
- Owner: camilchp
- Language: Agda
- Default Branch: main
- Size: 104 KB
Statistics
- Stars: 0
- Watchers: 2
- Forks: 1
- Open Issues: 0
- Releases: 0
Created over 2 years ago
· Last pushed about 2 years ago
Metadata Files
Readme
Citation
README.md
Delooping generated groups in homotopy type theory
This repository presents the developments accompanying the paper Delooping generated groups in homotopy type theory by Camil Champin, Samuel Mimram and Emile Oleon. They have been tested with Agda 2.6.3 with the cubical Agda libraray version 0.5.
A brief table of contents:
- GSet
- Definition of Actions
- Definition of GSets and the GSet Structure
- GSetHom
- Definition of GSet Homomorphisms
- Definition of GSetEquiv : GSet Isomorphisms
- GSetProperties
- Equality types for Actions and GSetHoms
- Properties of GSetEquivs
- Isomorphisms and paths are equivalent (through fundamental theorem of identity types)
- Gsets form a groupoid
- XSet
- Definition of Set Actions
- Definition of XSets and the XSet Structure
- XSetProperties
- The forgetful functor U from GSets to XSets when X is a subset of G
- Proof that the the loop space of the principal torsor is invariant by U.
- Comp
- Definition of Comp the connected component of a pointed space (A, a0)
- Definition of the fundamental group π₁ for groupoids
- The Comp of a groupoid is a groupoid
- π₁(Comp(A, a0)) = π₁(A,a0)
- Generators
- Definition of Group generation
- PrincipalTorsor
- Definition of the principal torsor of a group
- Deloopings
- Delooping by torsors (classical construction and proof)
- Delooping by generated torsors
- Caracterisation of the Principal torsor's Aut group
Owner
- Name: Camil Champin
- Login: camilchp
- Kind: user
- Location: Lyon, France
- Company: ENS Lyon
- Repositories: 1
- Profile: https://github.com/camilchp
Citation (CITATION.cff)
cff-version: 1.2.0 message: "If you use this software, please cite it as below." authors: - family-names: "Champin" given-names: "Camil" - family-names: "Mimram" given-names: "Samuel" title: "Delooping generated groups" url: "https://github.com/camilchp/generated-deloopings"