DOCSEARCHbyAlgolia
Submit Docs

Cubical Agda Standard Library

repository·master·Indexed 20 days ago

https://github.com/agda/cubical

A standard library for Cubical Agda providing implementations for univalence and higher inductive types using a variation of cubical type theory. It includes algebraic tools such as the CommRingSolver for commutative rings and NatSolver for natural numbers, as well as comprehensive naming conventions for algebraic operations and structures.

Tokens
2.8K
Snippets
9
Records
15
Agent score
69%

What's inside agda-cubical

  2. Understand the theoretical background of Cubical Agda

    master

    Cubical Agda implements a variation of cubical type theory. Key theoretical references include:

    • Core Paper: "Cubical Agda: a dependently typed programming language with univalence and higher inductive types" by Andrea Vezzosi, Anders Mörtberg, and Andreas Abel.
    • Foundational Theory: Based on "Cubical Type Theory: a constructive interpretation of the univalence axiom" by Cohen, Coquand, Huber, and Mörtberg.
    • Implementation Detail: The Kan composition operations are decomposed into homogeneous composition and generalized transport, as described in "On Higher Inductive Types in Cubical Type Theory" by Coquand, Huber, and Mörtberg. This decomposition allows for the direct representation of higher inductive types.

  3. How the CommRingSolver works

    master

    The CommRingSolver is a tactic used to prove equalities of the form x = y in a commutative ring. The solver follows a three-step approach:

    1. Reflection: Converts x and y into Expressions (syntax trees) using reflection.
    2. Normalization: Maps these expressions to polynomials in Horner form.
    3. Unification: Uses Agda's built-in unification to compare the normalized results.

    For a practical demonstration of how to use the solver, refer to the Examples.agda file in the repository.

  5. Install and use the Cubical Agda library

    master

    The Cubical Agda library requires specific versions of Agda to function correctly. For detailed installation instructions, refer to the INSTALL.md file in the repository.

    If you are using a specific version of Agda, you should check out the corresponding tag of the cubical library. For example, if you are using Agda v2.6.2.2, you should use version v0.4 of the library.

    git checkout v0.4

  6. Register the cubical library for Agda development

    master

    To use the cubical library as a dependency in your own Agda projects, you must register it in your Agda configuration files.

    On Linux/Mac, update the following files:

    1. .agda/defaults: Add cubical to the list.
    2. .agda/libraries: Add the absolute path to the cubical.agda-lib file.
    # .agda/defaults
cubical

# .agda/libraries
/path/to/cubical.agda-lib

  7. Naming properties of algebraic operations

    master

    When naming a property of an operation in the Algebra folder, use the name of the operation first, followed by the property name. For example, use +Comm or ·Assoc.

    Common abbreviations for properties include:

    • Assoc: Associativity
    • Comm: Commutativity
    • Dist: Distributivity
    • Id: Unit laws (identity)
    • Inv: Inverse laws
    • Absorb: Absorption
    • Invol: Involution
    • Cancel: Cancellation
    • Annihil: Annihilation
    • Idem: Idempotency

    For laws with left and right versions, append the suffix L or R.

    ·Assoc : x · (y · z) ≡ (x · y) · z
·Comm : x · y ≡ y · x
·CommL : x · (y · z) ≡ y · (x · z)
·CommR : (x · y) · z ≡ (x · z) · y
·DistR+ : x · (y + z) ≡ (x · y) + (x · z)
·DistL+ : (x + y) · z ≡ (x · z) + (y · z)
·IdL : 1 · x ≡ x
-Id : (- 0) ≡ 0
+InvL : (- x) + x ≡ 0
∧AbsorbL∨ : x ∧ (x ∨ y) ≡ x
-Invol : - (- x) ≡ x
·CancelL : x · a ≡ x · b → a ≡ b
·AnnihilL : 0 · x ≡ 0
∧Idem : x ∧ x ≡ x

  8. Install Agda using cabal sandboxes

    master

    To prevent Agda from interfering with other Haskell packages, you can install it in a local sandbox.

    1. Clone the Agda repository and checkout a RELEASE tag.
    2. Initialize the sandbox using cabal sandbox init (or cabal v1-sandbox init if using cabal v2).
    3. Run make to build.
    4. Add the sandbox bin directory (agda/.cabal-sandbox/bin) to your $PATH.
    5. Verify with agda --version and run agda-mode setup for Emacs.
    git clone https://github.com/agda/agda
