From b84936fcc0c2b274c3a31ef4dac559b096a2e874 Mon Sep 17 00:00:00 2001 From: lemastero Date: Sun, 29 Oct 2023 17:17:39 +0100 Subject: [PATCH 1/7] add nix flake with Agda 2.6.4 --- flake.nix | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 flake.nix diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..cac8940 --- /dev/null +++ b/flake.nix @@ -0,0 +1,21 @@ +{ + description = "hott-wiki2"; + + inputs = { + nixpkgs.url = "github:ncfavier/nixpkgs/agda-updates"; + utils.url = "github:numtide/flake-utils"; + }; + + outputs = { self, nixpkgs, utils, ... }: + utils.lib.eachDefaultSystem (system: + let + pkgs = nixpkgs.legacyPackages.${system}; + in rec { + devShells.default = pkgs.mkShell { + buildInputs = [ + (pkgs.agda.withPackages (ps: [ ps.standard-library ])) + ]; + }; + } + ); +} From 45455883186e4ca75ea8b6da048c52afa22e986a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Piotr=20Paradzi=C5=84ski?= Date: Wed, 4 Dec 2024 19:14:09 +0100 Subject: [PATCH 2/7] Update flake.nix --- flake.nix | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/flake.nix b/flake.nix index cac8940..f9a8c93 100644 --- a/flake.nix +++ b/flake.nix @@ -1,15 +1,14 @@ { - description = "hott-wiki2"; + description = "agda-hott"; inputs = { - nixpkgs.url = "github:ncfavier/nixpkgs/agda-updates"; + nixpkgs.url = "github:nixos/nixpkgs"; utils.url = "github:numtide/flake-utils"; }; outputs = { self, nixpkgs, utils, ... }: utils.lib.eachDefaultSystem (system: - let - pkgs = nixpkgs.legacyPackages.${system}; + let pkgs = nixpkgs.legacyPackages.${system}; in rec { devShells.default = pkgs.mkShell { buildInputs = [ From 1e4eba203a3a9a28781ff4112d0c47e5f026ed1f Mon Sep 17 00:00:00 2001 From: lemastero Date: Wed, 4 Dec 2024 19:40:24 +0100 Subject: [PATCH 3/7] fix compile error in MonoidObject --- src/FP/SimplifiedCategories/MonoidObject.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/FP/SimplifiedCategories/MonoidObject.agda b/src/FP/SimplifiedCategories/MonoidObject.agda index 38fbab6..77988a6 100755 --- a/src/FP/SimplifiedCategories/MonoidObject.agda +++ b/src/FP/SimplifiedCategories/MonoidObject.agda @@ -8,7 +8,7 @@ open import HoTT.Identity-Types using (refl; _≡_) open import FP.Types using (Function) open import TypeTheory.FunctionsProperties using (compose-id; id-compose; compose-compose; compose-assoc) open import FP.Abstractions.Bifunctor using (Bifunctor; BifunctorProduct; BifunctorEither; BifunctorThese) -open import FP.SimplifiedCategories.Category using (Category; CategoryFunction) +open import FP.SimplifiedCategories.Category using (Category) open import TypeTheory.Product using (_×_; ×assocLR; ×assocRL ; ×left-id; ×id-left; ×right-id; ×id-right; ×bimap) open import TypeTheory.Sum using (_+_; +right-id; +left-id; +id-right; +id-left From ff03a81c6d210f3d621ad04b7b39636189787f5d Mon Sep 17 00:00:00 2001 From: lemastero Date: Wed, 4 Dec 2024 19:51:00 +0100 Subject: [PATCH 4/7] test nix develop in CI --- .github/workflows/agda.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml index aa0ea13..b03a276 100644 --- a/.github/workflows/agda.yml +++ b/.github/workflows/agda.yml @@ -44,3 +44,6 @@ jobs: - run: agda Logic/Hurken-paradox.agda working-directory: src + + - uses: cachix/install-nix-action@v30 + - run: nix develop From 76d45cb105a681591dc11f58b6252d518ebc8f93 Mon Sep 17 00:00:00 2001 From: lemastero Date: Wed, 4 Dec 2024 19:51:15 +0100 Subject: [PATCH 5/7] Cleanup readme --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index d1a0613..6534c5b 100644 --- a/README.md +++ b/README.md @@ -16,10 +16,10 @@ Notes in Agda about * [Category Theory](https://ncatlab.org/nlab/show/category+theory) (based on * CS410 Advanced Functional Programming at the University of Strathclyde by Conor McBride ([videos](https://www.youtube.com/playlist?list=PLqggUNm8QSqmeTg5n37oxBif-PInUfTJ2)), ([GH repo with code](https://github.com/pigworker/CS410-17)), ([lecture notes](https://github.com/pigworker/CS410-15/blob/master/CS410-notes.pdf)), ([GH 2018](https://github.com/pigworker/CS410-18)), * [agda-categories](https://github.com/agda/agda-categories)) -* Patterns of Functional Programming (inspired by category theory that can be found in Haskell, Scala, PureScript, Idris) +* Functional Programming (abstractions from category theory used in Haskell, Scala, PureScript, Idris) -Patters of FP can be seen as continuation of [scala_typeclassopedia](https://github.com/lemastero/scala_typeclassopedia) - this time in Agda). +Abstractions in FP can be seen as continuation of [scala_typeclassopedia](https://github.com/lemastero/scala_typeclassopedia) - this time in Agda :) -Section zio-prelude aims at formally verifying encoding from Scala library [zio-prelude](https://zio.dev/zio-prelude/) (that improve usuall encoding of FP abstractions e.g. by adding Zivariant, introducing novel definitions like ZRerf that is a generalization of optics). +[src/FP/zio-prelude](src/FP/zio-prelude) aims at formally verifying encoding from Scala library [zio-prelude](https://zio.dev/zio-prelude/) (that improve usual encoding of FP abstractions e.g. by adding Zivariant, introducing novel definitions like ZRerf that is a generalization of optics). Category theory definitions are strict - use equality (agda-categories are parametrized by equivalence relation). From 34534734a6c2ea8f120f9a0854a65497096b9acf Mon Sep 17 00:00:00 2001 From: lemastero Date: Wed, 4 Dec 2024 19:57:13 +0100 Subject: [PATCH 6/7] Add info about creating nix develop --- README.md | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 6534c5b..ec3a85f 100644 --- a/README.md +++ b/README.md @@ -2,10 +2,6 @@ # Agda HoTT -Mature library for HoTT: https://unimath.github.io/agda-unimath/ - -Rest are my naive attempts, as I understand mathematics by writing code :) - Notes in Agda about * [Homotopy Type Theory](https://homotopytypetheory.org/book/) (based on * [Introduction to Univalent Foundations of Mathematics with Agda](https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/) by Martín Hötzel Escardó, ([arxiv 1911.00580](https://arxiv.org/abs/1911.00580)), @@ -23,3 +19,15 @@ Abstractions in FP can be seen as continuation of [scala_typeclassopedia](https: [src/FP/zio-prelude](src/FP/zio-prelude) aims at formally verifying encoding from Scala library [zio-prelude](https://zio.dev/zio-prelude/) (that improve usual encoding of FP abstractions e.g. by adding Zivariant, introducing novel definitions like ZRerf that is a generalization of optics). Category theory definitions are strict - use equality (agda-categories are parametrized by equivalence relation). + +## Getting Agda + +[Official install instructions](https://agda.readthedocs.io/en/latest/getting-started/installation.html) + +### for Nix + +If you are nix user you can get shell with recent Agda by running: + +```sh +nix develop +``` From 451d6b4ba3487f14e2c95dbe2e9330def4aafb7c Mon Sep 17 00:00:00 2001 From: lemastero Date: Wed, 4 Dec 2024 20:01:27 +0100 Subject: [PATCH 7/7] ignore nix and IntelliJ files --- .gitignore | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.gitignore b/.gitignore index 58ab67f..22e59c6 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,7 @@ *.agdai MAlonzo/** + +flake.lock + +.idea/ +*.iml