cd agda
git checkout RELEASE
cabal sandbox init
cabal update
make

# Add to ~/.bashrc or ~/.bash_profile
export PATH=/path/to/agda/.cabal-sandbox/bin:$PATH
source ~/.bashrc

agda --version
agda-mode setup

  9. Install Agda using stack

    master

    You can install Agda using stack by specifying a suitable GHC version via a stack-VERSION.yaml file.

    1. Clone the Agda repository and checkout a RELEASE tag.
    2. Run stack build --stack-yaml stack-VERSION.yaml.
    3. The executables will be located in agda/.stack-work/install/.../bin. Add this path to your $PATH.
    4. Alternatively, run stack install to copy agda and agda-mode to ~/.local/bin.
    5. Verify with agda --version and run agda-mode setup for Emacs.
    git clone https://github.com/agda/agda
cd agda
git checkout RELEASE
stack build --stack-yaml stack-VERSION.yaml

# Or to install to ~/.local/bin
stack install

# Add to PATH if using stack build
export PATH=/path/to/agda/.stack-work/install/.../.../.../bin:$PATH
source ~/.bashrc

agda --version
agda-mode setup

  10. Set up Agda with Cubical using Nix flakes

    master

    You can use Nix flakes to create an environment containing both Agda and the cubical library.

    1. Create a flake.nix using the provided template.
    2. Use nix shell to enter the environment.
    3. Test the installation by creating a test.agda file that imports Cubical.Foundations.Prelude and running Agda with the -l cubical flag.
    # flake.nix
{
  inputs.cubical = {
    url = "github:agda/cubical";
    inputs.nixpkgs.follows = "nixpkgs";
  };
  outputs = { self, nixpkgs, cubical }: 
  let 
    system = "x86_64-linux";
    cub-packages = cubical.packages.${system};
    cubical-lbry = cub-packages.cubical;
  in
  with import nixpkgs { system = system; };
  rec {
    packages.${system} = {
      cubical = cubical-lbry;
      agda = agda.withPackages [cubical-lbry];
    };
    defaultPackage.${system} = packages.${system}.agda;
  };
}
    -- test.agda
{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
    nix --extra-experimental-features "nix-command flakes" shell
agda -l cubical -i . test.agda

  11. Install Agda using cabal v2-build

    master

    To install the development version of Agda using cabal v2-build, you must have cabal-install version 2.4 or later. This method installs Agda into a mode where projects do not interfere with each other.

    1. Download and compile Agda:
      • Clone the Agda repository.
      • Checkout a specific RELEASE tag (e.g., v2.6.2.2).
      • Run cabal v2-install agda agda-mode.
    2. Update your $PATH to include ~/.cabal/bin.
    3. Verify the installation with agda --version.
    4. Set up Emacs support by running agda-mode setup.
    cabal v2-update
git clone https://github.com/agda/agda
cd agda
git checkout RELEASE
touch doc/user-manual.pdf
cabal v2-install agda agda-mode

# Add to ~/.bashrc or ~/.bash_profile
export PATH=$HOME/.cabal/bin:$PATH
source ~/.bashrc

agda --version
agda-mode setup

  12. Naming homomorphisms and algebraic structures

    master

    Follow these conventions for naming homomorphisms and structure instances:

    • Homomorphisms: To indicate that a homomorphism preserves a specific operation, use the prefix pres· where · is the operation.
    • Algebraic Structures: An instance of an algebraic structure should include the name of the structure (e.g., UnitGroup or ℤGroup).
    • Constructions: Use traditional algebraic names found in standard textbooks (e.g., use DirectSum instead of Coproduct).