diff --git a/Makefile b/Makefile
index db28a1e8ae..e2ed2f507d 100644
--- a/Makefile
+++ b/Makefile
@@ -62,7 +62,7 @@ src/everything.lagda.md: agdaFiles
| cut -c 5- \
| cut -f1 -d'.' \
| sed 's/\//\./g' \
- | awk 'BEGIN { FS = "."; OFS = "."; lastdir = "" } { if ($$1 != lastdir) { print ""; lastdir = $$1 } print "open import " $$0 }' \
+ | awk 'BEGIN { FS = "."; OFS = "."; lastdir = "" } { if ($$1 != lastdir) { print ""; lastdir = $$1 } print "open import " $$0 " public"}' \
>> $@ ;\
echo "\`\`\`" >> $@ ;
diff --git a/src/finite-algebra.lagda.md b/src/finite-algebra.lagda.md
index 27ed892454..359239c09d 100644
--- a/src/finite-algebra.lagda.md
+++ b/src/finite-algebra.lagda.md
@@ -8,13 +8,8 @@ module finite-algebra where
open import finite-algebra.commutative-finite-rings public
open import finite-algebra.dependent-products-commutative-finite-rings public
open import finite-algebra.dependent-products-finite-rings public
-open import finite-algebra.finite-abelian-groups public
-open import finite-algebra.finite-commutative-monoids public
open import finite-algebra.finite-fields public
-open import finite-algebra.finite-groups public
-open import finite-algebra.finite-monoids public
open import finite-algebra.finite-rings public
-open import finite-algebra.finite-semigroups public
open import finite-algebra.homomorphisms-commutative-finite-rings public
open import finite-algebra.homomorphisms-finite-rings public
open import finite-algebra.products-commutative-finite-rings public
diff --git a/src/finite-algebra/commutative-finite-rings.lagda.md b/src/finite-algebra/commutative-finite-rings.lagda.md
index dbb33bd468..52394614ad 100644
--- a/src/finite-algebra/commutative-finite-rings.lagda.md
+++ b/src/finite-algebra/commutative-finite-rings.lagda.md
@@ -591,7 +591,7 @@ module _
preserves-concat-add-list-Ring-π½ finite-ring-Commutative-Ring-π½
```
-### Equip a finite type with a structure of commutative finite ring
+### Equipping a finite type with the structure of a commutative finite ring
```agda
module _
@@ -603,14 +603,14 @@ module _
UU l1
structure-commutative-ring-π½ =
Ξ£ ( structure-ring-π½ X)
- ( Ξ» r β is-commutative-Ring-π½ (compute-structure-ring-π½ X r))
+ ( Ξ» r β is-commutative-Ring-π½ (finite-ring-structure-ring-π½ X r))
- compute-structure-commutative-ring-π½ :
+ finite-commutative-ring-structure-commutative-ring-π½ :
structure-commutative-ring-π½ β
Commutative-Ring-π½ l1
- pr1 (compute-structure-commutative-ring-π½ (r , c)) =
- compute-structure-ring-π½ X r
- pr2 (compute-structure-commutative-ring-π½ (r , c)) = c
+ pr1 (finite-commutative-ring-structure-commutative-ring-π½ (r , c)) =
+ finite-ring-structure-ring-π½ X r
+ pr2 (finite-commutative-ring-structure-commutative-ring-π½ (r , c)) = c
is-finite-structure-commutative-ring-π½ :
is-finite structure-commutative-ring-π½
diff --git a/src/finite-algebra/dependent-products-finite-rings.lagda.md b/src/finite-algebra/dependent-products-finite-rings.lagda.md
index 18b15b2f33..bcf62b5a1c 100644
--- a/src/finite-algebra/dependent-products-finite-rings.lagda.md
+++ b/src/finite-algebra/dependent-products-finite-rings.lagda.md
@@ -156,5 +156,5 @@ module _
ring-Ξ -Ring-π½ = Ξ -Ring (type-π½ I) (ring-Ring-π½ β A)
Ξ -Ring-π½ : Ring-π½ (l1 β l2)
- Ξ -Ring-π½ = compute-ring-π½ ring-Ξ -Ring-π½ is-finite-type-Ξ -Ring-π½
+ Ξ -Ring-π½ = finite-ring-is-finite-Ring ring-Ξ -Ring-π½ is-finite-type-Ξ -Ring-π½
```
diff --git a/src/finite-algebra/finite-groups.lagda.md b/src/finite-algebra/finite-groups.lagda.md
deleted file mode 100644
index 6e5c9cda1d..0000000000
--- a/src/finite-algebra/finite-groups.lagda.md
+++ /dev/null
@@ -1,217 +0,0 @@
-# Abstract finite groups
-
-```agda
-module finite-algebra.finite-groups where
-```
-
-Imports
-
-```agda
-open import finite-algebra.finite-monoids
-open import finite-algebra.finite-semigroups
-
-open import foundation.identity-types
-open import foundation.propositions
-open import foundation.sets
-open import foundation.universe-levels
-
-open import group-theory.commuting-elements-groups
-open import group-theory.groups
-open import group-theory.monoids
-open import group-theory.semigroups
-
-open import structured-types.pointed-types
-
-open import univalent-combinatorics.cartesian-product-types
-open import univalent-combinatorics.dependent-function-types
-open import univalent-combinatorics.dependent-pair-types
-open import univalent-combinatorics.equality-finite-types
-open import univalent-combinatorics.finite-types
-```
-
-
-
-## Idea
-
-An **abstract finite group** is a finite group in the usual algebraic sense,
-i.e., it consists of a finite type equipped with a unit element `e`, a binary
-operation `x, y β¦ xy`, and an inverse operation `x β¦ xβ»ΒΉ` satisfying the group
-laws
-
-```text
- (xy)z = x(yz) (associativity)
- ex = x (left unit law)
- xe = x (right unit law)
- xβ»ΒΉx = e (left inverse law)
- xxβ»ΒΉ = e (right inverse law)
-```
-
-## Definition
-
-### The condition that a finite semigroup is a finite group
-
-```agda
-is-group-π½ :
- {l : Level} (G : Semigroup-π½ l) β UU l
-is-group-π½ G = is-group (semigroup-Semigroup-π½ G)
-```
-
-### The type of groups
-
-```agda
-Group-π½ :
- (l : Level) β UU (lsuc l)
-Group-π½ l = Ξ£ (Semigroup-π½ l) is-group-π½
-
-compute-group-π½ :
- {l : Level} β (G : Group l) β is-finite (type-Group G) β Group-π½ l
-pr1 (compute-group-π½ G f) = compute-semigroup-π½ (semigroup-Group G) f
-pr2 (compute-group-π½ G f) = is-group-Group G
-
-module _
- {l : Level} (G : Group-π½ l)
- where
-
- finite-semigroup-Group-π½ : Semigroup-π½ l
- finite-semigroup-Group-π½ = pr1 G
-
- semigroup-Group-π½ : Semigroup l
- semigroup-Group-π½ = semigroup-Semigroup-π½ finite-semigroup-Group-π½
-
- is-group-Group-π½ : is-group-π½ finite-semigroup-Group-π½
- is-group-Group-π½ = pr2 G
-
- group-Group-π½ : Group l
- pr1 group-Group-π½ = semigroup-Group-π½
- pr2 group-Group-π½ = is-group-Group-π½
-
- finite-type-Group-π½ : π½ l
- finite-type-Group-π½ = finite-type-Semigroup-π½ finite-semigroup-Group-π½
-
- type-Group-π½ : UU l
- type-Group-π½ = type-Semigroup semigroup-Group-π½
-
- is-finite-type-Group-π½ : is-finite type-Group-π½
- is-finite-type-Group-π½ = is-finite-type-Semigroup-π½ finite-semigroup-Group-π½
-
- set-Group-π½ : Set l
- set-Group-π½ = set-Group group-Group-π½
-
- is-set-type-Group-π½ : is-set type-Group-π½
- is-set-type-Group-π½ = is-set-type-Group group-Group-π½
-
- has-associative-mul-Group-π½ : has-associative-mul type-Group-π½
- has-associative-mul-Group-π½ = has-associative-mul-Group group-Group-π½
-
- mul-Group-π½ : type-Group-π½ β type-Group-π½ β type-Group-π½
- mul-Group-π½ = mul-Group group-Group-π½
-
- ap-mul-Group-π½ :
- {x x' y y' : type-Group-π½} (p : Id x x') (q : Id y y') β
- Id (mul-Group-π½ x y) (mul-Group-π½ x' y')
- ap-mul-Group-π½ = ap-mul-Group group-Group-π½
-
- mul-Group-π½' : type-Group-π½ β type-Group-π½ β type-Group-π½
- mul-Group-π½' = mul-Group' group-Group-π½
-
- commute-Group-π½ : type-Group-π½ β type-Group-π½ β UU l
- commute-Group-π½ = commute-Group group-Group-π½
-
- associative-mul-Group-π½ :
- (x y z : type-Group-π½) β
- Id (mul-Group-π½ (mul-Group-π½ x y) z) (mul-Group-π½ x (mul-Group-π½ y z))
- associative-mul-Group-π½ = associative-mul-Group group-Group-π½
-
- is-unital-Group-π½ : is-unital-Semigroup semigroup-Group-π½
- is-unital-Group-π½ = is-unital-Group group-Group-π½
-
- monoid-Group-π½ : Monoid l
- monoid-Group-π½ = monoid-Group group-Group-π½
-
- finite-monoid-Group-π½ : Monoid-π½ l
- pr1 finite-monoid-Group-π½ = finite-semigroup-Group-π½
- pr2 finite-monoid-Group-π½ = is-unital-Group-π½
-
- unit-Group-π½ : type-Group-π½
- unit-Group-π½ = unit-Group group-Group-π½
-
- is-unit-Group-π½ : type-Group-π½ β UU l
- is-unit-Group-π½ = is-unit-Group group-Group-π½
-
- is-prop-is-unit-Group-π½ : (x : type-Group-π½) β is-prop (is-unit-Group-π½ x)
- is-prop-is-unit-Group-π½ = is-prop-is-unit-Group group-Group-π½
-
- is-unit-prop-Group-π½ : type-Group-π½ β Prop l
- is-unit-prop-Group-π½ = is-unit-prop-Group group-Group-π½
-
- left-unit-law-mul-Group-π½ :
- (x : type-Group-π½) β Id (mul-Group-π½ unit-Group-π½ x) x
- left-unit-law-mul-Group-π½ = left-unit-law-mul-Group group-Group-π½
-
- right-unit-law-mul-Group-π½ :
- (x : type-Group-π½) β Id (mul-Group-π½ x unit-Group-π½) x
- right-unit-law-mul-Group-π½ = right-unit-law-mul-Group group-Group-π½
-
- pointed-type-Group-π½ : Pointed-Type l
- pointed-type-Group-π½ = pointed-type-Group group-Group-π½
-
- has-inverses-Group-π½ : is-group' semigroup-Group-π½ is-unital-Group-π½
- has-inverses-Group-π½ = has-inverses-Group group-Group-π½
-
- inv-Group-π½ : type-Group-π½ β type-Group-π½
- inv-Group-π½ = inv-Group group-Group-π½
-
- left-inverse-law-mul-Group-π½ :
- (x : type-Group-π½) β Id (mul-Group-π½ (inv-Group-π½ x) x) unit-Group-π½
- left-inverse-law-mul-Group-π½ = left-inverse-law-mul-Group group-Group-π½
-
- right-inverse-law-mul-Group-π½ :
- (x : type-Group-π½) β Id (mul-Group-π½ x (inv-Group-π½ x)) unit-Group-π½
- right-inverse-law-mul-Group-π½ = right-inverse-law-mul-Group group-Group-π½
-
- inv-unit-Group-π½ :
- Id (inv-Group-π½ unit-Group-π½) unit-Group-π½
- inv-unit-Group-π½ = inv-unit-Group group-Group-π½
-```
-
-## Properties
-
-### There is a finite number of ways to equip a finite type with a structure of group
-
-```agda
-module _
- {l : Level}
- (X : π½ l)
- where
-
- structure-group-π½ : UU l
- structure-group-π½ =
- Ξ£ (structure-semigroup-π½ X) (Ξ» s β is-group-π½ (X , s))
-
- compute-structure-group-π½ :
- structure-group-π½ β Group-π½ l
- pr1 (compute-structure-group-π½ (s , g)) = (X , s)
- pr2 (compute-structure-group-π½ (s , g)) = g
-
- is-finite-structure-group-π½ :
- is-finite (structure-group-π½)
- is-finite-structure-group-π½ =
- is-finite-Ξ£
- ( is-finite-structure-semigroup-π½ X)
- ( Ξ» s β
- is-finite-Ξ£
- ( is-finite-is-unital-Semigroup-π½ (X , s))
- ( Ξ» u β
- is-finite-Ξ£
- ( is-finite-Ξ
- ( is-finite-type-π½ X)
- ( Ξ» _ β is-finite-type-π½ X))
- ( Ξ» i β
- is-finite-product
- ( is-finite-Ξ
- ( is-finite-type-π½ X)
- ( Ξ» x β is-finite-eq-π½ X))
- ( is-finite-Ξ
- ( is-finite-type-π½ X)
- ( Ξ» x β is-finite-eq-π½ X)))))
-```
diff --git a/src/finite-algebra/finite-monoids.lagda.md b/src/finite-algebra/finite-monoids.lagda.md
deleted file mode 100644
index 4cd881562d..0000000000
--- a/src/finite-algebra/finite-monoids.lagda.md
+++ /dev/null
@@ -1,158 +0,0 @@
-# Finite monoids
-
-```agda
-module finite-algebra.finite-monoids where
-```
-
-Imports
-
-```agda
-open import finite-algebra.finite-semigroups
-
-open import foundation.identity-types
-open import foundation.propositions
-open import foundation.sets
-open import foundation.unital-binary-operations
-open import foundation.universe-levels
-
-open import group-theory.monoids
-open import group-theory.semigroups
-
-open import univalent-combinatorics.cartesian-product-types
-open import univalent-combinatorics.dependent-function-types
-open import univalent-combinatorics.dependent-pair-types
-open import univalent-combinatorics.equality-finite-types
-open import univalent-combinatorics.finite-types
-```
-
-
-
-## Idea
-
-Finite monoids are unital finite semigroups
-
-## Definition
-
-```agda
-is-unital-Semigroup-π½ :
- {l : Level} β Semigroup-π½ l β UU l
-is-unital-Semigroup-π½ G = is-unital (mul-Semigroup-π½ G)
-
-Monoid-π½ :
- (l : Level) β UU (lsuc l)
-Monoid-π½ l = Ξ£ (Semigroup-π½ l) is-unital-Semigroup-π½
-
-module _
- {l : Level} (M : Monoid-π½ l)
- where
-
- finite-semigroup-Monoid-π½ : Semigroup-π½ l
- finite-semigroup-Monoid-π½ = pr1 M
-
- semigroup-Monoid-π½ : Semigroup l
- semigroup-Monoid-π½ = semigroup-Semigroup-π½ finite-semigroup-Monoid-π½
-
- finite-type-Monoid-π½ : π½ l
- finite-type-Monoid-π½ = finite-type-Semigroup-π½ finite-semigroup-Monoid-π½
-
- type-Monoid-π½ : UU l
- type-Monoid-π½ = type-Semigroup-π½ finite-semigroup-Monoid-π½
-
- is-finite-type-Monoid-π½ : is-finite type-Monoid-π½
- is-finite-type-Monoid-π½ = is-finite-type-Semigroup-π½ finite-semigroup-Monoid-π½
-
- set-Monoid-π½ : Set l
- set-Monoid-π½ = set-Semigroup semigroup-Monoid-π½
-
- is-set-type-Monoid-π½ : is-set type-Monoid-π½
- is-set-type-Monoid-π½ = is-set-type-Semigroup semigroup-Monoid-π½
-
- mul-Monoid-π½ : type-Monoid-π½ β type-Monoid-π½ β type-Monoid-π½
- mul-Monoid-π½ = mul-Semigroup semigroup-Monoid-π½
-
- mul-Monoid-π½' : type-Monoid-π½ β type-Monoid-π½ β type-Monoid-π½
- mul-Monoid-π½' y x = mul-Monoid-π½ x y
-
- ap-mul-Monoid-π½ :
- {x x' y y' : type-Monoid-π½} β
- x οΌ x' β y οΌ y' β mul-Monoid-π½ x y οΌ mul-Monoid-π½ x' y'
- ap-mul-Monoid-π½ = ap-mul-Semigroup semigroup-Monoid-π½
-
- associative-mul-Monoid-π½ :
- (x y z : type-Monoid-π½) β
- mul-Monoid-π½ (mul-Monoid-π½ x y) z οΌ mul-Monoid-π½ x (mul-Monoid-π½ y z)
- associative-mul-Monoid-π½ = associative-mul-Semigroup semigroup-Monoid-π½
-
- has-unit-Monoid-π½ : is-unital mul-Monoid-π½
- has-unit-Monoid-π½ = pr2 M
-
- monoid-Monoid-π½ : Monoid l
- pr1 monoid-Monoid-π½ = semigroup-Monoid-π½
- pr2 monoid-Monoid-π½ = has-unit-Monoid-π½
-
- unit-Monoid-π½ : type-Monoid-π½
- unit-Monoid-π½ = unit-Monoid monoid-Monoid-π½
-
- left-unit-law-mul-Monoid-π½ :
- (x : type-Monoid-π½) β mul-Monoid-π½ unit-Monoid-π½ x οΌ x
- left-unit-law-mul-Monoid-π½ = left-unit-law-mul-Monoid monoid-Monoid-π½
-
- right-unit-law-mul-Monoid-π½ :
- (x : type-Monoid-π½) β mul-Monoid-π½ x unit-Monoid-π½ οΌ x
- right-unit-law-mul-Monoid-π½ = right-unit-law-mul-Monoid monoid-Monoid-π½
-```
-
-## Properties
-
-### For any finite semigroup `G`, being unital is a property
-
-```agda
-abstract
- is-prop-is-unital-Semigroup-π½ :
- {l : Level} (G : Semigroup-π½ l) β is-prop (is-unital-Semigroup-π½ G)
- is-prop-is-unital-Semigroup-π½ G =
- is-prop-is-unital-Semigroup (semigroup-Semigroup-π½ G)
-
-is-unital-Semigroup-π½-Prop : {l : Level} (G : Semigroup-π½ l) β Prop l
-pr1 (is-unital-Semigroup-π½-Prop G) = is-unital-Semigroup-π½ G
-pr2 (is-unital-Semigroup-π½-Prop G) = is-prop-is-unital-Semigroup-π½ G
-```
-
-### For any finite semigroup `G`, being unital is finite
-
-```agda
-is-finite-is-unital-Semigroup-π½ :
- {l : Level} (G : Semigroup-π½ l) β is-finite (is-unital-Semigroup-π½ G)
-is-finite-is-unital-Semigroup-π½ G =
- is-finite-Ξ£
- ( is-finite-type-Semigroup-π½ G)
- ( Ξ» e β
- is-finite-product
- ( is-finite-Ξ
- ( is-finite-type-Semigroup-π½ G)
- ( Ξ» x β is-finite-eq-π½ (finite-type-Semigroup-π½ G)))
- ( is-finite-Ξ
- ( is-finite-type-Semigroup-π½ G)
- ( Ξ» x β is-finite-eq-π½ (finite-type-Semigroup-π½ G))))
-```
-
-### There is a finite number of ways to equip a finite type with a structure of semigroup
-
-```agda
-structure-monoid-π½ :
- {l1 : Level} β π½ l1 β UU l1
-structure-monoid-π½ X =
- Ξ£ (structure-semigroup-π½ X) (Ξ» p β is-unital-Semigroup-π½ (X , p))
-
-compute-structure-monoid-π½ :
- {l : Level} β (X : π½ l) β structure-monoid-π½ X β Monoid-π½ l
-pr1 (compute-structure-monoid-π½ X (a , u)) = X , a
-pr2 (compute-structure-monoid-π½ X (a , u)) = u
-
-is-finite-structure-monoid-π½ :
- {l : Level} β (X : π½ l) β is-finite (structure-monoid-π½ X)
-is-finite-structure-monoid-π½ X =
- is-finite-Ξ£
- ( is-finite-structure-semigroup-π½ X)
- ( Ξ» m β is-finite-is-unital-Semigroup-π½ (X , m))
-```
diff --git a/src/finite-algebra/finite-rings.lagda.md b/src/finite-algebra/finite-rings.lagda.md
index e420bd09d9..0f4df958a6 100644
--- a/src/finite-algebra/finite-rings.lagda.md
+++ b/src/finite-algebra/finite-rings.lagda.md
@@ -10,9 +10,9 @@ module finite-algebra.finite-rings where
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers
-open import finite-algebra.finite-abelian-groups
-open import finite-algebra.finite-groups
-open import finite-algebra.finite-monoids
+open import finite-group-theory.finite-abelian-groups
+open import finite-group-theory.finite-groups
+open import finite-group-theory.finite-monoids
open import foundation.binary-embeddings
open import foundation.binary-equivalences
@@ -62,10 +62,11 @@ has-mul-Ab-π½ A = has-mul-Ab (ab-Ab-π½ A)
Ring-π½ : (l1 : Level) β UU (lsuc l1)
Ring-π½ l1 = Ξ£ (Ab-π½ l1) (Ξ» A β has-mul-Ab-π½ A)
-compute-ring-π½ :
+finite-ring-is-finite-Ring :
{l : Level} β (R : Ring l) β is-finite (type-Ring R) β Ring-π½ l
-pr1 (compute-ring-π½ R f) = compute-abelian-group-π½ (ab-Ring R) f
-pr2 (compute-ring-π½ R f) = pr2 R
+pr1 (finite-ring-is-finite-Ring R f) =
+ finite-abelian-group-is-finite-Ab (ab-Ring R) f
+pr2 (finite-ring-is-finite-Ring R f) = pr2 R
module _
{l : Level} (R : Ring-π½ l)
@@ -500,7 +501,7 @@ module _
## Properties
-### There is a finite number of ways to equip a finite type with a structure of ring
+### There is a finite number of ways to equip a finite type with the structure of a ring
```agda
module _
@@ -511,13 +512,13 @@ module _
structure-ring-π½ : UU l
structure-ring-π½ =
Ξ£ ( structure-abelian-group-π½ X)
- ( Ξ» m β has-mul-Ab-π½ (compute-structure-abelian-group-π½ X m))
+ ( Ξ» m β has-mul-Ab-π½ (finite-abelian-group-structure-abelian-group-π½ X m))
- compute-structure-ring-π½ :
+ finite-ring-structure-ring-π½ :
structure-ring-π½ β Ring-π½ l
- pr1 (compute-structure-ring-π½ (m , c)) =
- compute-structure-abelian-group-π½ X m
- pr2 (compute-structure-ring-π½ (m , c)) = c
+ pr1 (finite-ring-structure-ring-π½ (m , c)) =
+ finite-abelian-group-structure-abelian-group-π½ X m
+ pr2 (finite-ring-structure-ring-π½ (m , c)) = c
is-finite-structure-ring-π½ :
is-finite structure-ring-π½
diff --git a/src/finite-algebra/finite-semigroups.lagda.md b/src/finite-algebra/finite-semigroups.lagda.md
deleted file mode 100644
index 83cf5f5e47..0000000000
--- a/src/finite-algebra/finite-semigroups.lagda.md
+++ /dev/null
@@ -1,126 +0,0 @@
-# Finite semigroups
-
-```agda
-module finite-algebra.finite-semigroups where
-```
-
-Imports
-
-```agda
-open import foundation.decidable-propositions
-open import foundation.identity-types
-open import foundation.sets
-open import foundation.universe-levels
-
-open import group-theory.semigroups
-
-open import univalent-combinatorics.dependent-function-types
-open import univalent-combinatorics.dependent-pair-types
-open import univalent-combinatorics.equality-finite-types
-open import univalent-combinatorics.finite-types
-```
-
-
-
-## Idea
-
-Finite semigroups are finite sets equipped with an associative binary operation.
-
-## Definition
-
-```agda
-has-associative-mul-π½ : {l : Level} (X : π½ l) β UU l
-has-associative-mul-π½ X = has-associative-mul (type-π½ X)
-
-Semigroup-π½ :
- (l : Level) β UU (lsuc l)
-Semigroup-π½ l = Ξ£ (π½ l) has-associative-mul-π½
-
-compute-semigroup-π½ :
- {l : Level} β (G : Semigroup l) β is-finite (type-Semigroup G) β Semigroup-π½ l
-pr1 (pr1 (compute-semigroup-π½ G f)) = type-Semigroup G
-pr2 (pr1 (compute-semigroup-π½ G f)) = f
-pr2 (compute-semigroup-π½ G f) = has-associative-mul-Semigroup G
-
-module _
- {l : Level} (G : Semigroup-π½ l)
- where
-
- finite-type-Semigroup-π½ : π½ l
- finite-type-Semigroup-π½ = pr1 G
-
- type-Semigroup-π½ : UU l
- type-Semigroup-π½ = type-π½ finite-type-Semigroup-π½
-
- is-finite-type-Semigroup-π½ : is-finite type-Semigroup-π½
- is-finite-type-Semigroup-π½ = is-finite-type-π½ finite-type-Semigroup-π½
-
- has-associative-mul-Semigroup-π½ : has-associative-mul type-Semigroup-π½
- has-associative-mul-Semigroup-π½ = pr2 G
-
- semigroup-Semigroup-π½ : Semigroup l
- pr1 semigroup-Semigroup-π½ = set-π½ finite-type-Semigroup-π½
- pr2 semigroup-Semigroup-π½ = has-associative-mul-Semigroup-π½
-
- set-Semigroup-π½ : Set l
- set-Semigroup-π½ = set-Semigroup semigroup-Semigroup-π½
-
- is-set-type-Semigroup-π½ : is-set type-Semigroup-π½
- is-set-type-Semigroup-π½ = is-set-type-Semigroup semigroup-Semigroup-π½
-
- mul-Semigroup-π½ : type-Semigroup-π½ β type-Semigroup-π½ β type-Semigroup-π½
- mul-Semigroup-π½ = mul-Semigroup semigroup-Semigroup-π½
-
- mul-Semigroup-π½' : type-Semigroup-π½ β type-Semigroup-π½ β type-Semigroup-π½
- mul-Semigroup-π½' = mul-Semigroup' semigroup-Semigroup-π½
-
- ap-mul-Semigroup-π½ :
- {x x' y y' : type-Semigroup-π½} β
- x οΌ x' β y οΌ y' β mul-Semigroup-π½ x y οΌ mul-Semigroup-π½ x' y'
- ap-mul-Semigroup-π½ = ap-mul-Semigroup semigroup-Semigroup-π½
-
- associative-mul-Semigroup-π½ :
- (x y z : type-Semigroup-π½) β
- Id
- ( mul-Semigroup-π½ (mul-Semigroup-π½ x y) z)
- ( mul-Semigroup-π½ x (mul-Semigroup-π½ y z))
- associative-mul-Semigroup-π½ = associative-mul-Semigroup semigroup-Semigroup-π½
-```
-
-## Properties
-
-### There is a finite number of ways to equip a finite type with a structure of semigroup
-
-```agda
-structure-semigroup-π½ :
- {l1 : Level} β π½ l1 β UU l1
-structure-semigroup-π½ = has-associative-mul-π½
-
-is-finite-structure-semigroup-π½ :
- {l : Level} β (X : π½ l) β is-finite (structure-semigroup-π½ X)
-is-finite-structure-semigroup-π½ X =
- is-finite-Ξ£
- ( is-finite-Ξ
- ( is-finite-type-π½ X)
- ( Ξ» _ β is-finite-Ξ (is-finite-type-π½ X) (Ξ» _ β is-finite-type-π½ X)))
- ( Ξ» m β
- is-finite-Ξ
- ( is-finite-type-π½ X)
- ( Ξ» x β
- is-finite-Ξ
- ( is-finite-type-π½ X)
- ( Ξ» y β
- is-finite-Ξ
- ( is-finite-type-π½ X)
- ( Ξ» z β
- is-finite-is-decidable-Prop
- ( (m (m x y) z οΌ m x (m y z)) ,
- is-set-is-finite
- ( is-finite-type-π½ X)
- ( m (m x y) z)
- ( m x (m y z)))
- ( has-decidable-equality-is-finite
- ( is-finite-type-π½ X)
- ( m (m x y) z)
- ( m x (m y z)))))))
-```
diff --git a/src/finite-algebra/products-finite-rings.lagda.md b/src/finite-algebra/products-finite-rings.lagda.md
index 983599225b..ad21624529 100644
--- a/src/finite-algebra/products-finite-rings.lagda.md
+++ b/src/finite-algebra/products-finite-rings.lagda.md
@@ -159,5 +159,5 @@ module _
product-Ring-π½ : Ring-π½ (l1 β l2)
product-Ring-π½ =
- compute-ring-π½ ring-product-Ring-π½ is-finite-type-product-Ring-π½
+ finite-ring-is-finite-Ring ring-product-Ring-π½ is-finite-type-product-Ring-π½
```
diff --git a/src/finite-algebra/semisimple-commutative-finite-rings.lagda.md b/src/finite-algebra/semisimple-commutative-finite-rings.lagda.md
index f260f00137..2f4184550c 100644
--- a/src/finite-algebra/semisimple-commutative-finite-rings.lagda.md
+++ b/src/finite-algebra/semisimple-commutative-finite-rings.lagda.md
@@ -17,6 +17,7 @@ open import finite-algebra.homomorphisms-commutative-finite-rings
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
open import foundation.propositional-truncations
open import foundation.universe-levels
@@ -69,7 +70,7 @@ module _
## Properties
-### The number of ways to equip a finite type with a structure of semisimple commutative finite ring is finite
+### The number of ways to equip a finite type with the structure of a semisimple commutative ring is finite
```agda
module _
@@ -85,12 +86,13 @@ module _
( Ξ» r β
is-semisimple-Commutative-Ring-π½
( l2)
- ( compute-structure-commutative-ring-π½ X r))
+ ( finite-commutative-ring-structure-commutative-ring-π½ X r))
- compute-structure-semisimple-commutative-ring-π½ :
+ finite-semisimple-commutative-ring-structure-semisimple-commutative-ring-π½ :
structure-semisimple-commutative-ring-π½ β
Semisimple-Commutative-Ring-π½ l1 l2
- pr1 (compute-structure-semisimple-commutative-ring-π½ (p , s)) =
- compute-structure-commutative-ring-π½ X p
- pr2 (compute-structure-semisimple-commutative-ring-π½ (p , s)) = s
+ finite-semisimple-commutative-ring-structure-semisimple-commutative-ring-π½ =
+ map-Ξ£-map-base
+ ( finite-commutative-ring-structure-commutative-ring-π½ X)
+ ( is-semisimple-Commutative-Ring-π½ l2)
```
diff --git a/src/finite-group-theory.lagda.md b/src/finite-group-theory.lagda.md
index f1821d381d..e618f005a3 100644
--- a/src/finite-group-theory.lagda.md
+++ b/src/finite-group-theory.lagda.md
@@ -11,6 +11,8 @@ open import finite-group-theory.alternating-groups public
open import finite-group-theory.cartier-delooping-sign-homomorphism public
open import finite-group-theory.concrete-quaternion-group public
open import finite-group-theory.delooping-sign-homomorphism public
+open import finite-group-theory.finite-abelian-groups public
+open import finite-group-theory.finite-commutative-monoids public
open import finite-group-theory.finite-groups public
open import finite-group-theory.finite-monoids public
open import finite-group-theory.finite-semigroups public
diff --git a/src/finite-algebra/finite-abelian-groups.lagda.md b/src/finite-group-theory/finite-abelian-groups.lagda.md
similarity index 92%
rename from src/finite-algebra/finite-abelian-groups.lagda.md
rename to src/finite-group-theory/finite-abelian-groups.lagda.md
index 9b41ae19dc..137c9c647a 100644
--- a/src/finite-algebra/finite-abelian-groups.lagda.md
+++ b/src/finite-group-theory/finite-abelian-groups.lagda.md
@@ -1,13 +1,13 @@
# Abelian groups
```agda
-module finite-algebra.finite-abelian-groups where
+module finite-group-theory.finite-abelian-groups where
```
Imports
```agda
-open import finite-algebra.finite-groups
+open import finite-group-theory.finite-groups
open import foundation.equivalences
open import foundation.identity-types
@@ -57,10 +57,11 @@ is-prop-is-abelian-Group-π½ G =
Ab-π½ : (l : Level) β UU (lsuc l)
Ab-π½ l = Ξ£ (Group-π½ l) is-abelian-Group-π½
-compute-abelian-group-π½ :
+finite-abelian-group-is-finite-Ab :
{l : Level} β (A : Ab l) β is-finite (type-Ab A) β Ab-π½ l
-pr1 (compute-abelian-group-π½ A f) = compute-group-π½ (group-Ab A) f
-pr2 (compute-abelian-group-π½ A f) = pr2 A
+pr1 (finite-abelian-group-is-finite-Ab A f) =
+ finite-group-is-finite-Group (group-Ab A) f
+pr2 (finite-abelian-group-is-finite-Ab A f) = pr2 A
module _
{l : Level} (A : Ab-π½ l)
@@ -204,7 +205,7 @@ module _
## Properties
-### There is a finite number of ways to equip a finite type with a structure of abelian group
+### There is a finite number of ways to equip a finite type with the structure of an abelian group
```agda
module _
@@ -215,13 +216,13 @@ module _
structure-abelian-group-π½ : UU l
structure-abelian-group-π½ =
Ξ£ ( structure-group-π½ X)
- ( Ξ» g β is-abelian-Group-π½ (compute-structure-group-π½ X g))
+ ( Ξ» g β is-abelian-Group-π½ (finite-group-structure-group-π½ X g))
- compute-structure-abelian-group-π½ :
+ finite-abelian-group-structure-abelian-group-π½ :
structure-abelian-group-π½ β Ab-π½ l
- pr1 (compute-structure-abelian-group-π½ (m , c)) =
- compute-structure-group-π½ X m
- pr2 (compute-structure-abelian-group-π½ (m , c)) = c
+ pr1 (finite-abelian-group-structure-abelian-group-π½ (m , c)) =
+ finite-group-structure-group-π½ X m
+ pr2 (finite-abelian-group-structure-abelian-group-π½ (m , c)) = c
is-finite-structure-abelian-group-π½ :
is-finite structure-abelian-group-π½
diff --git a/src/finite-algebra/finite-commutative-monoids.lagda.md b/src/finite-group-theory/finite-commutative-monoids.lagda.md
similarity index 93%
rename from src/finite-algebra/finite-commutative-monoids.lagda.md
rename to src/finite-group-theory/finite-commutative-monoids.lagda.md
index c6d35c3d73..02ffea267b 100644
--- a/src/finite-algebra/finite-commutative-monoids.lagda.md
+++ b/src/finite-group-theory/finite-commutative-monoids.lagda.md
@@ -1,13 +1,13 @@
# Finite Commutative monoids
```agda
-module finite-algebra.finite-commutative-monoids where
+module finite-group-theory.finite-commutative-monoids where
```
Imports
```agda
-open import finite-algebra.finite-monoids
+open import finite-group-theory.finite-monoids
open import foundation.identity-types
open import foundation.sets
@@ -179,7 +179,7 @@ module _
## Properties
-### There is a finite number of ways to equip a finite type with a structure of finite commutative monoids
+### There is a finite number of ways to equip a finite type with the structure of a finite commutative monoid
```agda
module _
@@ -190,13 +190,13 @@ module _
structure-commutative-monoid-π½ : UU l
structure-commutative-monoid-π½ =
Ξ£ ( structure-monoid-π½ X)
- ( Ξ» m β is-commutative-Monoid-π½ (compute-structure-monoid-π½ X m))
+ ( Ξ» m β is-commutative-Monoid-π½ (finite-monoid-structure-monoid-π½ X m))
- compute-structure-commutative-monoid-π½ :
+ finite-commutative-monoid-structure-commutative-monoid-π½ :
structure-commutative-monoid-π½ β Commutative-Monoid-π½ l
- pr1 (compute-structure-commutative-monoid-π½ (m , c)) =
- compute-structure-monoid-π½ X m
- pr2 (compute-structure-commutative-monoid-π½ (m , c)) = c
+ pr1 (finite-commutative-monoid-structure-commutative-monoid-π½ (m , c)) =
+ finite-monoid-structure-monoid-π½ X m
+ pr2 (finite-commutative-monoid-structure-commutative-monoid-π½ (m , c)) = c
is-finite-structure-commutative-monoid-π½ :
is-finite structure-commutative-monoid-π½
diff --git a/src/finite-group-theory/finite-groups.lagda.md b/src/finite-group-theory/finite-groups.lagda.md
index ac29136492..fbb7a1421a 100644
--- a/src/finite-group-theory/finite-groups.lagda.md
+++ b/src/finite-group-theory/finite-groups.lagda.md
@@ -9,6 +9,7 @@ module finite-group-theory.finite-groups where
```agda
open import elementary-number-theory.natural-numbers
+open import finite-group-theory.finite-monoids
open import finite-group-theory.finite-semigroups
open import foundation.binary-embeddings
@@ -30,6 +31,7 @@ open import foundation.sets
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels
+open import group-theory.commuting-elements-groups
open import group-theory.groups
open import group-theory.monoids
open import group-theory.semigroups
@@ -43,6 +45,7 @@ open import univalent-combinatorics.decidable-dependent-function-types
open import univalent-combinatorics.decidable-dependent-pair-types
open import univalent-combinatorics.decidable-propositions
open import univalent-combinatorics.dependent-function-types
+open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.function-types
@@ -54,17 +57,37 @@ open import univalent-combinatorics.standard-finite-types
## Idea
-A finite group is a group of which the underlying type is finite.
+An {{#concept "(abstract) finite group" Agda=Group-π½}} is a finite group in the
+usual algebraic sense, i.e., it consists of a
+[finite type](univalent-combinatorics.finite-types.md)
+[equipped](foundation.structure.md) with a unit element `e`, a binary operation
+`x, y β¦ xy`, and an inverse operation `x β¦ xβ»ΒΉ` satisfying the
+[group](group-theory.groups.md) laws
+
+```text
+ (xy)z = x(yz) (associativity)
+ ex = x (left unit law)
+ xe = x (right unit law)
+ xβ»ΒΉx = e (left inverse law)
+ xxβ»ΒΉ = e (right inverse law)
+```
## Definitions
+### The condition that a finite semigroup is a finite group
+
+```agda
+is-group-π½ :
+ {l : Level} (G : Semigroup-π½ l) β UU l
+is-group-π½ G = is-group (semigroup-Semigroup-π½ G)
+```
+
### The type of finite groups
```agda
Group-π½ :
(l : Level) β UU (lsuc l)
-Group-π½ l =
- Ξ£ (Semigroup-π½ l) (Ξ» G β is-group (semigroup-Semigroup-π½ G))
+Group-π½ l = Ξ£ (Semigroup-π½ l) (is-group-π½)
module _
{l : Level} (G : Group-π½ l)
@@ -282,6 +305,23 @@ module _
inv-inv-Group-π½ :
(x : type-Group-π½) β inv-Group-π½ (inv-Group-π½ x) οΌ x
inv-inv-Group-π½ = inv-inv-Group group-Group-π½
+
+finite-group-is-finite-Group :
+ {l : Level} β (G : Group l) β is-finite (type-Group G) β Group-π½ l
+pr1 (finite-group-is-finite-Group G f) =
+ finite-semigroup-is-finite-Semigroup (semigroup-Group G) f
+pr2 (finite-group-is-finite-Group G f) = is-group-Group G
+
+module _
+ {l : Level} (G : Group-π½ l)
+ where
+
+ commute-Group-π½ : type-Group-π½ G β type-Group-π½ G β UU l
+ commute-Group-π½ = commute-Group (group-Group-π½ G)
+
+ finite-monoid-Group-π½ : Monoid-π½ l
+ pr1 finite-monoid-Group-π½ = finite-semigroup-Group-π½ G
+ pr2 finite-monoid-Group-π½ = is-unital-Group-π½ G
```
### Groups of fixed finite order
@@ -374,3 +414,43 @@ mere-equiv-number-of-groups-of-order n =
mere-equiv-number-of-connected-components
( is-Ο-finite-Group-of-Order {lzero} zero-β n)
```
+
+### There is a finite number of ways to equip a finite type with the structure of a group
+
+```agda
+module _
+ {l : Level}
+ (X : π½ l)
+ where
+
+ structure-group-π½ : UU l
+ structure-group-π½ =
+ Ξ£ (structure-semigroup-π½ X) (Ξ» s β is-group-π½ (X , s))
+
+ finite-group-structure-group-π½ :
+ structure-group-π½ β Group-π½ l
+ pr1 (finite-group-structure-group-π½ (s , g)) = (X , s)
+ pr2 (finite-group-structure-group-π½ (s , g)) = g
+
+ is-finite-structure-group-π½ :
+ is-finite (structure-group-π½)
+ is-finite-structure-group-π½ =
+ is-finite-Ξ£
+ ( is-finite-structure-semigroup-π½ X)
+ ( Ξ» s β
+ is-finite-Ξ£
+ ( is-finite-is-unital-Semigroup-π½ (X , s))
+ ( Ξ» u β
+ is-finite-Ξ£
+ ( is-finite-Ξ
+ ( is-finite-type-π½ X)
+ ( Ξ» _ β is-finite-type-π½ X))
+ ( Ξ» i β
+ is-finite-product
+ ( is-finite-Ξ
+ ( is-finite-type-π½ X)
+ ( Ξ» x β is-finite-eq-π½ X))
+ ( is-finite-Ξ
+ ( is-finite-type-π½ X)
+ ( Ξ» x β is-finite-eq-π½ X)))))
+```
diff --git a/src/finite-group-theory/finite-monoids.lagda.md b/src/finite-group-theory/finite-monoids.lagda.md
index e9d8d415a3..a9fa4daee5 100644
--- a/src/finite-group-theory/finite-monoids.lagda.md
+++ b/src/finite-group-theory/finite-monoids.lagda.md
@@ -15,18 +15,26 @@ open import foundation.decidable-propositions
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.equivalences
+open import foundation.identity-types
open import foundation.mere-equivalences
open import foundation.propositional-truncations
+open import foundation.propositions
open import foundation.set-truncations
+open import foundation.sets
open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.unital-binary-operations
open import foundation.universe-levels
open import group-theory.monoids
open import group-theory.semigroups
+open import univalent-combinatorics.cartesian-product-types
open import univalent-combinatorics.counting
open import univalent-combinatorics.decidable-dependent-function-types
open import univalent-combinatorics.decidable-dependent-pair-types
+open import univalent-combinatorics.dependent-function-types
+open import univalent-combinatorics.dependent-pair-types
+open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.pi-finite-types
open import univalent-combinatorics.standard-finite-types
@@ -40,7 +48,78 @@ A finite monoid is a monoid of which the underlying type is finite.
## Definition
-### Monoids of order n
+### The type of finite monoids
+
+```agda
+is-unital-Semigroup-π½ :
+ {l : Level} β Semigroup-π½ l β UU l
+is-unital-Semigroup-π½ G = is-unital (mul-Semigroup-π½ G)
+
+Monoid-π½ :
+ (l : Level) β UU (lsuc l)
+Monoid-π½ l = Ξ£ (Semigroup-π½ l) is-unital-Semigroup-π½
+
+module _
+ {l : Level} (M : Monoid-π½ l)
+ where
+
+ finite-semigroup-Monoid-π½ : Semigroup-π½ l
+ finite-semigroup-Monoid-π½ = pr1 M
+
+ semigroup-Monoid-π½ : Semigroup l
+ semigroup-Monoid-π½ = semigroup-Semigroup-π½ finite-semigroup-Monoid-π½
+
+ finite-type-Monoid-π½ : π½ l
+ finite-type-Monoid-π½ = finite-type-Semigroup-π½ finite-semigroup-Monoid-π½
+
+ type-Monoid-π½ : UU l
+ type-Monoid-π½ = type-Semigroup-π½ finite-semigroup-Monoid-π½
+
+ is-finite-type-Monoid-π½ : is-finite type-Monoid-π½
+ is-finite-type-Monoid-π½ = is-finite-type-Semigroup-π½ finite-semigroup-Monoid-π½
+
+ set-Monoid-π½ : Set l
+ set-Monoid-π½ = set-Semigroup semigroup-Monoid-π½
+
+ is-set-type-Monoid-π½ : is-set type-Monoid-π½
+ is-set-type-Monoid-π½ = is-set-type-Semigroup semigroup-Monoid-π½
+
+ mul-Monoid-π½ : type-Monoid-π½ β type-Monoid-π½ β type-Monoid-π½
+ mul-Monoid-π½ = mul-Semigroup semigroup-Monoid-π½
+
+ mul-Monoid-π½' : type-Monoid-π½ β type-Monoid-π½ β type-Monoid-π½
+ mul-Monoid-π½' y x = mul-Monoid-π½ x y
+
+ ap-mul-Monoid-π½ :
+ {x x' y y' : type-Monoid-π½} β
+ x οΌ x' β y οΌ y' β mul-Monoid-π½ x y οΌ mul-Monoid-π½ x' y'
+ ap-mul-Monoid-π½ = ap-mul-Semigroup semigroup-Monoid-π½
+
+ associative-mul-Monoid-π½ :
+ (x y z : type-Monoid-π½) β
+ mul-Monoid-π½ (mul-Monoid-π½ x y) z οΌ mul-Monoid-π½ x (mul-Monoid-π½ y z)
+ associative-mul-Monoid-π½ = associative-mul-Semigroup semigroup-Monoid-π½
+
+ has-unit-Monoid-π½ : is-unital mul-Monoid-π½
+ has-unit-Monoid-π½ = pr2 M
+
+ monoid-Monoid-π½ : Monoid l
+ pr1 monoid-Monoid-π½ = semigroup-Monoid-π½
+ pr2 monoid-Monoid-π½ = has-unit-Monoid-π½
+
+ unit-Monoid-π½ : type-Monoid-π½
+ unit-Monoid-π½ = unit-Monoid monoid-Monoid-π½
+
+ left-unit-law-mul-Monoid-π½ :
+ (x : type-Monoid-π½) β mul-Monoid-π½ unit-Monoid-π½ x οΌ x
+ left-unit-law-mul-Monoid-π½ = left-unit-law-mul-Monoid monoid-Monoid-π½
+
+ right-unit-law-mul-Monoid-π½ :
+ (x : type-Monoid-π½) β mul-Monoid-π½ x unit-Monoid-π½ οΌ x
+ right-unit-law-mul-Monoid-π½ = right-unit-law-mul-Monoid monoid-Monoid-π½
+```
+
+### Monoids of order `n`
```agda
Monoid-of-Order : (l : Level) (n : β) β UU (lsuc l)
@@ -49,7 +128,7 @@ Monoid-of-Order l n = Ξ£ (Monoid l) (Ξ» M β mere-equiv (Fin n) (type-Monoid M)
## Properties
-### For any semigroup of order n, the type of multiplicative units is finite
+### For any semigroup of order `n`, the type of multiplicative units is finite
```agda
is-finite-is-unital-Semigroup :
@@ -101,7 +180,7 @@ is-Ο-finite-Monoid-of-Order {l} k n =
e = equiv-right-swap-Ξ£
```
-### The function that returns for any n the number of monoids of order n up to isomorphism
+### The function that returns for any `n` the number of monoids of order `n` up to isomorphism
```agda
number-of-monoids-of-order : β β β
@@ -118,3 +197,56 @@ mere-equiv-number-of-monoids-of-order n =
mere-equiv-number-of-connected-components
( is-Ο-finite-Monoid-of-Order {lzero} zero-β n)
```
+
+### For any finite semigroup `G`, being unital is a property
+
+```agda
+abstract
+ is-prop-is-unital-Semigroup-π½ :
+ {l : Level} (G : Semigroup-π½ l) β is-prop (is-unital-Semigroup-π½ G)
+ is-prop-is-unital-Semigroup-π½ G =
+ is-prop-is-unital-Semigroup (semigroup-Semigroup-π½ G)
+
+is-unital-Semigroup-π½-Prop : {l : Level} (G : Semigroup-π½ l) β Prop l
+pr1 (is-unital-Semigroup-π½-Prop G) = is-unital-Semigroup-π½ G
+pr2 (is-unital-Semigroup-π½-Prop G) = is-prop-is-unital-Semigroup-π½ G
+```
+
+### For any finite semigroup `G`, being unital is finite
+
+```agda
+is-finite-is-unital-Semigroup-π½ :
+ {l : Level} (G : Semigroup-π½ l) β is-finite (is-unital-Semigroup-π½ G)
+is-finite-is-unital-Semigroup-π½ G =
+ is-finite-Ξ£
+ ( is-finite-type-Semigroup-π½ G)
+ ( Ξ» e β
+ is-finite-product
+ ( is-finite-Ξ
+ ( is-finite-type-Semigroup-π½ G)
+ ( Ξ» x β is-finite-eq-π½ (finite-type-Semigroup-π½ G)))
+ ( is-finite-Ξ
+ ( is-finite-type-Semigroup-π½ G)
+ ( Ξ» x β is-finite-eq-π½ (finite-type-Semigroup-π½ G))))
+```
+
+### There is a finite number of ways to equip a finite type with the structure of a monoid
+
+```agda
+structure-monoid-π½ :
+ {l1 : Level} β π½ l1 β UU l1
+structure-monoid-π½ X =
+ Ξ£ (structure-semigroup-π½ X) (Ξ» p β is-unital-Semigroup-π½ (X , p))
+
+finite-monoid-structure-monoid-π½ :
+ {l : Level} β (X : π½ l) β structure-monoid-π½ X β Monoid-π½ l
+pr1 (finite-monoid-structure-monoid-π½ X (a , u)) = X , a
+pr2 (finite-monoid-structure-monoid-π½ X (a , u)) = u
+
+is-finite-structure-monoid-π½ :
+ {l : Level} β (X : π½ l) β is-finite (structure-monoid-π½ X)
+is-finite-structure-monoid-π½ X =
+ is-finite-Ξ£
+ ( is-finite-structure-semigroup-π½ X)
+ ( Ξ» m β is-finite-is-unital-Semigroup-π½ (X , m))
+```
diff --git a/src/finite-group-theory/finite-semigroups.lagda.md b/src/finite-group-theory/finite-semigroups.lagda.md
index 95c63559fb..14bbbfe4f2 100644
--- a/src/finite-group-theory/finite-semigroups.lagda.md
+++ b/src/finite-group-theory/finite-semigroups.lagda.md
@@ -9,6 +9,7 @@ module finite-group-theory.finite-semigroups where
```agda
open import elementary-number-theory.natural-numbers
+open import foundation.decidable-propositions
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
@@ -39,12 +40,18 @@ Finite semigroups are semigroups of which the underlying type is finite.
## Definitions
+### The predicate of having an associative multiplication operation on finite types
+
+```agda
+has-associative-mul-π½ : {l : Level} (X : π½ l) β UU l
+has-associative-mul-π½ X = has-associative-mul (type-π½ X)
+```
+
### Finite semigroups
```agda
Semigroup-π½ : (l : Level) β UU (lsuc l)
-Semigroup-π½ l =
- Ξ£ (π½ l) (Ξ» X β has-associative-mul (type-π½ X))
+Semigroup-π½ l = Ξ£ (π½ l) (has-associative-mul-π½)
module _
{l : Level} (G : Semigroup-π½ l)
@@ -89,9 +96,24 @@ module _
( mul-Semigroup-π½ x (mul-Semigroup-π½ y z))
associative-mul-Semigroup-π½ =
associative-mul-Semigroup semigroup-Semigroup-π½
+
+finite-semigroup-is-finite-Semigroup :
+ {l : Level} β (G : Semigroup l) β is-finite (type-Semigroup G) β Semigroup-π½ l
+pr1 (pr1 (finite-semigroup-is-finite-Semigroup G f)) = type-Semigroup G
+pr2 (pr1 (finite-semigroup-is-finite-Semigroup G f)) = f
+pr2 (finite-semigroup-is-finite-Semigroup G f) = has-associative-mul-Semigroup G
+
+module _
+ {l : Level} (G : Semigroup-π½ l)
+ where
+
+ ap-mul-Semigroup-π½ :
+ {x x' y y' : type-Semigroup-π½ G} β
+ x οΌ x' β y οΌ y' β mul-Semigroup-π½ G x y οΌ mul-Semigroup-π½ G x' y'
+ ap-mul-Semigroup-π½ = ap-mul-Semigroup (semigroup-Semigroup-π½ G)
```
-### Semigroups of order n
+### Semigroups of order `n`
```agda
Semigroup-of-Order' : (l : Level) (n : β) β UU (lsuc l)
@@ -124,7 +146,7 @@ is-finite-has-associative-mul H =
is-finite-eq (has-decidable-equality-is-finite H)))))
```
-### The type of semigroups of order n is Ο-finite
+### The type of semigroups of order `n` is Ο-finite
```agda
is-Ο-finite-Semigroup-of-Order' :
@@ -176,3 +198,39 @@ mere-equiv-number-of-semi-groups-of-order n =
mere-equiv-number-of-connected-components
( is-Ο-finite-Semigroup-of-Order {lzero} zero-β n)
```
+
+### There is a finite number of ways to equip a finite type with the structure of a semigroup
+
+```agda
+structure-semigroup-π½ :
+ {l1 : Level} β π½ l1 β UU l1
+structure-semigroup-π½ = has-associative-mul-π½
+
+is-finite-structure-semigroup-π½ :
+ {l : Level} β (X : π½ l) β is-finite (structure-semigroup-π½ X)
+is-finite-structure-semigroup-π½ X =
+ is-finite-Ξ£
+ ( is-finite-Ξ
+ ( is-finite-type-π½ X)
+ ( Ξ» _ β is-finite-Ξ (is-finite-type-π½ X) (Ξ» _ β is-finite-type-π½ X)))
+ ( Ξ» m β
+ is-finite-Ξ
+ ( is-finite-type-π½ X)
+ ( Ξ» x β
+ is-finite-Ξ
+ ( is-finite-type-π½ X)
+ ( Ξ» y β
+ is-finite-Ξ
+ ( is-finite-type-π½ X)
+ ( Ξ» z β
+ is-finite-is-decidable-Prop
+ ( (m (m x y) z οΌ m x (m y z)) ,
+ is-set-is-finite
+ ( is-finite-type-π½ X)
+ ( m (m x y) z)
+ ( m x (m y z)))
+ ( has-decidable-equality-is-finite
+ ( is-finite-type-π½ X)
+ ( m (m x y) z)
+ ( m x (m y z)))))))
+```
diff --git a/src/foundation/path-algebra.lagda.md b/src/foundation/path-algebra.lagda.md
index 96a439ae35..bb110a0312 100644
--- a/src/foundation/path-algebra.lagda.md
+++ b/src/foundation/path-algebra.lagda.md
@@ -37,12 +37,12 @@ type is often called a _type of 2-paths_.
Since 2-paths are just identifications, they have the usual operations and
coherences on paths/identifications. In the context of 2-paths, this famliar
-concatination operation is called vertical concatination (see
+concatenation operation is called vertical concatenation (see
`vertical-concat-IdΒ²` below). However, 2-paths have novel operations and
coherences derived from the operations and coherences of the boundary 1-paths
-(these are `p` and `q` in the example above). Since concatination of 1-paths is
+(these are `p` and `q` in the example above). Since concatenation of 1-paths is
a functor, it has an induced action on paths. We call this operation horizontal
-concatination (see `horizontal-concat-IdΒ²` below). It comes with the standard
+concatenation (see `horizontal-concat-IdΒ²` below). It comes with the standard
coherences of an action on paths function, as well as coherences induced by
coherences on the boundary 1-paths.
@@ -187,7 +187,7 @@ right-unit-law-horizontal-concat-IdΒ² :
right-unit-law-horizontal-concat-IdΒ² = right-unit-ap-binary (_β_)
```
-Horizontal concatination satisfies an additional "2-dimensional" unit law (on
+Horizontal concatenation satisfies an additional "2-dimensional" unit law (on
both the left and right) induced by the unit laws on the boundary 1-paths.
```agda
@@ -318,7 +318,7 @@ unit-law-Ξ΄-interchange-IdΒ² p refl = refl
3-paths are identifications of 2-paths. In symbols, a type of 3-paths is a type
of the form `Ξ± οΌ Ξ²` where `Ξ± Ξ² : p οΌ q` and `p q : x οΌ y`.
-### Concatination in a type of 3-paths
+### Concatenation in a type of 3-paths
Like with 2-paths, 3-paths have the standard operations on equalties, plus the
operations induced by the operations on 1-paths. But 3-paths also have
@@ -327,7 +327,7 @@ in triple identity types. We name the three concatenations of triple identity
types x-, y-, and z-concatenation, after the standard names for the three axis
in 3-dimensional space.
-The x-concatenation operation corresponds the standard concatination of
+The x-concatenation operation corresponds the standard concatenation of
equalities.
```agda
@@ -338,7 +338,7 @@ x-concat-IdΒ³ Ο Ο = vertical-concat-IdΒ² Ο Ο
```
The y-concatenation operation corresponds the operation induced by the
-concatination on 1-paths.
+concatenation on 1-paths.
```agda
y-concat-IdΒ³ :
@@ -347,8 +347,8 @@ y-concat-IdΒ³ :
y-concat-IdΒ³ = horizontal-concat-IdΒ²
```
-The z-concatenation operation corresponds the concatination induced by the
-horizontal concatination on 2-paths.
+The z-concatenation operation corresponds the concatenation induced by the
+horizontal concatenation on 2-paths.
```agda
z-concat-IdΒ³ :
@@ -436,7 +436,7 @@ after the standard names for the quaternions `i`, `j`, and `k`.
### Concatenation of four paths
-#### The standard concatination
+#### The standard concatenation
```agda
concat-Idβ΄ :
@@ -445,7 +445,7 @@ concat-Idβ΄ :
concat-Idβ΄ Ο Ο = x-concat-IdΒ³ Ο Ο
```
-#### Concatination induced by concatination of boundary 1-paths
+#### Concatenation induced by concatenation of boundary 1-paths
```agda
i-concat-Idβ΄ :
@@ -455,7 +455,7 @@ i-concat-Idβ΄ :
i-concat-Idβ΄ Ο Ο = y-concat-IdΒ³ Ο Ο
```
-#### Concatination induced by concatination of boundary 2-paths
+#### Concatenation induced by concatenation of boundary 2-paths
```agda
j-concat-Idβ΄ :
@@ -465,7 +465,7 @@ j-concat-Idβ΄ :
j-concat-Idβ΄ Ο Ο = z-concat-IdΒ³ Ο Ο
```
-#### Concatination induced by concatination of boundary 3-paths
+#### Concatenation induced by concatenation of boundary 3-paths
```agda
k-concat-Idβ΄ :
@@ -482,7 +482,7 @@ module _
{l : Level} {A : UU l} {x000 x001 x010 x100 x011 x101 x110 x111 : A}
where
- cube :
+ coherence-cube-identifications :
(p000Μ : x000 οΌ x001) (p00Μ0 : x000 οΌ x010) (p0Μ00 : x000 οΌ x100)
(p00Μ1 : x001 οΌ x011) (p0Μ01 : x001 οΌ x101) (p010Μ : x010 οΌ x011)
(p0Μ10 : x010 οΌ x110) (p100Μ : x100 οΌ x101) (p10Μ0 : x100 οΌ x110)
@@ -493,7 +493,7 @@ module _
(p0Μ0Μ1 : coherence-square-identifications p0Μ01 p00Μ1 p10Μ1 p0Μ11)
(p0Μ10Μ : coherence-square-identifications p0Μ10 p010Μ p110Μ p0Μ11)
(p10Μ0Μ : coherence-square-identifications p10Μ0 p100Μ p110Μ p10Μ1) β UU l
- cube
+ coherence-cube-identifications
p000Μ p00Μ0 p0Μ00 p00Μ1 p0Μ01 p010Μ p0Μ10 p100Μ p10Μ0 p0Μ11 p10Μ1 p110Μ
p00Μ0Μ p0Μ00Μ p0Μ0Μ0 p0Μ0Μ1 p0Μ10Μ p10Μ0Μ =
Id
diff --git a/src/group-theory/abelian-groups.lagda.md b/src/group-theory/abelian-groups.lagda.md
index 22fb7110a0..518213fe02 100644
--- a/src/group-theory/abelian-groups.lagda.md
+++ b/src/group-theory/abelian-groups.lagda.md
@@ -240,12 +240,13 @@ module _
structure-abelian-group :
{l1 : Level} β UU l1 β UU l1
structure-abelian-group X =
- Ξ£ (structure-group X) (Ξ» p β is-abelian-Group (compute-structure-group X p))
+ Ξ£ (structure-group X) (Ξ» p β is-abelian-Group (group-structure-group X p))
-compute-structure-abelian-group :
+abelian-group-structure-abelian-group :
{l1 : Level} β (X : UU l1) β structure-abelian-group X β Ab l1
-pr1 (compute-structure-abelian-group X (p , q)) = compute-structure-group X p
-pr2 (compute-structure-abelian-group X (p , q)) = q
+pr1 (abelian-group-structure-abelian-group X (p , q)) =
+ group-structure-group X p
+pr2 (abelian-group-structure-abelian-group X (p , q)) = q
```
### Conjugation in an abelian group
diff --git a/src/group-theory/groups.lagda.md b/src/group-theory/groups.lagda.md
index 9376350274..513db7f496 100644
--- a/src/group-theory/groups.lagda.md
+++ b/src/group-theory/groups.lagda.md
@@ -216,12 +216,12 @@ module _
structure-group :
{l1 : Level} β UU l1 β UU l1
structure-group X =
- Ξ£ (structure-semigroup X) (Ξ» p β is-group (compute-structure-semigroup X p))
+ Ξ£ (structure-semigroup X) (Ξ» p β is-group (semigroup-structure-semigroup X p))
-compute-structure-group :
+group-structure-group :
{l1 : Level} β (X : UU l1) β structure-group X β Group l1
-pr1 (compute-structure-group X (p , q)) = compute-structure-semigroup X p
-pr2 (compute-structure-group X (p , q)) = q
+pr1 (group-structure-group X (p , q)) = semigroup-structure-semigroup X p
+pr2 (group-structure-group X (p , q)) = q
```
## Properties
diff --git a/src/group-theory/semigroups.lagda.md b/src/group-theory/semigroups.lagda.md
index d90ca26f2f..be720c9094 100644
--- a/src/group-theory/semigroups.lagda.md
+++ b/src/group-theory/semigroups.lagda.md
@@ -108,8 +108,8 @@ structure-semigroup :
structure-semigroup X =
Ξ£ (is-set X) (Ξ» p β has-associative-mul-Set (X , p))
-compute-structure-semigroup :
+semigroup-structure-semigroup :
{l1 : Level} β (X : UU l1) β structure-semigroup X β Semigroup l1
-pr1 (compute-structure-semigroup X (s , g)) = X , s
-pr2 (compute-structure-semigroup X (s , g)) = g
+pr1 (semigroup-structure-semigroup X (s , g)) = X , s
+pr2 (semigroup-structure-semigroup X (s , g)) = g
```
diff --git a/src/orthogonal-factorization-systems/higher-modalities.lagda.md b/src/orthogonal-factorization-systems/higher-modalities.lagda.md
index 1ace39ec54..b44ca06b76 100644
--- a/src/orthogonal-factorization-systems/higher-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/higher-modalities.lagda.md
@@ -47,8 +47,8 @@ defining map (propositionally).
Lastly, higher modalities must also be **identity closed** in the sense that for
every type `X` the identity types `(x' οΌ y')` are modal for all terms
`x' y' : β X`. In other words, `β X` is
-[`β`-separated](orthogonal-factorization-systems.separated-types.md). Because of
-this, higher modalities in their most general form only make sense for
+[`β`-separated](foundation.separated-types.md). Because of this, higher
+modalities in their most general form only make sense for
[locally small modal operators](orthogonal-factorization-systems.locally-small-modal-operators.md).
## Definition
diff --git a/src/orthogonal-factorization-systems/separated-types.lagda.md b/src/orthogonal-factorization-systems/separated-types.lagda.md
index d773fc900e..965dcad305 100644
--- a/src/orthogonal-factorization-systems/separated-types.lagda.md
+++ b/src/orthogonal-factorization-systems/separated-types.lagda.md
@@ -28,11 +28,11 @@ module _
{l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (f : X β Y)
where
- is-separated-family : (X β UU l3) β UU (l1 β l2 β l3)
- is-separated-family A = (x : X) (y z : A x) β is-local f (y οΌ z)
+ is-map-separated-family : (X β UU l3) β UU (l1 β l2 β l3)
+ is-map-separated-family A = (x : X) (y z : A x) β is-local f (y οΌ z)
- is-separated : UU l3 β UU (l1 β l2 β l3)
- is-separated A = is-separated-family (Ξ» _ β A)
+ is-map-separated : UU l3 β UU (l1 β l2 β l3)
+ is-map-separated A = is-map-separated-family (Ξ» _ β A)
```
## References
diff --git a/src/reflection/abstractions.lagda.md b/src/reflection/abstractions.lagda.md
index 9dc0d8b673..6395c53b4c 100644
--- a/src/reflection/abstractions.lagda.md
+++ b/src/reflection/abstractions.lagda.md
@@ -16,14 +16,14 @@ open import primitives.strings
## Idea
-The `Abs` type represents a lambda abstraction.
+The `Abstraction-Agda` type represents a lambda abstraction.
## Definition
```agda
-data Abs {l} (A : UU l) : UU l where
- abs : String β A β Abs A
+data Abstraction-Agda {l : Level} (A : UU l) : UU l where
+ cons-Abstraction-Agda : String β A β Abstraction-Agda A
-{-# BUILTIN ABS Abs #-}
-{-# BUILTIN ABSABS abs #-}
+{-# BUILTIN ABS Abstraction-Agda #-}
+{-# BUILTIN ABSABS cons-Abstraction-Agda #-}
```
diff --git a/src/reflection/arguments.lagda.md b/src/reflection/arguments.lagda.md
index c225b10bf4..176d7be2c4 100644
--- a/src/reflection/arguments.lagda.md
+++ b/src/reflection/arguments.lagda.md
@@ -23,8 +23,8 @@ argument has three properties:
3. Quantity: whether they are run-time relevant or not (see,
[docs](https://agda.readthedocs.io/en/latest/language/runtime-irrelevance.html))
-The properties of `Relevance` and `Quantity` are combined in one, called
-`Modality`.
+The properties of `Relevance-Argument-Agda` and `Quantity-Argument-Agda` are
+combined in one, called `Modality-Argument-Agda`.
For concrete examples, see
[`reflection.definitions`](reflection.definitions.md).
@@ -32,49 +32,55 @@ For concrete examples, see
## Definitions
```agda
-data Visibility : UU lzero where
- visible hidden instanceβ² : Visibility
+data Visibility-Argument-Agda : UU lzero where
+ visible-Visibility-Argument-Agda : Visibility-Argument-Agda
+ hidden-Visibility-Argument-Agda : Visibility-Argument-Agda
+ instance-Visibility-Argument-Agda : Visibility-Argument-Agda
-data Relevance : UU lzero where
- relevant irrelevant : Relevance
+data Relevance-Argument-Agda : UU lzero where
+ relevant-Relevance-Argument-Agda : Relevance-Argument-Agda
+ irrelevant-Relevance-Argument-Agda : Relevance-Argument-Agda
-data Quantity : UU lzero where
- quantity-0 quantity-Ο : Quantity
+data Quantity-Argument-Agda : UU lzero where
+ zero-Quantity-Argument-Agda : Quantity-Argument-Agda
+ omega-Quantity-Argument-Agda : Quantity-Argument-Agda
-data Modality : UU lzero where
- modality : (r : Relevance) (q : Quantity) β Modality
+data Modality-Argument-Agda : UU lzero where
+ cons-Modality-Argument-Agda :
+ Relevance-Argument-Agda β Quantity-Argument-Agda β Modality-Argument-Agda
-data ArgInfo : UU lzero where
- arg-info : (v : Visibility) (m : Modality) β ArgInfo
+data Info-Argument-Agda : UU lzero where
+ cons-Info-Argument-Agda :
+ Visibility-Argument-Agda β Modality-Argument-Agda β Info-Argument-Agda
-data Arg {l} (A : UU l) : UU l where
- arg : (i : ArgInfo) (x : A) β Arg A
+data Argument-Agda {l : Level} (A : UU l) : UU l where
+ cons-Argument-Agda : Info-Argument-Agda β A β Argument-Agda A
```
Bindings
```agda
-{-# BUILTIN HIDING Visibility #-}
-{-# BUILTIN VISIBLE visible #-}
-{-# BUILTIN HIDDEN hidden #-}
-{-# BUILTIN INSTANCE instanceβ² #-}
+{-# BUILTIN HIDING Visibility-Argument-Agda #-}
+{-# BUILTIN VISIBLE visible-Visibility-Argument-Agda #-}
+{-# BUILTIN HIDDEN hidden-Visibility-Argument-Agda #-}
+{-# BUILTIN INSTANCE instance-Visibility-Argument-Agda #-}
-{-# BUILTIN RELEVANCE Relevance #-}
-{-# BUILTIN RELEVANT relevant #-}
-{-# BUILTIN IRRELEVANT irrelevant #-}
+{-# BUILTIN RELEVANCE Relevance-Argument-Agda #-}
+{-# BUILTIN RELEVANT relevant-Relevance-Argument-Agda #-}
+{-# BUILTIN IRRELEVANT irrelevant-Relevance-Argument-Agda #-}
-{-# BUILTIN QUANTITY Quantity #-}
-{-# BUILTIN QUANTITY-0 quantity-0 #-}
-{-# BUILTIN QUANTITY-Ο quantity-Ο #-}
+{-# BUILTIN QUANTITY Quantity-Argument-Agda #-}
+{-# BUILTIN QUANTITY-0 zero-Quantity-Argument-Agda #-}
+{-# BUILTIN QUANTITY-Ο omega-Quantity-Argument-Agda #-}
-{-# BUILTIN MODALITY Modality #-}
-{-# BUILTIN MODALITY-CONSTRUCTOR modality #-}
+{-# BUILTIN MODALITY Modality-Argument-Agda #-}
+{-# BUILTIN MODALITY-CONSTRUCTOR cons-Modality-Argument-Agda #-}
-{-# BUILTIN ARGINFO ArgInfo #-}
-{-# BUILTIN ARGARGINFO arg-info #-}
+{-# BUILTIN ARGINFO Info-Argument-Agda #-}
+{-# BUILTIN ARGARGINFO cons-Info-Argument-Agda #-}
-{-# BUILTIN ARG Arg #-}
-{-# BUILTIN ARGARG arg #-}
+{-# BUILTIN ARG Argument-Agda #-}
+{-# BUILTIN ARGARG cons-Argument-Agda #-}
```
@@ -84,9 +90,23 @@ data Arg {l} (A : UU l) : UU l where
We create helper patterns for the two most common type of arguments.
```agda
--- visible-Arg : {l : Level} {A : UU l} β A β Arg A
-pattern visible-Arg t = arg (arg-info visible (modality relevant quantity-Ο)) t
-
--- hidden-Arg : {l : Level} {A : UU l} β A β Arg A
-pattern hidden-Arg t = arg (arg-info hidden (modality relevant quantity-Ο)) t
+-- visible-Argument-Agda : {l : Level} {A : UU l} β A β Argument-Agda A
+pattern visible-Argument-Agda t =
+ cons-Argument-Agda
+ ( cons-Info-Argument-Agda
+ ( visible-Visibility-Argument-Agda)
+ ( cons-Modality-Argument-Agda
+ ( relevant-Relevance-Argument-Agda)
+ ( omega-Quantity-Argument-Agda)))
+ ( t)
+
+-- hidden-Argument-Agda : {l : Level} {A : UU l} β A β Argument-Agda A
+pattern hidden-Argument-Agda t =
+ cons-Argument-Agda
+ ( cons-Info-Argument-Agda
+ ( hidden-Visibility-Argument-Agda)
+ ( cons-Modality-Argument-Agda
+ ( relevant-Relevance-Argument-Agda)
+ ( omega-Quantity-Argument-Agda)))
+ ( t)
```
diff --git a/src/reflection/definitions.lagda.md b/src/reflection/definitions.lagda.md
index 8f8d286846..1c98f22065 100644
--- a/src/reflection/definitions.lagda.md
+++ b/src/reflection/definitions.lagda.md
@@ -28,25 +28,31 @@ open import reflection.terms
## Idea
-The `Definition` type represents a definition in Agda.
+The `Definition-Agda` type represents a definition in Agda.
## Definition
```agda
-data Definition : UU lzero where
- function : (cs : list Clause) β Definition
- data-type : (pars : β) (cs : list Name) β Definition
- record-type : (c : Name) (fs : list (Arg Name)) β Definition
- data-cons : (d : Name) β Definition
- axiom : Definition
- prim-fun : Definition
-{-# BUILTIN AGDADEFINITION Definition #-}
-{-# BUILTIN AGDADEFINITIONFUNDEF function #-}
-{-# BUILTIN AGDADEFINITIONDATADEF data-type #-}
-{-# BUILTIN AGDADEFINITIONRECORDDEF record-type #-}
-{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR data-cons #-}
-{-# BUILTIN AGDADEFINITIONPOSTULATE axiom #-}
-{-# BUILTIN AGDADEFINITIONPRIMITIVE prim-fun #-}
+data Definition-Agda : UU lzero where
+ function-Definition-Agda : list Clause-Agda β Definition-Agda
+ data-type-Definition-Agda : β β list Name-Agda β Definition-Agda
+ record-type-Definition-Agda :
+ Name-Agda β list (Argument-Agda Name-Agda) β Definition-Agda
+ data-constructor-Definition-Agda : Name-Agda β Definition-Agda
+ postulate-Definition-Agda : Definition-Agda
+ primitive-function-Definition-Agda : Definition-Agda
+```
+
+## Bindings
+
+```agda
+{-# BUILTIN AGDADEFINITION Definition-Agda #-}
+{-# BUILTIN AGDADEFINITIONFUNDEF function-Definition-Agda #-}
+{-# BUILTIN AGDADEFINITIONDATADEF data-type-Definition-Agda #-}
+{-# BUILTIN AGDADEFINITIONRECORDDEF record-type-Definition-Agda #-}
+{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR data-constructor-Definition-Agda #-}
+{-# BUILTIN AGDADEFINITIONPOSTULATE postulate-Definition-Agda #-}
+{-# BUILTIN AGDADEFINITIONPRIMITIVE primitive-function-Definition-Agda #-}
```
## Examples
@@ -54,24 +60,25 @@ data Definition : UU lzero where
### Constructors and definitions
```agda
-_ : quoteTerm β οΌ def (quote β) nil
+_ : quoteTerm β οΌ definition-Term-Agda (quote β) nil
_ = refl
_ :
quoteTerm (succ-β zero-β) οΌ
- con
+ constructor-Term-Agda
( quote succ-β)
- ( unit-list (visible-Arg (con (quote zero-β) nil)))
+ ( unit-list
+ ( visible-Argument-Agda (constructor-Term-Agda (quote zero-β) nil)))
_ = refl
_ :
{l : Level} {A : UU l} β
quoteTerm (type-trunc-Prop A) οΌ
- def
+ definition-Term-Agda
( quote type-trunc-Prop)
( cons
- ( hidden-Arg (var 1 nil))
- ( unit-list (visible-Arg (var 0 nil))))
+ ( hidden-Argument-Agda (variable-Term-Agda 1 nil))
+ ( unit-list (visible-Argument-Agda (variable-Term-Agda 0 nil))))
_ = refl
```
@@ -79,12 +86,18 @@ _ = refl
```agda
_ :
- quoteTerm (Ξ» (x : β) β x) οΌ lam visible (abs "x" (var 0 nil))
+ quoteTerm (Ξ» (x : β) β x) οΌ
+ lambda-Term-Agda visible-Visibility-Argument-Agda
+ ( cons-Abstraction-Agda "x" (variable-Term-Agda 0 nil))
_ = refl
_ :
quoteTerm (Ξ» {x : β} (y : β) β x) οΌ
- lam hidden (abs "x" (lam visible (abs "y" (var 1 nil))))
+ lambda-Term-Agda hidden-Visibility-Argument-Agda
+ ( cons-Abstraction-Agda
+ ( "x")
+ ( lambda-Term-Agda visible-Visibility-Argument-Agda
+ ( cons-Abstraction-Agda "y" (variable-Term-Agda 1 nil))))
_ = refl
private
@@ -93,62 +106,71 @@ private
_ :
quoteTerm (helper (β β β) (Ξ» { zero-β β zero-β ; (succ-β x) β x})) οΌ
- def
+ definition-Term-Agda
( quote helper)
( cons
-- β β β
- ( visible-Arg
- ( pi
- ( visible-Arg (def (quote β) nil))
- ( abs "_" (def (quote β) nil))))
+ ( visible-Argument-Agda
+ ( dependent-product-Term-Agda
+ ( visible-Argument-Agda (definition-Term-Agda (quote β) nil))
+ ( cons-Abstraction-Agda "_" (definition-Term-Agda (quote β) nil))))
( unit-list
-- The pattern matching lambda
- ( visible-Arg
- ( pat-lam
+ ( visible-Argument-Agda
+ ( pattern-lambda-Term-Agda
( cons
- -- zero-β clause
- ( clause
+ -- zero-β clause-Clause-Agda
+ ( clause-Clause-Agda
-- No telescope
( nil)
-- Left side of the first lambda case
- ( unit-list (visible-Arg (con (quote zero-β) nil)))
+ ( unit-list
+ ( visible-Argument-Agda
+ ( constructor-Term-Agda (quote zero-β) nil)))
-- Right side of the first lambda case
- ( con (quote zero-β) nil))
+ ( constructor-Term-Agda (quote zero-β) nil))
( unit-list
- -- succ-β clause
- ( clause
- -- Telescope matching the "x"
- ( unit-list ("x" , visible-Arg (def (quote β) nil)))
+ -- succ-β clause-Clause-Agda
+ ( clause-Clause-Agda
+ -- Telescope-Agda matching the "x"
+ ( unit-list
+ ( "x" ,
+ visible-Argument-Agda
+ ( definition-Term-Agda (quote β) nil)))
-- Left side of the second lambda case
( unit-list
- ( visible-Arg
- ( con
+ ( visible-Argument-Agda
+ ( constructor-Term-Agda
( quote succ-β)
- ( unit-list ( visible-Arg (var 0))))))
+ ( unit-list
+ ( visible-Argument-Agda (variable-Term-Agda 0))))))
-- Right side of the second lambda case
- ( var 0 nil))))
+ ( variable-Term-Agda 0 nil))))
( nil)))))
_ = refl
_ :
quoteTerm (helper (empty β β) (Ξ» ())) οΌ
- def
+ definition-Term-Agda
( quote helper)
( cons
- ( visible-Arg
- ( pi (visible-Arg (def (quote empty) nil))
- ( abs "_" (def (quote β) nil))))
+ ( visible-Argument-Agda
+ ( dependent-product-Term-Agda
+ ( visible-Argument-Agda (definition-Term-Agda (quote empty) nil))
+ ( cons-Abstraction-Agda "_" (definition-Term-Agda (quote β) nil))))
( unit-list
- ( visible-Arg
+ ( visible-Argument-Agda
-- Lambda
- ( pat-lam
+ ( pattern-lambda-Term-Agda
( unit-list
- -- Clause
- ( absurd-clause
+ -- Clause-Agda
+ ( absurd-Clause-Agda
( unit-list
- ( "()" , visible-Arg (def (quote empty) nil)))
+ ( "()" ,
+ visible-Argument-Agda
+ ( definition-Term-Agda (quote empty) nil)))
( unit-list
- ( visible-Arg (absurd 0)))))
+ ( visible-Argument-Agda (absurd-Pattern-Agda 0)))))
( nil)))))
_ = refl
```
@@ -157,19 +179,19 @@ private
```agda
_ : quoteTerm (β β β) οΌ
- pi
- ( visible-Arg (def (quote β) nil))
- ( abs "_" (def (quote β) nil))
+ dependent-product-Term-Agda
+ ( visible-Argument-Agda (definition-Term-Agda (quote β) nil))
+ ( cons-Abstraction-Agda "_" (definition-Term-Agda (quote β) nil))
_ = refl
_ : quoteTerm ((x : β) β is-zero-β x) οΌ
- pi
- ( visible-Arg (def (quote β) nil))
- ( abs "x"
- ( def
+ dependent-product-Term-Agda
+ ( visible-Argument-Agda (definition-Term-Agda (quote β) nil))
+ ( cons-Abstraction-Agda "x"
+ ( definition-Term-Agda
( quote is-zero-β)
( cons
- ( visible-Arg (var 0 nil))
+ ( visible-Argument-Agda (variable-Term-Agda 0 nil))
( nil))))
_ = refl
```
@@ -177,22 +199,25 @@ _ = refl
### Universes
```agda
-_ : {l : Level} β quoteTerm (UU l) οΌ agda-sort (set (var 0 nil))
+_ :
+ {l : Level} β
+ quoteTerm (UU l) οΌ
+ sort-Term-Agda (universe-Sort-Agda (variable-Term-Agda 0 nil))
_ = refl
-_ : quoteTerm (UU (lsuc lzero)) οΌ agda-sort (lit 1)
+_ : quoteTerm (UU (lsuc lzero)) οΌ sort-Term-Agda (fixed-universe-Sort-Agda 1)
_ = refl
-_ : quoteTerm (UUΟ) οΌ agda-sort (inf 0)
+_ : quoteTerm (UUΟ) οΌ sort-Term-Agda (fixed-large-universe-Sort-Agda 0)
_ = refl
```
### Literals
```agda
-_ : quoteTerm 3 οΌ lit (nat 3)
+_ : quoteTerm 3 οΌ literal-Term-Agda (nat-Literal-Agda 3)
_ = refl
-_ : quoteTerm "hello" οΌ lit (string "hello")
+_ : quoteTerm "hello" οΌ literal-Term-Agda (string-Literal-Agda "hello")
_ = refl
```
diff --git a/src/reflection/fixity.lagda.md b/src/reflection/fixity.lagda.md
index 06b66421c0..52e0174190 100644
--- a/src/reflection/fixity.lagda.md
+++ b/src/reflection/fixity.lagda.md
@@ -30,40 +30,44 @@ The fixity of a quoted name is given by
## Definition
```agda
-data Associativity : UU lzero where
- left-associative : Associativity
- right-associative : Associativity
- nonassociative : Associativity
+data Associativity-Agda : UU lzero where
+ left-Associativity-Agda : Associativity-Agda
+ right-Associativity-Agda : Associativity-Agda
+ none-Associativity-Agda : Associativity-Agda
-data Precedence : UU lzero where
- related : Float β Precedence
- unrelated : Precedence
+data Precedence-Agda : UU lzero where
+ related-Precedence-Agda : Float β Precedence-Agda
+ unrelated-Precedence-Agda : Precedence-Agda
-data Fixity : UU lzero where
- fixity : Associativity β Precedence β Fixity
+data Fixity-Agda : UU lzero where
+ cons-Fixity-Agda : Associativity-Agda β Precedence-Agda β Fixity-Agda
-{-# BUILTIN ASSOC Associativity #-}
-{-# BUILTIN ASSOCLEFT left-associative #-}
-{-# BUILTIN ASSOCRIGHT right-associative #-}
-{-# BUILTIN ASSOCNON nonassociative #-}
+{-# BUILTIN ASSOC Associativity-Agda #-}
+{-# BUILTIN ASSOCLEFT left-Associativity-Agda #-}
+{-# BUILTIN ASSOCRIGHT right-Associativity-Agda #-}
+{-# BUILTIN ASSOCNON none-Associativity-Agda #-}
-{-# BUILTIN PRECEDENCE Precedence #-}
-{-# BUILTIN PRECRELATED related #-}
-{-# BUILTIN PRECUNRELATED unrelated #-}
+{-# BUILTIN PRECEDENCE Precedence-Agda #-}
+{-# BUILTIN PRECRELATED related-Precedence-Agda #-}
+{-# BUILTIN PRECUNRELATED unrelated-Precedence-Agda #-}
-{-# BUILTIN FIXITY Fixity #-}
-{-# BUILTIN FIXITYFIXITY fixity #-}
+{-# BUILTIN FIXITY Fixity-Agda #-}
+{-# BUILTIN FIXITYFIXITY cons-Fixity-Agda #-}
primitive
- primQNameFixity : Name β Fixity
+ primQNameFixity : Name-Agda β Fixity-Agda
```
## Examples
```agda
-_ : primQNameFixity (quote add-β€) οΌ fixity nonassociative unrelated
+_ :
+ primQNameFixity (quote add-β€) οΌ
+ cons-Fixity-Agda none-Associativity-Agda unrelated-Precedence-Agda
_ = refl
-_ : primQNameFixity (quote (_+β€_)) οΌ fixity left-associative (related 35.0)
+_ :
+ primQNameFixity (quote (_+β€_)) οΌ
+ cons-Fixity-Agda left-Associativity-Agda (related-Precedence-Agda 35.0)
_ = refl
```
diff --git a/src/reflection/group-solver.lagda.md b/src/reflection/group-solver.lagda.md
index 92cda445f2..c75a96bbe7 100644
--- a/src/reflection/group-solver.lagda.md
+++ b/src/reflection/group-solver.lagda.md
@@ -35,33 +35,33 @@ way and removes units and inverses next to the original.
The main entry-point is `solveExpr` below
```agda
-data Fin : β β UU lzero where
- zero-Fin : β {n} β Fin (succ-β n)
- succ-Fin : β {n} β Fin n β Fin (succ-β n)
-
-finEq : β {n} β (a b : Fin n) β is-decidable (Id a b)
-finEq zero-Fin zero-Fin = inl refl
-finEq zero-Fin (succ-Fin b) = inr (Ξ» ())
-finEq (succ-Fin a) zero-Fin = inr (Ξ» ())
-finEq (succ-Fin a) (succ-Fin b) with finEq a b
-... | inl eq = inl (ap succ-Fin eq)
+data Inductive-Fin : β β UU lzero where
+ zero-Inductive-Fin : {n : β} β Inductive-Fin (succ-β n)
+ succ-Inductive-Fin : {n : β} β Inductive-Fin n β Inductive-Fin (succ-β n)
+
+finEq : {n : β} β (a b : Inductive-Fin n) β is-decidable (Id a b)
+finEq zero-Inductive-Fin zero-Inductive-Fin = inl refl
+finEq zero-Inductive-Fin (succ-Inductive-Fin b) = inr (Ξ» ())
+finEq (succ-Inductive-Fin a) zero-Inductive-Fin = inr (Ξ» ())
+finEq (succ-Inductive-Fin a) (succ-Inductive-Fin b) with finEq a b
+... | inl eq = inl (ap succ-Inductive-Fin eq)
... | inr neq = inr (Ξ» where refl β neq refl)
-getVec : β {n} {l} {A : UU l} β vec A n β Fin n β A
-getVec (x β· v) zero-Fin = x
-getVec (x β· v) (succ-Fin k) = getVec v k
+getVec : {n : β} {l : Level} {A : UU l} β vec A n β Inductive-Fin n β A
+getVec (x β· v) zero-Inductive-Fin = x
+getVec (x β· v) (succ-Inductive-Fin k) = getVec v k
data GroupSyntax (n : β) : UU where
gUnit : GroupSyntax n
gMul : GroupSyntax n β GroupSyntax n β GroupSyntax n
gInv : GroupSyntax n β GroupSyntax n
- inner : Fin n β GroupSyntax n
+ inner : Inductive-Fin n β GroupSyntax n
data SimpleElem (n : β) : UU where
- inv-SE : Fin n β SimpleElem n
- pure-SE : Fin n β SimpleElem n
+ inv-SE : Inductive-Fin n β SimpleElem n
+ pure-SE : Inductive-Fin n β SimpleElem n
-inv-SE' : β {n} β SimpleElem n β SimpleElem n
+inv-SE' : {n : β} β SimpleElem n β SimpleElem n
inv-SE' (inv-SE k) = pure-SE k
inv-SE' (pure-SE k) = inv-SE k
@@ -106,96 +106,134 @@ module _ {n : β} where
data GroupEqualityElem : GroupSyntax n β GroupSyntax n β UU where
-- equivalence relation
- xsym-GE : β {x} {y} β GroupEqualityElem x y β GroupEqualityElem y x
+ xsym-GE :
+ {x y : GroupSyntax n} β GroupEqualityElem x y β GroupEqualityElem y x
-- Variations on ap
- -- xap-gMul : β {x} {y} {z} {w} β GroupEqualityElem x y β GroupEqualityElem z w β GroupEqualityElem (gMul x z) (gMul y w)
+ -- xap-gMul :
+ -- {x y z w : GroupSyntax n} β
+ -- GroupEqualityElem x y β GroupEqualityElem z w β
+ -- GroupEqualityElem (gMul x z) (gMul y w)
xap-gMul-l :
- β {x} {y} {z} β
+ {x y z : GroupSyntax n} β
GroupEqualityElem x y β GroupEqualityElem (gMul x z) (gMul y z)
xap-gMul-r :
- β {x} {y} {z} β
+ {x y z : GroupSyntax n} β
GroupEqualityElem y z β GroupEqualityElem (gMul x y) (gMul x z)
xap-gInv :
- β {x} {y} β
+ {x y : GroupSyntax n} β
GroupEqualityElem x y β GroupEqualityElem (gInv x) (gInv y)
-- Group laws
xassoc-GE :
- β x y z β GroupEqualityElem (gMul (gMul x y) z) (gMul x (gMul y z))
- xl-unit : β x β GroupEqualityElem (gMul gUnit x) x
- xr-unit : β x β GroupEqualityElem (gMul x gUnit) x
- xl-inv : β x β GroupEqualityElem (gMul (gInv x) x) gUnit
- xr-inv : β x β GroupEqualityElem (gMul x (gInv x)) gUnit
+ (x y z : GroupSyntax n) β
+ GroupEqualityElem (gMul (gMul x y) z) (gMul x (gMul y z))
+ xl-unit :
+ (x : GroupSyntax n) β GroupEqualityElem (gMul gUnit x) x
+ xr-unit :
+ (x : GroupSyntax n) β GroupEqualityElem (gMul x gUnit) x
+ xl-inv :
+ (x : GroupSyntax n) β GroupEqualityElem (gMul (gInv x) x) gUnit
+ xr-inv :
+ (x : GroupSyntax n) β GroupEqualityElem (gMul x (gInv x)) gUnit
-- Theorems that are provable from the others
- xinv-unit-GE : GroupEqualityElem (gInv gUnit) gUnit
- xinv-inv-GE : β x β GroupEqualityElem (gInv (gInv x)) x
+ xinv-unit-GE :
+ GroupEqualityElem (gInv gUnit) gUnit
+ xinv-inv-GE :
+ (x : GroupSyntax n) β GroupEqualityElem (gInv (gInv x)) x
xdistr-inv-mul-GE :
- β x y β GroupEqualityElem (gInv (gMul x y)) (gMul (gInv y) (gInv x))
+ (x y : GroupSyntax n) β
+ GroupEqualityElem (gInv (gMul x y)) (gMul (gInv y) (gInv x))
+
data GroupEquality : GroupSyntax n β GroupSyntax n β UU where
- refl-GE : β {x} β GroupEquality x x
+ refl-GE :
+ {x : GroupSyntax n} β GroupEquality x x
_β·GE_ :
- β {x} {y} {z} β
+ {x y z : GroupSyntax n} β
GroupEqualityElem x y β GroupEquality y z β GroupEquality x z
infixr 10 _β·GE_
module _ where
-- equivalence relation
- singleton-GE : β {x y} β GroupEqualityElem x y β GroupEquality x y
+ singleton-GE :
+ {x y : GroupSyntax n} β GroupEqualityElem x y β GroupEquality x y
singleton-GE x = x β·GE refl-GE
_βGE_ :
- β {x} {y} {z} β GroupEquality x y β GroupEquality y z β GroupEquality x z
+ {x y z : GroupSyntax n} β
+ GroupEquality x y β GroupEquality y z β GroupEquality x z
refl-GE βGE b = b
(x β·GE a) βGE b = x β·GE (a βGE b)
infixr 15 _βGE_
- sym-GE : β {x} {y} β GroupEquality x y β GroupEquality y x
+ sym-GE : {x y : GroupSyntax n} β GroupEquality x y β GroupEquality y x
sym-GE refl-GE = refl-GE
sym-GE (a β·GE as) = sym-GE as βGE singleton-GE (xsym-GE a)
-- Variations on ap
- ap-gInv : β {x} {y} β GroupEquality x y β GroupEquality (gInv x) (gInv y)
+ ap-gInv :
+ {x y : GroupSyntax n} β
+ GroupEquality x y β GroupEquality (gInv x) (gInv y)
ap-gInv refl-GE = refl-GE
ap-gInv (a β·GE as) = xap-gInv a β·GE ap-gInv as
+
ap-gMul-l :
- β {x} {y} {z} β GroupEquality x y β GroupEquality (gMul x z) (gMul y z)
+ {x y z : GroupSyntax n} β
+ GroupEquality x y β GroupEquality (gMul x z) (gMul y z)
ap-gMul-l refl-GE = refl-GE
ap-gMul-l (x β·GE xs) = xap-gMul-l x β·GE ap-gMul-l xs
+
ap-gMul-r :
- β {x} {y} {z} β GroupEquality y z β GroupEquality (gMul x y) (gMul x z)
+ {x y z : GroupSyntax n} β
+ GroupEquality y z β GroupEquality (gMul x y) (gMul x z)
ap-gMul-r refl-GE = refl-GE
ap-gMul-r (x β·GE xs) = xap-gMul-r x β·GE ap-gMul-r xs
+
ap-gMul :
- β {x} {y} {z} {w} β
+ {x y z w : GroupSyntax n} β
GroupEquality x y β GroupEquality z w β
GroupEquality (gMul x z) (gMul y w)
ap-gMul p q = ap-gMul-l p βGE ap-gMul-r q
-- Group laws
- assoc-GE : β x y z β GroupEquality (gMul (gMul x y) z) (gMul x (gMul y z))
+ assoc-GE :
+ (x y z : GroupSyntax n) β
+ GroupEquality (gMul (gMul x y) z) (gMul x (gMul y z))
assoc-GE x y z = singleton-GE (xassoc-GE x y z)
- l-unit : β x β GroupEquality (gMul gUnit x) x
+
+ l-unit :
+ (x : GroupSyntax n) β GroupEquality (gMul gUnit x) x
l-unit x = singleton-GE (xl-unit x)
- r-unit : β x β GroupEquality (gMul x gUnit) x
+
+ r-unit :
+ (x : GroupSyntax n) β GroupEquality (gMul x gUnit) x
r-unit x = singleton-GE (xr-unit x)
- l-inv : β x β GroupEquality (gMul (gInv x) x) gUnit
+
+ l-inv :
+ (x : GroupSyntax n) β GroupEquality (gMul (gInv x) x) gUnit
l-inv x = singleton-GE (xl-inv x)
- r-inv : β x β GroupEquality (gMul x (gInv x)) gUnit
+
+ r-inv :
+ (x : GroupSyntax n) β GroupEquality (gMul x (gInv x)) gUnit
r-inv x = singleton-GE (xr-inv x)
-- Theorems that are provable from the others
inv-unit-GE : GroupEquality (gInv gUnit) gUnit
inv-unit-GE = singleton-GE (xinv-unit-GE)
- inv-inv-GE : β x β GroupEquality (gInv (gInv x)) x
+
+ inv-inv-GE : (x : GroupSyntax n) β GroupEquality (gInv (gInv x)) x
inv-inv-GE x = singleton-GE (xinv-inv-GE x)
+
distr-inv-mul-GE :
- β x y β GroupEquality (gInv (gMul x y)) (gMul (gInv y) (gInv x))
+ (x y : GroupSyntax n) β
+ GroupEquality (gInv (gMul x y)) (gMul (gInv y) (gInv x))
distr-inv-mul-GE x y = singleton-GE (xdistr-inv-mul-GE x y)
- assoc-GE' : β x y z β GroupEquality (gMul x (gMul y z)) (gMul (gMul x y) z)
+ assoc-GE' :
+ (x y z : GroupSyntax n) β
+ GroupEquality (gMul x (gMul y z)) (gMul (gMul x y) z)
assoc-GE' x y z = sym-GE (assoc-GE x y z)
elim-inverses-remove-valid :
@@ -239,7 +277,7 @@ module _ {n : β} where
elim-inverses-valid x (elim-inverses y (concat-simplify a b))
concat-simplify-valid :
- β (u w : Simple n) β
+ (u w : Simple n) β
GroupEquality
( gMul (unquoteSimple w) (unquoteSimple u))
( unquoteSimple (concat-simplify u w))
@@ -247,7 +285,7 @@ module _ {n : β} where
concat-simplify-valid (cons x a) b = concat-simplify-nonempty-valid x a b
inv-single-valid :
- β w β
+ (w : SimpleElem n) β
GroupEquality
( gInv (unquoteSimpleElem w))
( unquoteSimpleElem (inv-SE' w))
@@ -280,7 +318,7 @@ module _ {n : β} where
( unquoteSimple (concat-list xs (cons x nil)))
gMul-concat-1 xs a = gMul-concat' xs (cons a nil)
- -- inv-simplify-valid'-nonempty : β (x : SimpleElem n) (xs : list (SimpleElem n)) β
+ -- inv-simplify-valid'-nonempty : (x : SimpleElem n) (xs : list (SimpleElem n)) β
-- GroupEquality (gInv (unquoteSimple (cons x xs)))
-- (unquoteSimple (reverse-list (map-list inv-SE' (cons x xs))))
-- inv-simplify-valid'-nonempty x nil = inv-single-valid x
@@ -289,14 +327,14 @@ module _ {n : β} where
-- ap-gMul (inv-single-valid x) (inv-simplify-valid'-nonempty y xs) βGE
-- gMul-concat-1 (concat-list (reverse-list (map-list inv-SE' xs)) (in-list (inv-SE' y))) (inv-SE' x)
- -- inv-simplify-valid' : β (w : list (SimpleElem n)) β
+ -- inv-simplify-valid' : (w : list (SimpleElem n)) β
-- GroupEquality (gInv (unquoteSimple w))
-- (unquoteSimple (reverse-list (map-list inv-SE' w)))
-- inv-simplify-valid' nil = inv-unit-GE
-- inv-simplify-valid' (cons x xs) =
-- inv-simplify-valid'-nonempty x xs
- -- simplifyValid : β (g : GroupSyntax n) β GroupEquality g (unquoteSimple (simplifyGS g))
+ -- simplifyValid : (g : GroupSyntax n) β GroupEquality g (unquoteSimple (simplifyGS g))
-- simplifyValid gUnit = refl-GE
-- simplifyValid (gMul a b) =
-- (ap-gMul (simplifyValid a) (simplifyValid b)) βGE
@@ -304,14 +342,14 @@ module _ {n : β} where
-- simplifyValid (gInv g) = ap-gInv (simplifyValid g) βGE inv-simplify-valid' (simplifyGS g)
-- simplifyValid (inner _) = refl-GE
- Env : β {l} β β β UU l β UU l
+ Env : {l : Level} β β β UU l β UU l
Env n A = vec A n
module _
{l : Level} (G : Group l)
where
- unQuoteGS : β {n} β GroupSyntax n β Env n (type-Group G) β type-Group G
+ unQuoteGS : {n : β} β GroupSyntax n β Env n (type-Group G) β type-Group G
unQuoteGS gUnit e = unit-Group G
unQuoteGS (gMul x y) e = mul-Group G (unQuoteGS x e) (unQuoteGS y e)
unQuoteGS (gInv x) e = inv-Group G (unQuoteGS x e)
@@ -357,7 +395,7 @@ module _ {n : β} where
useGroupEqualityElem env x β useGroupEquality env xs
-- simplifyExpression :
- -- β (g : GroupSyntax n) (env : Env n (type-Group G)) β
+ -- (g : GroupSyntax n) (env : Env n (type-Group G)) β
-- unQuoteGS g env οΌ unQuoteGS (unquoteSimple (simplifyGS g)) env
-- simplifyExpression g env = useGroupEquality env (simplifyValid g)
@@ -366,46 +404,50 @@ module _ {n : β} where
n-args zero-β A B = B
n-args (succ-β n) A B = A β n-args n A B
map-n-args :
- β {A A' B : UU} (n : β) β (A' β A) β n-args n A B β n-args n A' B
+ {A A' B : UU} (n : β) β (A' β A) β n-args n A B β n-args n A' B
map-n-args zero-β f v = v
map-n-args (succ-β n) f v = Ξ» x β map-n-args n f (v (f x))
- apply-n-args-fin : β {B : UU} (n : β) β n-args n (Fin n) B β B
+ apply-n-args-fin : {B : UU} (n : β) β n-args n (Inductive-Fin n) B β B
apply-n-args-fin zero-β f = f
apply-n-args-fin (succ-β n) f =
- apply-n-args-fin n (map-n-args n succ-Fin (f zero-Fin))
- apply-n-args : β {B : UU} (n : β) β n-args n (GroupSyntax n) B β B
+ apply-n-args-fin
+ ( n)
+ ( map-n-args n succ-Inductive-Fin (f zero-Inductive-Fin))
+ apply-n-args : {B : UU} (n : β) β n-args n (GroupSyntax n) B β B
apply-n-args n f = apply-n-args-fin n (map-n-args n inner f)
-- A variation of simplifyExpression which takes a function from the free variables to expr
-- simplifyExpr :
- -- β (env : Env n (type-Group G)) (g : n-args n (GroupSyntax n) (GroupSyntax n)) β
+ -- (env : Env n (type-Group G)) (g : n-args n (GroupSyntax n) (GroupSyntax n)) β
-- unQuoteGS (apply-n-args n g) env οΌ unQuoteGS (unquoteSimple (simplifyGS (apply-n-args n g))) env
-- simplifyExpr env g = simplifyExpression (apply-n-args n g) env
-
- open import linear-algebra.vectors using (_β·_ ; empty-vec) public
```
-```agda
--- private _\*'_ : β {n} β GroupSyntax n β GroupSyntax n β GroupSyntax n _\*'_ =
--- gMul x : GroupSyntax 2 x = inner (zero-Fin) y : GroupSyntax 2 y = inner
--- (succ-Fin zero-Fin)
-
--- infixl 40 _*'_
--- ex1 : GroupEquality {n = 2} (gInv (x *' y *' gInv x *' gInv y)) (y *' x *' gInv y *' gInv x)
--- ex1 = simplifyValid _
-
--- ex2 : β x y β (x * y * x β»ΒΉ * y β»ΒΉ) β»ΒΉ οΌ (y * x * y β»ΒΉ * x β»ΒΉ)
--- ex2 x' y' = simplifyExpression (gInv (x *' y *' gInv x *' gInv y)) (x' β· y' β· empty-vec)
-
--- _ : UU
--- -- _ = {!simplifyValid (y *' (x *' (gInv y *' (gInv x *' gUnit))))!}
--- _ = {!ex1!}
-
--- ex3 : β x y β (x * y) β»ΒΉ οΌ (y β»ΒΉ * x β»ΒΉ)
--- ex3 x' y' = {!simplifyExpression (gInv (x *' y)) (x' β· y' β· empty-vec)!}
-
--- _ : GroupEquality {n = 2} (y *' (x *' (gInv y *' (gInv x *' gUnit)))) (y *' (x *' (gInv y *' (gInv x *' gUnit))))
--- _ = {!simplifyValid (gInv x *' x *' y)!}
--- -- _ = {!simplifyValid (gUnit *' gUnit)!}
--- -- _ = {!simplifyValid (x *' gUnit)!}
+```text
+private
+ _*'_ : {n : β} β GroupSyntax n β GroupSyntax n β GroupSyntax n
+ _*'_ = gMul
+ x : GroupSyntax 2
+ x = inner (zero-Inductive-Fin)
+ y : GroupSyntax 2
+ y = inner (succ-Inductive-Fin zero-Inductive-Fin)
+
+ infixl 40 _*'_
+ ex1 : GroupEquality {n = 2} (gInv (x *' y *' gInv x *' gInv y)) (y *' x *' gInv y *' gInv x)
+ ex1 = simplifyValid _
+
+ ex2 : β x y β (x * y * x β»ΒΉ * y β»ΒΉ) β»ΒΉ οΌ (y * x * y β»ΒΉ * x β»ΒΉ)
+ ex2 x' y' = simplifyExpression (gInv (x *' y *' gInv x *' gInv y)) (x' β· y' β· empty-vec)
+
+ _ : UU
+ -- _ = {!simplifyValid (y *' (x *' (gInv y *' (gInv x *' gUnit))))!}
+ _ = {!ex1!}
+
+ ex3 : β x y β (x * y) β»ΒΉ οΌ (y β»ΒΉ * x β»ΒΉ)
+ ex3 x' y' = {!simplifyExpression (gInv (x *' y)) (x' β· y' β· empty-vec)!}
+
+ _ : GroupEquality {n = 2} (y *' (x *' (gInv y *' (gInv x *' gUnit)))) (y *' (x *' (gInv y *' (gInv x *' gUnit))))
+ _ = {!simplifyValid (gInv x *' x *' y)!}
+ -- _ = {!simplifyValid (gUnit *' gUnit)!}
+ -- _ = {!simplifyValid (x *' gUnit)!}
```
diff --git a/src/reflection/literals.lagda.md b/src/reflection/literals.lagda.md
index 106f2bf0a8..a5d3233f19 100644
--- a/src/reflection/literals.lagda.md
+++ b/src/reflection/literals.lagda.md
@@ -24,7 +24,7 @@ open import reflection.names
## Idea
-The `Literal` type represents literals in Agda.
+The `Literal-Agda` type represents literals in Agda.
For concrete examples, see
[`reflection.definitions`](reflection.definitions.md).
@@ -32,21 +32,25 @@ For concrete examples, see
## Definition
```agda
-data Literal : UU lzero where
- nat : (n : β) β Literal
- word64 : (n : Word64) β Literal
- float : (x : Float) β Literal
- char : (c : Char) β Literal
- string : (s : String) β Literal
- name : (x : Name) β Literal
- meta : (x : Meta) β Literal
-
-{-# BUILTIN AGDALITERAL Literal #-}
-{-# BUILTIN AGDALITNAT nat #-}
-{-# BUILTIN AGDALITWORD64 word64 #-}
-{-# BUILTIN AGDALITFLOAT float #-}
-{-# BUILTIN AGDALITCHAR char #-}
-{-# BUILTIN AGDALITSTRING string #-}
-{-# BUILTIN AGDALITQNAME name #-}
-{-# BUILTIN AGDALITMETA meta #-}
+data Literal-Agda : UU lzero where
+ nat-Literal-Agda : β β Literal-Agda
+ word64-Literal-Agda : Word64 β Literal-Agda
+ float-Literal-Agda : Float β Literal-Agda
+ char-Literal-Agda : Char β Literal-Agda
+ string-Literal-Agda : String β Literal-Agda
+ quoted-name-Literal-Agda : Name-Agda β Literal-Agda
+ metavariable-Literal-Agda : Metavariable-Agda β Literal-Agda
+```
+
+## Bindings
+
+```agda
+{-# BUILTIN AGDALITERAL Literal-Agda #-}
+{-# BUILTIN AGDALITNAT nat-Literal-Agda #-}
+{-# BUILTIN AGDALITWORD64 word64-Literal-Agda #-}
+{-# BUILTIN AGDALITFLOAT float-Literal-Agda #-}
+{-# BUILTIN AGDALITCHAR char-Literal-Agda #-}
+{-# BUILTIN AGDALITSTRING string-Literal-Agda #-}
+{-# BUILTIN AGDALITQNAME quoted-name-Literal-Agda #-}
+{-# BUILTIN AGDALITMETA metavariable-Literal-Agda #-}
```
diff --git a/src/reflection/metavariables.lagda.md b/src/reflection/metavariables.lagda.md
index 3cbe04810a..17e3ac21c1 100644
--- a/src/reflection/metavariables.lagda.md
+++ b/src/reflection/metavariables.lagda.md
@@ -22,30 +22,35 @@ open import primitives.strings
## Idea
-The `Meta` type represents metavariables in Agda.
+The `Metavariable-Agda` type represents metavariables in Agda.
## Definition
```agda
postulate
- Meta : UU lzero
+ Metavariable-Agda : UU lzero
-{-# BUILTIN AGDAMETA Meta #-}
+{-# BUILTIN AGDAMETA Metavariable-Agda #-}
primitive
- primMetaEquality : Meta β Meta β bool
- primMetaLess : Meta β Meta β bool
- primShowMeta : Meta β String
- primMetaToNat : Meta β β
- primMetaToNatInjective : β a b β primMetaToNat a οΌ primMetaToNat b β a οΌ b
-
-data Blocker : UU lzero where
- blocker-any : list Blocker β Blocker
- blocker-all : list Blocker β Blocker
- blocker-meta : Meta β Blocker
-
-{-# BUILTIN AGDABLOCKER Blocker #-}
-{-# BUILTIN AGDABLOCKERANY blocker-any #-}
-{-# BUILTIN AGDABLOCKERALL blocker-all #-}
-{-# BUILTIN AGDABLOCKERMETA blocker-meta #-}
+ primMetaEquality :
+ Metavariable-Agda β Metavariable-Agda β bool
+ primMetaLess :
+ Metavariable-Agda β Metavariable-Agda β bool
+ primShowMeta :
+ Metavariable-Agda β String
+ primMetaToNat :
+ Metavariable-Agda β β
+ primMetaToNatInjective :
+ (a b : Metavariable-Agda) β primMetaToNat a οΌ primMetaToNat b β a οΌ b
+
+data Blocker-Agda : UU lzero where
+ any-Blocker-Agda : list Blocker-Agda β Blocker-Agda
+ all-Blocker-Agda : list Blocker-Agda β Blocker-Agda
+ metavariable-Blocker-Agda : Metavariable-Agda β Blocker-Agda
+
+{-# BUILTIN AGDABLOCKER Blocker-Agda #-}
+{-# BUILTIN AGDABLOCKERANY any-Blocker-Agda #-}
+{-# BUILTIN AGDABLOCKERALL all-Blocker-Agda #-}
+{-# BUILTIN AGDABLOCKERMETA metavariable-Blocker-Agda #-}
```
diff --git a/src/reflection/names.lagda.md b/src/reflection/names.lagda.md
index d6420e89fd..8b971a32c0 100644
--- a/src/reflection/names.lagda.md
+++ b/src/reflection/names.lagda.md
@@ -21,26 +21,26 @@ open import primitives.strings
## Idea
-The `Name` type represents quoted names, i.e. they are an abstract syntactic
-representation of terms. Agda provides primitive functions to manipulate them,
-giving them an equality and ordering. A closed term can be converted to a quoted
-name by means of the `quote` keyword, e.g. `quote bool`.
+The `Name-Agda` type represents quoted names, i.e. they are an abstract
+syntactic representation of terms. Agda provides primitive functions to
+manipulate them, giving them an equality and ordering. A closed term can be
+converted to a quoted name by means of the `quote` keyword, e.g. `quote bool`.
## Definition
```agda
postulate
- Name : UU lzero
+ Name-Agda : UU lzero
-{-# BUILTIN QNAME Name #-}
+{-# BUILTIN QNAME Name-Agda #-}
primitive
- primQNameEquality : Name β Name β bool
- primQNameLess : Name β Name β bool
- primShowQName : Name β String
- primQNameToWord64s : Name β Word64 Γ Word64
+ primQNameEquality : Name-Agda β Name-Agda β bool
+ primQNameLess : Name-Agda β Name-Agda β bool
+ primShowQName : Name-Agda β String
+ primQNameToWord64s : Name-Agda β Word64 Γ Word64
primQNameToWord64sInjective :
- β a b β primQNameToWord64s a οΌ primQNameToWord64s b β a οΌ b
+ (a b : Name-Agda) β primQNameToWord64s a οΌ primQNameToWord64s b β a οΌ b
```
## Examples
diff --git a/src/reflection/precategory-solver.lagda.md b/src/reflection/precategory-solver.lagda.md
index 95f866533d..c0d90a380a 100644
--- a/src/reflection/precategory-solver.lagda.md
+++ b/src/reflection/precategory-solver.lagda.md
@@ -34,16 +34,16 @@ This module defines a macro, `solve-Precategory!` that solves any equation
between morphisms of a precategory, as long as it's derivable from the axioms of
precategories.
-To do this, we introduce the type `Precategory-Expr`, which is a syntactic
+To do this, we introduce the type `Precategory-Expression`, which is a syntactic
representation of a morphism. Then, noting that every morphism is represented by
-an expression (through `in-Precategory-Expr`), it will be sufficient to prove an
-equality of expresions to prove an equality of morphisms. However, if two
-morphisms are equal, then their normalized expressions are equal by reflexivity,
-so that the problem is reduced to finding which `Precategory-Expr` represents a
-given morphism.
+an expression (through `in-Precategory-Expression`), it will be sufficient to
+prove an equality of expresions to prove an equality of morphisms. However, if
+two morphisms are equal, then their normalized expressions are equal by
+reflexivity, so that the problem is reduced to finding which
+`Precategory-Expression` represents a given morphism.
-This last problem, as well as the application of the `solve-Precategory-Expr`
-lemma, is what the macro automates.
+This last problem, as well as the application of the
+`solve-Precategory-Expression` lemma, is what the macro automates.
## Definition
@@ -56,109 +56,95 @@ module _
where
data
- Precategory-Expr :
+ Precategory-Expression :
obj-Precategory C β obj-Precategory C β UU (l1 β l2)
where
- id-hom-Precategory-Expr :
- {x : obj-Precategory C} β Precategory-Expr x x
- hom-Precategory-Expr :
+ id-hom-Precategory-Expression :
+ {x : obj-Precategory C} β Precategory-Expression x x
+ hom-Precategory-Expression :
{x y : obj-Precategory C} β
- hom-Precategory C x y β Precategory-Expr x y
- comp-hom-Precategory-Expr :
+ hom-Precategory C x y β Precategory-Expression x y
+ comp-hom-Precategory-Expression :
{x y z : obj-Precategory C} β
- Precategory-Expr y z β Precategory-Expr x y β Precategory-Expr x z
+ Precategory-Expression y z β
+ Precategory-Expression x y β
+ Precategory-Expression x z
```
### The syntactic representation of a morphism
```agda
- in-Precategory-Expr :
+ in-Precategory-Expression :
{x y : obj-Precategory C} β
- Precategory-Expr x y β
+ Precategory-Expression x y β
hom-Precategory C x y
- in-Precategory-Expr id-hom-Precategory-Expr = id-hom-Precategory C
- in-Precategory-Expr (hom-Precategory-Expr f) = f
- in-Precategory-Expr (comp-hom-Precategory-Expr f g) =
- comp-hom-Precategory C (in-Precategory-Expr f) (in-Precategory-Expr g)
+ in-Precategory-Expression id-hom-Precategory-Expression = id-hom-Precategory C
+ in-Precategory-Expression (hom-Precategory-Expression f) = f
+ in-Precategory-Expression (comp-hom-Precategory-Expression f g) =
+ comp-hom-Precategory C
+ ( in-Precategory-Expression f)
+ ( in-Precategory-Expression g)
```
### The normalization of the syntactic representation of a morphism
```agda
- eval-Precategory-Expr :
+ eval-Precategory-Expression :
{x y z : obj-Precategory C} β
- Precategory-Expr y z β
+ Precategory-Expression y z β
hom-Precategory C x y β
hom-Precategory C x z
- eval-Precategory-Expr id-hom-Precategory-Expr f = f
- eval-Precategory-Expr (hom-Precategory-Expr f) g =
+ eval-Precategory-Expression id-hom-Precategory-Expression f = f
+ eval-Precategory-Expression (hom-Precategory-Expression f) g =
comp-hom-Precategory C f g
- eval-Precategory-Expr (comp-hom-Precategory-Expr f g) h =
- eval-Precategory-Expr f (eval-Precategory-Expr g h)
+ eval-Precategory-Expression (comp-hom-Precategory-Expression f g) h =
+ eval-Precategory-Expression f (eval-Precategory-Expression g h)
- is-sound-eval-Precategory-Expr :
+ is-sound-eval-Precategory-Expression :
{x y z : obj-Precategory C}
- (e : Precategory-Expr y z)
+ (e : Precategory-Expression y z)
(f : hom-Precategory C x y) β
- ( eval-Precategory-Expr e f) οΌ
- ( comp-hom-Precategory C (in-Precategory-Expr e) f)
- is-sound-eval-Precategory-Expr id-hom-Precategory-Expr f =
+ ( eval-Precategory-Expression e f) οΌ
+ ( comp-hom-Precategory C (in-Precategory-Expression e) f)
+ is-sound-eval-Precategory-Expression id-hom-Precategory-Expression f =
inv (left-unit-law-comp-hom-Precategory C f)
- is-sound-eval-Precategory-Expr (hom-Precategory-Expr f) g = refl
- is-sound-eval-Precategory-Expr (comp-hom-Precategory-Expr f g) h =
- equational-reasoning
- eval-Precategory-Expr f (eval-Precategory-Expr g h)
- οΌ comp-hom-Precategory C
- ( in-Precategory-Expr f)
- ( eval-Precategory-Expr g h)
- by is-sound-eval-Precategory-Expr f (eval-Precategory-Expr g h)
- οΌ comp-hom-Precategory C
- ( in-Precategory-Expr f)
- ( comp-hom-Precategory C (in-Precategory-Expr g) h)
- by ap
- ( comp-hom-Precategory C (in-Precategory-Expr f))
- ( is-sound-eval-Precategory-Expr g h)
- οΌ comp-hom-Precategory C
- ( comp-hom-Precategory C
- ( in-Precategory-Expr f)
- ( in-Precategory-Expr g))
- h
- by
- inv
- ( associative-comp-hom-Precategory
- C (in-Precategory-Expr f) (in-Precategory-Expr g) h)
-
- normalize-Precategory-Expr :
+ is-sound-eval-Precategory-Expression (hom-Precategory-Expression f) g = refl
+ is-sound-eval-Precategory-Expression (comp-hom-Precategory-Expression f g) h =
+ ( is-sound-eval-Precategory-Expression
+ ( f)
+ ( eval-Precategory-Expression g h)) β
+ ( ap
+ ( comp-hom-Precategory C (in-Precategory-Expression f))
+ ( is-sound-eval-Precategory-Expression g h)) β
+ ( inv
+ ( associative-comp-hom-Precategory
+ C (in-Precategory-Expression f) (in-Precategory-Expression g) h))
+
+ normalize-Precategory-Expression :
{x y : obj-Precategory C} β
- Precategory-Expr x y β
+ Precategory-Expression x y β
hom-Precategory C x y
- normalize-Precategory-Expr e = eval-Precategory-Expr e (id-hom-Precategory C)
+ normalize-Precategory-Expression e =
+ eval-Precategory-Expression e (id-hom-Precategory C)
- is-sound-normalize-Precategory-Expr :
+ is-sound-normalize-Precategory-Expression :
{x y : obj-Precategory C} β
- (e : Precategory-Expr x y) β
- normalize-Precategory-Expr e οΌ in-Precategory-Expr e
- is-sound-normalize-Precategory-Expr e = equational-reasoning
- eval-Precategory-Expr e (id-hom-Precategory C)
- οΌ comp-hom-Precategory C (in-Precategory-Expr e) (id-hom-Precategory C)
- by is-sound-eval-Precategory-Expr e (id-hom-Precategory C)
- οΌ in-Precategory-Expr e
- by right-unit-law-comp-hom-Precategory C (in-Precategory-Expr e)
+ (e : Precategory-Expression x y) β
+ normalize-Precategory-Expression e οΌ in-Precategory-Expression e
+ is-sound-normalize-Precategory-Expression e =
+ ( is-sound-eval-Precategory-Expression e (id-hom-Precategory C)) β
+ ( right-unit-law-comp-hom-Precategory C (in-Precategory-Expression e))
abstract
- solve-Precategory-Expr :
+ solve-Precategory-Expression :
{x y : obj-Precategory C} β
- (f g : Precategory-Expr x y) β
- normalize-Precategory-Expr f οΌ normalize-Precategory-Expr g β
- in-Precategory-Expr f οΌ in-Precategory-Expr g
- solve-Precategory-Expr f g p = equational-reasoning
- in-Precategory-Expr f
- οΌ normalize-Precategory-Expr f
- by inv (is-sound-normalize-Precategory-Expr f)
- οΌ normalize-Precategory-Expr g
- by p
- οΌ in-Precategory-Expr g
- by is-sound-normalize-Precategory-Expr g
+ (f g : Precategory-Expression x y) β
+ normalize-Precategory-Expression f οΌ normalize-Precategory-Expression g β
+ in-Precategory-Expression f οΌ in-Precategory-Expression g
+ solve-Precategory-Expression f g p =
+ ( inv (is-sound-normalize-Precategory-Expression f)) β
+ ( p) β
+ ( is-sound-normalize-Precategory-Expression g)
```
## The macro definition
@@ -174,73 +160,76 @@ private
infixr 10 _++_
pattern apply-pr1 xs =
- def (quote pr1)
- ( hidden-Arg unknown β·
- hidden-Arg unknown β·
- hidden-Arg unknown β·
- hidden-Arg unknown β·
+ definition-Term-Agda (quote pr1)
+ ( hidden-Argument-Agda unknown-Term-Agda β·
+ hidden-Argument-Agda unknown-Term-Agda β·
+ hidden-Argument-Agda unknown-Term-Agda β·
+ hidden-Argument-Agda unknown-Term-Agda β·
xs)
pattern apply-pr2 xs =
- def (quote pr2)
- ( hidden-Arg unknown β·
- hidden-Arg unknown β·
- hidden-Arg unknown β·
- hidden-Arg unknown β·
+ definition-Term-Agda (quote pr2)
+ ( hidden-Argument-Agda unknown-Term-Agda β·
+ hidden-Argument-Agda unknown-Term-Agda β·
+ hidden-Argument-Agda unknown-Term-Agda β·
+ hidden-Argument-Agda unknown-Term-Agda β·
xs)
```
-### Building a term of `Precategory-Expr C x y` from a term of type `hom-Precategory C x y`
+### Building a term of `Precategory-Expression C x y` from a term of type `hom-Precategory C x y`
```agda
-build-Precategory-Expr : Term β Term
-build-Precategory-Expr
+build-Precategory-Expression : Term-Agda β Term-Agda
+build-Precategory-Expression
( apply-pr1
- ( visible-Arg
+ ( visible-Argument-Agda
( apply-pr2
- ( visible-Arg
+ ( visible-Argument-Agda
( apply-pr2
- ( visible-Arg
- ( apply-pr2 (visible-Arg C β· nil)) β·
+ ( visible-Argument-Agda
+ ( apply-pr2 (visible-Argument-Agda C β· nil)) β·
( nil))) β·
( nil))) β·
- ( visible-Arg x) β·
+ ( visible-Argument-Agda x) β·
nil)) =
- con (quote id-hom-Precategory-Expr) nil
-build-Precategory-Expr
+ constructor-Term-Agda (quote id-hom-Precategory-Expression) nil
+build-Precategory-Expression
( apply-pr1
- ( visible-Arg
+ ( visible-Argument-Agda
( apply-pr1
- ( visible-Arg
+ ( visible-Argument-Agda
( apply-pr2
- ( visible-Arg
+ ( visible-Argument-Agda
( apply-pr2
- (visible-Arg C β· nil)) β· nil))
+ (visible-Argument-Agda C β· nil)) β· nil))
β· nil)) β·
- hidden-Arg x β· hidden-Arg y β· hidden-Arg z β·
- visible-Arg g β· visible-Arg f β· nil)) =
- con
- ( quote comp-hom-Precategory-Expr)
- ( visible-Arg (build-Precategory-Expr g) β·
- visible-Arg (build-Precategory-Expr f) β·
+ hidden-Argument-Agda x β· hidden-Argument-Agda y β· hidden-Argument-Agda z β·
+ visible-Argument-Agda g β· visible-Argument-Agda f β· nil)) =
+ constructor-Term-Agda
+ ( quote comp-hom-Precategory-Expression)
+ ( visible-Argument-Agda (build-Precategory-Expression g) β·
+ visible-Argument-Agda (build-Precategory-Expression f) β·
nil)
-build-Precategory-Expr f =
- con (quote hom-Precategory-Expr) (visible-Arg f β· nil)
+build-Precategory-Expression f =
+ constructor-Term-Agda
+ ( quote hom-Precategory-Expression)
+ ( visible-Argument-Agda f β· nil)
```
-### The application of the `solve-Precategory-Expr` lemma
+### The application of the `solve-Precategory-Expression` lemma
```agda
-apply-solve-Precategory-Expr : Term β Term β Term β Term
-apply-solve-Precategory-Expr cat lhs rhs =
- def
- ( quote solve-Precategory-Expr)
- ( replicate-hidden-Arg 2 ++
- visible-Arg cat β·
- replicate-hidden-Arg 2 ++
- visible-Arg lhs β·
- visible-Arg rhs β·
- visible-Arg (con (quote refl) nil) β·
+apply-solve-Precategory-Expression :
+ Term-Agda β Term-Agda β Term-Agda β Term-Agda
+apply-solve-Precategory-Expression cat lhs rhs =
+ definition-Term-Agda
+ ( quote solve-Precategory-Expression)
+ ( replicate-hidden-Argument-Agda 2 ++
+ visible-Argument-Agda cat β·
+ replicate-hidden-Argument-Agda 2 ++
+ visible-Argument-Agda lhs β·
+ visible-Argument-Agda rhs β·
+ visible-Argument-Agda (constructor-Term-Agda (quote refl) nil) β·
nil)
```
@@ -248,13 +237,15 @@ apply-solve-Precategory-Expr cat lhs rhs =
```agda
macro
- solve-Precategory! : Term β Term β TC unit
+ solve-Precategory! : Term-Agda β Term-Agda β type-Type-Checker unit
solve-Precategory! cat hole = do
- goal β inferType hole >>= reduce
- (lhs , rhs) β boundary-TCM goal
- built-lhs β normalise lhs >>= (returnTC β build-Precategory-Expr)
- built-rhs β normalise rhs >>= (returnTC β build-Precategory-Expr)
- unify hole (apply-solve-Precategory-Expr cat built-lhs built-rhs)
+ goal β infer-type hole >>= reduce
+ (lhs , rhs) β boundary-Type-Checker goal
+ built-lhs β
+ normalize lhs >>= (return-Type-Checker β build-Precategory-Expression)
+ built-rhs β
+ normalize rhs >>= (return-Type-Checker β build-Precategory-Expression)
+ unify hole (apply-solve-Precategory-Expression cat built-lhs built-rhs)
```
## Examples
diff --git a/src/reflection/terms.lagda.md b/src/reflection/terms.lagda.md
index 7beeb3ecc4..5a823a2be2 100644
--- a/src/reflection/terms.lagda.md
+++ b/src/reflection/terms.lagda.md
@@ -28,9 +28,9 @@ open import reflection.names
## Idea
In this module we represent the terms of agda by an inductive definition of the
-type `Term`. See the comments for details on the constructors.
+type `Term-Agda`. See the comments for details on the constructors.
-We can obtain a `Term` from an agda term through the keyword `quoteTerm`.
+We can obtain a `Term-Agda` from an agda term through the keyword `quoteTerm`.
For concrete examples, see
[`reflection.definitions`](reflection.definitions.md).
@@ -38,107 +38,113 @@ For concrete examples, see
## Definition
```agda
-data Term : UU lzero
-data Sort : UU lzero
-data Pattern : UU lzero
-data Clause : UU lzero
-Telescope = list (String Γ Arg Term)
+data Term-Agda : UU lzero
+data Sort-Agda : UU lzero
+data Pattern-Agda : UU lzero
+data Clause-Agda : UU lzero
+Telescope-Agda = list (String Γ Argument-Agda Term-Agda)
-data Term where
+data Term-Agda where
-- Variables, where the natural number is a de Bruijn index
- var : (x : β) (args : list (Arg Term)) β Term
+ variable-Term-Agda : β β list (Argument-Agda Term-Agda) β Term-Agda
-- An application of a constructor or definition
- con : (c : Name) (args : list (Arg Term)) β Term
- def : (f : Name) (args : list (Arg Term)) β Term
+ constructor-Term-Agda : Name-Agda β list (Argument-Agda Term-Agda) β Term-Agda
+ definition-Term-Agda : Name-Agda β list (Argument-Agda Term-Agda) β Term-Agda
-- A lambda abstraction
- lam : (v : Visibility) (t : Abs Term) β Term
- pat-lam : (cs : list Clause) (args : list (Arg Term)) β Term
+ lambda-Term-Agda :
+ Visibility-Argument-Agda β Abstraction-Agda Term-Agda β Term-Agda
+ pattern-lambda-Term-Agda :
+ list Clause-Agda β list (Argument-Agda Term-Agda) β Term-Agda
-- A Pi term
- pi : (a : Arg Term) (b : Abs Term) β Term
+ dependent-product-Term-Agda :
+ Argument-Agda Term-Agda β Abstraction-Agda Term-Agda β Term-Agda
-- A sort, also called a universe
- agda-sort : (s : Sort) β Term
+ sort-Term-Agda : Sort-Agda β Term-Agda
-- A literal, e.g. `3`
- lit : (l : Literal) β Term
+ literal-Term-Agda : Literal-Agda β Term-Agda
-- A metavariable
- meta : (x : Meta) β list (Arg Term) β Term
+ metavariable-Term-Agda :
+ Metavariable-Agda β list (Argument-Agda Term-Agda) β Term-Agda
-- A hole
- unknown : Term
+ unknown-Term-Agda : Term-Agda
-data Sort where
+data Sort-Agda where
-- A universe of a given (possibly neutral) level
- set : (t : Term) β Sort
+ universe-Sort-Agda : Term-Agda β Sort-Agda
-- A universe of a given concrete level
- lit : (n : β) β Sort
+ fixed-universe-Sort-Agda : β β Sort-Agda
-- A Prop of a given (possibly neutral) level
- prop : (t : Term) β Sort
+ prop-Sort-Agda : Term-Agda β Sort-Agda
-- A Prop of a given concrete level
- propLit : (n : β) β Sort
+ fixed-prop-Sort-Agda : β β Sort-Agda
-- UUΟi of a given concrete level i.
- inf : (n : β) β Sort
+ fixed-large-universe-Sort-Agda : β β Sort-Agda
-- A hole
- unknown : Sort
-
-data Pattern where
- con : (c : Name) (ps : list (Arg Pattern)) β Pattern
- dot : (t : Term) β Pattern
- var : (x : β) β Pattern
- lit : (l : Literal) β Pattern
- proj : (f : Name) β Pattern
+ unknown-Sort-Agda : Sort-Agda
+
+data Pattern-Agda where
+ constructor-Term-Agda :
+ Name-Agda β list (Argument-Agda Pattern-Agda) β Pattern-Agda
+ dot-Pattern-Agda : Term-Agda β Pattern-Agda
+ variable-Term-Agda : β β Pattern-Agda
+ literal-Term-Agda : Literal-Agda β Pattern-Agda
+ projection-Pattern-Agda : Name-Agda β Pattern-Agda
-- Absurd pattern with a de Bruijn index
- absurd : (x : β) β Pattern
-
--- A clause on a pattern matching lambda
-data Clause where
- clause :
- (tel : Telescope) (ps : list (Arg Pattern)) (t : Term) β Clause
- absurd-clause :
- (tel : Telescope) (ps : list (Arg Pattern)) β Clause
+ absurd-Pattern-Agda : β β Pattern-Agda
+
+-- A clause-Clause-Agda on a pattern matching lambda
+data Clause-Agda where
+ clause-Clause-Agda :
+ Telescope-Agda β list (Argument-Agda Pattern-Agda) β Term-Agda β Clause-Agda
+ absurd-Clause-Agda :
+ Telescope-Agda β list (Argument-Agda Pattern-Agda) β Clause-Agda
```
-Bindings
+## Bindings
```agda
-{-# BUILTIN AGDATERM Term #-}
-{-# BUILTIN AGDASORT Sort #-}
-{-# BUILTIN AGDAPATTERN Pattern #-}
-{-# BUILTIN AGDACLAUSE Clause #-}
-
-{-# BUILTIN AGDATERMVAR var #-}
-{-# BUILTIN AGDATERMCON con #-}
-{-# BUILTIN AGDATERMDEF def #-}
-{-# BUILTIN AGDATERMMETA meta #-}
-{-# BUILTIN AGDATERMLAM lam #-}
-{-# BUILTIN AGDATERMEXTLAM pat-lam #-}
-{-# BUILTIN AGDATERMPI pi #-}
-{-# BUILTIN AGDATERMSORT agda-sort #-}
-{-# BUILTIN AGDATERMLIT lit #-}
-{-# BUILTIN AGDATERMUNSUPPORTED unknown #-}
-
-{-# BUILTIN AGDASORTSET set #-}
-{-# BUILTIN AGDASORTLIT lit #-}
-{-# BUILTIN AGDASORTPROP prop #-}
-{-# BUILTIN AGDASORTPROPLIT propLit #-}
-{-# BUILTIN AGDASORTINF inf #-}
-{-# BUILTIN AGDASORTUNSUPPORTED unknown #-}
-
-{-# BUILTIN AGDAPATCON con #-}
-{-# BUILTIN AGDAPATDOT dot #-}
-{-# BUILTIN AGDAPATVAR var #-}
-{-# BUILTIN AGDAPATLIT lit #-}
-{-# BUILTIN AGDAPATPROJ proj #-}
-{-# BUILTIN AGDAPATABSURD absurd #-}
-
-{-# BUILTIN AGDACLAUSECLAUSE clause #-}
-{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}
+{-# BUILTIN AGDATERM Term-Agda #-}
+{-# BUILTIN AGDASORT Sort-Agda #-}
+{-# BUILTIN AGDAPATTERN Pattern-Agda #-}
+{-# BUILTIN AGDACLAUSE Clause-Agda #-}
+
+{-# BUILTIN AGDATERMVAR variable-Term-Agda #-}
+{-# BUILTIN AGDATERMCON constructor-Term-Agda #-}
+{-# BUILTIN AGDATERMDEF definition-Term-Agda #-}
+{-# BUILTIN AGDATERMMETA metavariable-Term-Agda #-}
+{-# BUILTIN AGDATERMLAM lambda-Term-Agda #-}
+{-# BUILTIN AGDATERMEXTLAM pattern-lambda-Term-Agda #-}
+{-# BUILTIN AGDATERMPI dependent-product-Term-Agda #-}
+{-# BUILTIN AGDATERMSORT sort-Term-Agda #-}
+{-# BUILTIN AGDATERMLIT literal-Term-Agda #-}
+{-# BUILTIN AGDATERMUNSUPPORTED unknown-Term-Agda #-}
+
+{-# BUILTIN AGDASORTSET universe-Sort-Agda #-}
+{-# BUILTIN AGDASORTLIT fixed-universe-Sort-Agda #-}
+{-# BUILTIN AGDASORTPROP prop-Sort-Agda #-}
+{-# BUILTIN AGDASORTPROPLIT fixed-prop-Sort-Agda #-}
+{-# BUILTIN AGDASORTINF fixed-large-universe-Sort-Agda #-}
+{-# BUILTIN AGDASORTUNSUPPORTED unknown-Sort-Agda #-}
+
+{-# BUILTIN AGDAPATCON constructor-Term-Agda #-}
+{-# BUILTIN AGDAPATDOT dot-Pattern-Agda #-}
+{-# BUILTIN AGDAPATVAR variable-Term-Agda #-}
+{-# BUILTIN AGDAPATLIT literal-Term-Agda #-}
+{-# BUILTIN AGDAPATPROJ projection-Pattern-Agda #-}
+{-# BUILTIN AGDAPATABSURD absurd-Pattern-Agda #-}
+
+{-# BUILTIN AGDACLAUSECLAUSE clause-Clause-Agda #-}
+{-# BUILTIN AGDACLAUSEABSURD absurd-Clause-Agda #-}
```
-
-
## Helpers
```agda
-replicate-hidden-Arg : β β list (Arg Term)
-replicate-hidden-Arg zero-β = nil
-replicate-hidden-Arg (succ-β n) =
- cons (hidden-Arg (unknown)) (replicate-hidden-Arg n)
+replicate-hidden-Argument-Agda : β β list (Argument-Agda Term-Agda)
+replicate-hidden-Argument-Agda zero-β =
+ nil
+replicate-hidden-Argument-Agda (succ-β n) =
+ cons
+ ( hidden-Argument-Agda (unknown-Term-Agda))
+ ( replicate-hidden-Argument-Agda n)
```
diff --git a/src/reflection/type-checking-monad.lagda.md b/src/reflection/type-checking-monad.lagda.md
index 790aa2470e..328ffe1795 100644
--- a/src/reflection/type-checking-monad.lagda.md
+++ b/src/reflection/type-checking-monad.lagda.md
@@ -34,168 +34,211 @@ open import reflection.terms
## Idea
-The type-checking monad `TC` allows us to interact directly with Agda's type
-checking mechanism. Additionally to primitives (see below), Agda includes the
-the keyword `unquote` to manually unquote an element from `TC unit`.
+The type-checking monad `type-Type-Checker` allows us to interact directly with
+Agda's type checking mechanism. Additionally to primitives (see below), Agda
+includes the the keyword `unquote` to manually unquote an element from
+`type-Type-Checker unit`.
-## Definition
+## Definitions
```agda
-data ErrorPart : UU lzero where
- strErr : String β ErrorPart
- termErr : Term β ErrorPart
- pattErr : Pattern β ErrorPart
- nameErr : Name β ErrorPart
+data Error-Part : UU lzero where
+ string-Error-Part : String β Error-Part
+ term-Error-Part : Term-Agda β Error-Part
+ pattern-Error-Part : Pattern-Agda β Error-Part
+ name-Error-Part : Name-Agda β Error-Part
postulate
-- The type checking monad
- TC : β {a} β UU a β UU a
- returnTC : β {a} {A : UU a} β A β TC A
- bindTC : β {a b} {A : UU a} {B : UU b} β TC A β (A β TC B) β TC B
+ type-Type-Checker :
+ {l : Level} β UU l β UU l
+ return-Type-Checker :
+ {l : Level} {A : UU l} β A β type-Type-Checker A
+ bind-Type-Checker :
+ {l1 l2 : Level} {A : UU l1} {B : UU l2} β
+ type-Type-Checker A β (A β type-Type-Checker B) β type-Type-Checker B
-- Tries the unify the first term with the second
- unify : Term β Term β TC unit
+ unify :
+ Term-Agda β Term-Agda β type-Type-Checker unit
-- Gives an error
- typeError : β {a} {A : UU a} β list ErrorPart β TC A
+ type-error :
+ {l : Level} {A : UU l} β list Error-Part β type-Type-Checker A
-- Infers the type of a goal
- inferType : Term β TC Term
- checkType : Term β Term β TC Term
- normalise : Term β TC Term
- reduce : Term β TC Term
+ infer-type :
+ Term-Agda β type-Type-Checker Term-Agda
+ check-type :
+ Term-Agda β Term-Agda β type-Type-Checker Term-Agda
+ normalize :
+ Term-Agda β type-Type-Checker Term-Agda
+ reduce :
+ Term-Agda β type-Type-Checker Term-Agda
-- Tries the first computation, if it fails tries the second
- catchTC : β {a} {A : UU a} β TC A β TC A β TC A
- quoteTC : β {a} {A : UU a} β A β TC Term
- unquoteTC : β {a} {A : UU a} β Term β TC A
- quoteΟTC : β {A : UUΟ} β A β TC Term
- getContext : TC Telescope
- extendContext : β {a} {A : UU a} β String β Arg Term β TC A β TC A
- inContext : β {a} {A : UU a} β Telescope β TC A β TC A
- freshName : String β TC Name
- declareDef : Arg Name β Term β TC unit
- declarePostulate : Arg Name β Term β TC unit
- defineFun : Name β list Clause β TC unit
- getType : Name β TC Term
- getDefinition : Name β TC Definition
- blockTC : β {a} {A : UU a} β Blocker β TC A
- commitTC : TC unit
- isMacro : Name β TC bool
-
- formatErrorParts : list ErrorPart β TC String
-
- -- Prints the third argument if the corresponding verbosity level is turned
+ catch-Type-Checker :
+ {l : Level} {A : UU l} β
+ type-Type-Checker A β type-Type-Checker A β type-Type-Checker A
+ quote-Type-Checker :
+ {l : Level} {A : UU l} β A β type-Type-Checker Term-Agda
+ unquote-Type-Checker :
+ {l : Level} {A : UU l} β Term-Agda β type-Type-Checker A
+ quoteΟ-Type-Checker :
+ {A : UUΟ} β A β type-Type-Checker Term-Agda
+ get-context :
+ type-Type-Checker Telescope-Agda
+ extend-context :
+ {l : Level} {A : UU l} β
+ String β Argument-Agda Term-Agda β type-Type-Checker A β type-Type-Checker A
+ in-context :
+ {l : Level} {A : UU l} β
+ Telescope-Agda β type-Type-Checker A β type-Type-Checker A
+ fresh-name :
+ String β type-Type-Checker Name-Agda
+ declare-definition :
+ Argument-Agda Name-Agda β Term-Agda β type-Type-Checker unit
+ declare-postulate :
+ Argument-Agda Name-Agda β Term-Agda β type-Type-Checker unit
+ define-function :
+ Name-Agda β list Clause-Agda β type-Type-Checker unit
+ get-type :
+ Name-Agda β type-Type-Checker Term-Agda
+ get-definition :
+ Name-Agda β type-Type-Checker Definition-Agda
+ block-Type-Checker :
+ {l : Level} {A : UU l} β Blocker-Agda β type-Type-Checker A
+ commit-Type-Checker :
+ type-Type-Checker unit
+ is-macro :
+ Name-Agda β type-Type-Checker bool
+
+ format-error :
+ list Error-Part β type-Type-Checker String
+
+ -- Prints the third argument if the corresponding verbosity Level is turned
-- on (with the -v flag to Agda).
- debugPrint : String β β β list ErrorPart β TC unit
+ debug-print :
+ String β β β list Error-Part β type-Type-Checker unit
- -- If 'true', makes the following primitives also normalise
- -- their results: inferType, checkType, quoteTC, getType, and getContext
- withNormalisation : β {a} {A : UU a} β bool β TC A β TC A
- askNormalisation : TC bool
+ -- If 'true', makes the following primitives also normalize
+ -- their results: infer-type, check-type, quote-Type-Checker, get-type, and get-context
+ with-normalization :
+ {l : Level} {A : UU l} β bool β type-Type-Checker A β type-Type-Checker A
+ ask-normalization : type-Type-Checker bool
-- If 'true', makes the following primitives to reconstruct hidden arguments:
- -- getDefinition, normalise, reduce, inferType, checkType and getContext
- withReconstructed : β {a} {A : UU a} β bool β TC A β TC A
- askReconstructed : TC bool
+ -- get-definition, normalize, reduce, infer-type, check-type and get-context
+ with-reconstructed :
+ {l : Level} {A : UU l} β bool β type-Type-Checker A β type-Type-Checker A
+ ask-reconstructed : type-Type-Checker bool
-- Whether implicit arguments at the end should be turned into metavariables
- withExpandLast : β {a} {A : UU a} β bool β TC A β TC A
- askExpandLast : TC bool
+ with-expand-last :
+ {l : Level} {A : UU l} β bool β type-Type-Checker A β type-Type-Checker A
+ ask-expand-last : type-Type-Checker bool
- -- White/blacklist specific definitions for reduction while executing the TC computation
+ -- White/blacklist specific definitions for reduction while executing the type-Type-Checker computation
-- 'true' for whitelist, 'false' for blacklist
- withReduceDefs : β {a} {A : UU a} β (Ξ£ bool Ξ» _ β list Name) β TC A β TC A
- askReduceDefs : TC (Ξ£ bool Ξ» _ β list Name)
+ with-reduce-definitions :
+ {l : Level} {A : UU l} β
+ bool Γ list Name-Agda β type-Type-Checker A β type-Type-Checker A
+ ask-reduce-definitions :
+ type-Type-Checker (bool Γ list Name-Agda)
-- Fail if the given computation gives rise to new, unsolved
-- "blocking" constraints.
- noConstraints : β {a} {A : UU a} β TC A β TC A
-
- -- Run the given TC action and return the first component. Resets to
- -- the old TC state if the second component is 'false', or keep the
- -- new TC state if it is 'true'.
- runSpeculative : β {a} {A : UU a} β TC (Ξ£ A Ξ» _ β bool) β TC A
-
- -- Get a list of all possible instance candidates for the given meta
- -- variable (it does not have to be an instance meta).
- getInstances : Meta β TC (list Term)
-
- declareData : Name β β β Term β TC unit
- defineData : Name β list (Ξ£ Name (Ξ» _ β Term)) β TC unit
+ no-constraints :
+ {l : Level} {A : UU l} β type-Type-Checker A β type-Type-Checker A
+
+ -- Run the given type-Type-Checker action and return the first component. Resets to
+ -- the old type-Type-Checker state if the second component is 'false', or keep the
+ -- new type-Type-Checker state if it is 'true'.
+ run-speculative :
+ {l : Level} {A : UU l} β type-Type-Checker (A Γ bool) β type-Type-Checker A
+
+ -- Get a list of all possible instance candidates for the given metavariable
+ -- variable (it does not have to be an instance metavariable).
+ get-instances :
+ Metavariable-Agda β type-Type-Checker (list Term-Agda)
+
+ declare-data :
+ Name-Agda β β β Term-Agda β type-Type-Checker unit
+ define-data :
+ Name-Agda β list (Name-Agda Γ Term-Agda) β type-Type-Checker unit
```
-Bindings
+## Bindings
```agda
-{-# BUILTIN AGDAERRORPART ErrorPart #-}
-{-# BUILTIN AGDAERRORPARTSTRING strErr #-}
-{-# BUILTIN AGDAERRORPARTTERM termErr #-}
-{-# BUILTIN AGDAERRORPARTPATT pattErr #-}
-{-# BUILTIN AGDAERRORPARTNAME nameErr #-}
-
-{-# BUILTIN AGDATCM TC #-}
-{-# BUILTIN AGDATCMRETURN returnTC #-}
-{-# BUILTIN AGDATCMBIND bindTC #-}
+{-# BUILTIN AGDAERRORPART Error-Part #-}
+{-# BUILTIN AGDAERRORPARTSTRING string-Error-Part #-}
+{-# BUILTIN AGDAERRORPARTTERM term-Error-Part #-}
+{-# BUILTIN AGDAERRORPARTPATT pattern-Error-Part #-}
+{-# BUILTIN AGDAERRORPARTNAME name-Error-Part #-}
+
+{-# BUILTIN AGDATCM type-Type-Checker #-}
+{-# BUILTIN AGDATCMRETURN return-Type-Checker #-}
+{-# BUILTIN AGDATCMBIND bind-Type-Checker #-}
{-# BUILTIN AGDATCMUNIFY unify #-}
-{-# BUILTIN AGDATCMTYPEERROR typeError #-}
-{-# BUILTIN AGDATCMINFERTYPE inferType #-}
-{-# BUILTIN AGDATCMCHECKTYPE checkType #-}
-{-# BUILTIN AGDATCMNORMALISE normalise #-}
+{-# BUILTIN AGDATCMTYPEERROR type-error #-}
+{-# BUILTIN AGDATCMINFERTYPE infer-type #-}
+{-# BUILTIN AGDATCMCHECKTYPE check-type #-}
+{-# BUILTIN AGDATCMNORMALISE normalize #-}
{-# BUILTIN AGDATCMREDUCE reduce #-}
-{-# BUILTIN AGDATCMCATCHERROR catchTC #-}
-{-# BUILTIN AGDATCMQUOTETERM quoteTC #-}
-{-# BUILTIN AGDATCMUNQUOTETERM unquoteTC #-}
-{-# BUILTIN AGDATCMQUOTEOMEGATERM quoteΟTC #-}
-{-# BUILTIN AGDATCMGETCONTEXT getContext #-}
-{-# BUILTIN AGDATCMEXTENDCONTEXT extendContext #-}
-{-# BUILTIN AGDATCMINCONTEXT inContext #-}
-{-# BUILTIN AGDATCMFRESHNAME freshName #-}
-{-# BUILTIN AGDATCMDECLAREDEF declareDef #-}
-{-# BUILTIN AGDATCMDECLAREPOSTULATE declarePostulate #-}
-{-# BUILTIN AGDATCMDEFINEFUN defineFun #-}
-{-# BUILTIN AGDATCMGETTYPE getType #-}
-{-# BUILTIN AGDATCMGETDEFINITION getDefinition #-}
-{-# BUILTIN AGDATCMBLOCK blockTC #-}
-{-# BUILTIN AGDATCMCOMMIT commitTC #-}
-{-# BUILTIN AGDATCMISMACRO isMacro #-}
-{-# BUILTIN AGDATCMWITHNORMALISATION withNormalisation #-}
-{-# BUILTIN AGDATCMFORMATERRORPARTS formatErrorParts #-}
-{-# BUILTIN AGDATCMDEBUGPRINT debugPrint #-}
-{-# BUILTIN AGDATCMWITHRECONSTRUCTED withReconstructed #-}
-{-# BUILTIN AGDATCMWITHEXPANDLAST withExpandLast #-}
-{-# BUILTIN AGDATCMWITHREDUCEDEFS withReduceDefs #-}
-{-# BUILTIN AGDATCMASKNORMALISATION askNormalisation #-}
-{-# BUILTIN AGDATCMASKRECONSTRUCTED askReconstructed #-}
-{-# BUILTIN AGDATCMASKEXPANDLAST askExpandLast #-}
-{-# BUILTIN AGDATCMASKREDUCEDEFS askReduceDefs #-}
-{-# BUILTIN AGDATCMNOCONSTRAINTS noConstraints #-}
-{-# BUILTIN AGDATCMRUNSPECULATIVE runSpeculative #-}
-{-# BUILTIN AGDATCMGETINSTANCES getInstances #-}
-{-# BUILTIN AGDATCMDECLAREDATA declareData #-}
-{-# BUILTIN AGDATCMDEFINEDATA defineData #-}
+{-# BUILTIN AGDATCMCATCHERROR catch-Type-Checker #-}
+{-# BUILTIN AGDATCMQUOTETERM quote-Type-Checker #-}
+{-# BUILTIN AGDATCMUNQUOTETERM unquote-Type-Checker #-}
+{-# BUILTIN AGDATCMQUOTEOMEGATERM quoteΟ-Type-Checker #-}
+{-# BUILTIN AGDATCMGETCONTEXT get-context #-}
+{-# BUILTIN AGDATCMEXTENDCONTEXT extend-context #-}
+{-# BUILTIN AGDATCMINCONTEXT in-context #-}
+{-# BUILTIN AGDATCMFRESHNAME fresh-name #-}
+{-# BUILTIN AGDATCMDECLAREDEF declare-definition #-}
+{-# BUILTIN AGDATCMDECLAREPOSTULATE declare-postulate #-}
+{-# BUILTIN AGDATCMDEFINEFUN define-function #-}
+{-# BUILTIN AGDATCMGETTYPE get-type #-}
+{-# BUILTIN AGDATCMGETDEFINITION get-definition #-}
+{-# BUILTIN AGDATCMBLOCK block-Type-Checker #-}
+{-# BUILTIN AGDATCMCOMMIT commit-Type-Checker #-}
+{-# BUILTIN AGDATCMISMACRO is-macro #-}
+{-# BUILTIN AGDATCMWITHNORMALISATION with-normalization #-}
+{-# BUILTIN AGDATCMFORMATERRORPARTS format-error #-}
+{-# BUILTIN AGDATCMDEBUGPRINT debug-print #-}
+{-# BUILTIN AGDATCMWITHRECONSTRUCTED with-reconstructed #-}
+{-# BUILTIN AGDATCMWITHEXPANDLAST with-expand-last #-}
+{-# BUILTIN AGDATCMWITHREDUCEDEFS with-reduce-definitions #-}
+{-# BUILTIN AGDATCMASKNORMALISATION ask-normalization #-}
+{-# BUILTIN AGDATCMASKRECONSTRUCTED ask-reconstructed #-}
+{-# BUILTIN AGDATCMASKEXPANDLAST ask-expand-last #-}
+{-# BUILTIN AGDATCMASKREDUCEDEFS ask-reduce-definitions #-}
+{-# BUILTIN AGDATCMNOCONSTRAINTS no-constraints #-}
+{-# BUILTIN AGDATCMRUNSPECULATIVE run-speculative #-}
+{-# BUILTIN AGDATCMGETINSTANCES get-instances #-}
+{-# BUILTIN AGDATCMDECLAREDATA declare-data #-}
+{-# BUILTIN AGDATCMDEFINEDATA define-data #-}
```
-
-
## Monad syntax
```agda
infixl 15 _<|>_
-_<|>_ : {l : Level} {A : UU l} β TC A β TC A β TC A
-_<|>_ = catchTC
+_<|>_ :
+ {l : Level} {A : UU l} β
+ type-Type-Checker A β type-Type-Checker A β type-Type-Checker A
+_<|>_ = catch-Type-Checker
infixl 10 _>>=_ _>>_ _<&>_
_>>=_ :
{l1 l2 : Level} {A : UU l1} {B : UU l2} β
- TC A β (A β TC B) β TC B
-_>>=_ = bindTC
+ type-Type-Checker A β (A β type-Type-Checker B) β type-Type-Checker B
+_>>=_ = bind-Type-Checker
_>>_ :
{l1 l2 : Level} {A : UU l1} {B : UU l2} β
- TC A β TC B β TC B
-xs >> ys = bindTC xs (Ξ» _ β ys)
+ type-Type-Checker A β type-Type-Checker B β type-Type-Checker B
+xs >> ys = bind-Type-Checker xs (Ξ» _ β ys)
_<&>_ :
{l1 l2 : Level} {A : UU l1} {B : UU l2} β
- TC A β (A β B) β TC B
-xs <&> f = bindTC xs (Ξ» x β returnTC (f x))
+ type-Type-Checker A β (A β B) β type-Type-Checker B
+xs <&> f = bind-Type-Checker xs (Ξ» x β return-Type-Checker (f x))
```
## Examples
@@ -210,10 +253,10 @@ adapted from alhassy's
```agda
private
- numTCM : Term β TC unit
- numTCM h = unify (quoteTerm 314) h
+ num-Type-Checker : Term-Agda β type-Type-Checker unit
+ num-Type-Checker h = unify (quoteTerm 314) h
- _ : unquote numTCM οΌ 314
+ _ : unquote num-Type-Checker οΌ 314
_ = refl
```
@@ -221,10 +264,10 @@ private
```agda
macro
- numTCM' : Term β TC unit
- numTCM' h = unify (quoteTerm 1) h
+ num-Type-Checker' : Term-Agda β type-Type-Checker unit
+ num-Type-Checker' h = unify (quoteTerm 1) h
- _ : numTCM' οΌ 1
+ _ : num-Type-Checker' οΌ 1
_ = refl
```
@@ -232,9 +275,9 @@ private
```agda
macro
- swap-add : Term β Term β TC unit
- swap-add (def (quote add-β) (cons a (cons b nil))) hole =
- unify hole (def (quote add-β) (cons b (cons a nil)))
+ swap-add : Term-Agda β Term-Agda β type-Type-Checker unit
+ swap-add (definition-Term-Agda (quote add-β) (cons a (cons b nil))) hole =
+ unify hole (definition-Term-Agda (quote add-β) (cons b (cons a nil)))
{-# CATCHALL #-}
swap-add v hole = unify hole v
@@ -255,22 +298,35 @@ example was addapted from
infixr 10 _β·_
pattern _β·_ x xs = cons x xs
- οΌ-type-info : Term β TC (Arg Term Γ (Arg Term Γ (Term Γ Term)))
+ οΌ-type-info :
+ Term-Agda β
+ type-Type-Checker
+ ( Argument-Agda Term-Agda Γ
+ ( Argument-Agda Term-Agda Γ
+ ( Term-Agda Γ Term-Agda)))
οΌ-type-info
- ( def (quote _οΌ_) (π β· π― β· (arg _ l) β· (arg _ r) β· nil)) =
- returnTC (π , π― , l , r)
- οΌ-type-info _ = typeError (unit-list (strErr "Term is not a οΌ-type."))
+ ( definition-Term-Agda
+ ( quote _οΌ_)
+ ( π β· π― β· (cons-Argument-Agda _ l) β· (cons-Argument-Agda _ r) β· nil)) =
+ return-Type-Checker (π , π― , l , r)
+ οΌ-type-info _ =
+ type-error (unit-list (string-Error-Part "Term-Agda is not a οΌ-type."))
macro
- try-path! : Term β Term β TC unit
+ try-path! : Term-Agda β Term-Agda β type-Type-Checker unit
try-path! p goal =
( unify goal p) <|>
( do
- p-type β inferType p
+ p-type β infer-type p
π , π― , l , r β οΌ-type-info p-type
unify goal
- ( def (quote inv)
- ( π β· π― β· hidden-Arg l β· hidden-Arg r β· visible-Arg p β· nil)))
+ ( definition-Term-Agda (quote inv)
+ ( π β·
+ π― β·
+ hidden-Argument-Agda l β·
+ hidden-Argument-Agda r β·
+ visible-Argument-Agda p β·
+ nil)))
module _ (a b : β) (p : a οΌ b) where
ex3 : Id a b
@@ -280,19 +336,19 @@ example was addapted from
ex4 = try-path! p
```
-### Getting the lhs and rhs of a goal
+### Getting the left-hand side and right-hand side of a goal
```agda
-boundary-TCM : Term β TC (Term Γ Term)
-boundary-TCM
- ( def
+boundary-Type-Checker : Term-Agda β type-Type-Checker (Term-Agda Γ Term-Agda)
+boundary-Type-Checker
+ ( definition-Term-Agda
( quote Id)
- ( π β· π― β· arg _ l β· arg _ r β· nil)) =
- returnTC (l , r)
-boundary-TCM t =
- typeError
- ( strErr "The term\n " β·
- termErr t β·
- strErr "\nis not a οΌ-type." β·
+ ( π β· π― β· cons-Argument-Agda _ l β· cons-Argument-Agda _ r β· nil)) =
+ return-Type-Checker (l , r)
+boundary-Type-Checker t =
+ type-error
+ ( string-Error-Part "The term\n " β·
+ term-Error-Part t β·
+ string-Error-Part "\nis not a οΌ-type." β·
nil)
```
diff --git a/src/ring-theory/rings.lagda.md b/src/ring-theory/rings.lagda.md
index 3a0311b017..69bdbd6ffa 100644
--- a/src/ring-theory/rings.lagda.md
+++ b/src/ring-theory/rings.lagda.md
@@ -690,17 +690,17 @@ module _
preserves-concat-add-list-Ring = preserves-concat-add-list-Ab (ab-Ring R)
```
-### Equip a type with a structure of a ring
+### Equipping a type with the structure of a ring
```agda
structure-ring :
{l1 : Level} β UU l1 β UU l1
structure-ring X =
Ξ£ ( structure-abelian-group X)
- ( Ξ» p β has-mul-Ab (compute-structure-abelian-group X p))
+ ( Ξ» p β has-mul-Ab (abelian-group-structure-abelian-group X p))
-compute-structure-ring :
+ring-structure-ring :
{l1 : Level} β (X : UU l1) β structure-ring X β Ring l1
-pr1 (compute-structure-ring X (p , q)) = compute-structure-abelian-group X p
-pr2 (compute-structure-ring X (p , q)) = q
+pr1 (ring-structure-ring X (p , q)) = abelian-group-structure-abelian-group X p
+pr2 (ring-structure-ring X (p , q)) = q
```
diff --git a/src/species/hasse-weil-species.lagda.md b/src/species/hasse-weil-species.lagda.md
index 1828a3238f..112b5ea0a7 100644
--- a/src/species/hasse-weil-species.lagda.md
+++ b/src/species/hasse-weil-species.lagda.md
@@ -26,7 +26,7 @@ types that preserves cartesian products. The **Hasse-Weil species** is a species
of finite inhabited types defined for any finite inhabited type `k` as
```text
-Ξ£ (p : structure-semisimple-commutative-ring-π½ k) ; S (commutative-finite-ring-compute-structure-semisimple-commutative-ring-π½ k p)
+Ξ£ (p : structure-semisimple-commutative-ring-π½ k) ; S (commutative-finite-ring-finite-semisimple-commutative-ring-structure-semisimple-commutative-ring-π½ k p)
```
## Definitions
@@ -55,7 +55,7 @@ module _
( Ξ» p β
S
( commutative-finite-ring-Semisimple-Commutative-Ring-π½
- ( compute-structure-semisimple-commutative-ring-π½
+ ( finite-semisimple-commutative-ring-structure-semisimple-commutative-ring-π½
( l3)
( l4)
( k , f)
diff --git a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md
index 9d75d749c2..a756011d87 100644
--- a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md
+++ b/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md
@@ -48,7 +48,7 @@ module _
refl-Ω² = refl
```
-### Vertical and horizontal concatination operations on double loop
+### Vertical and horizontal concatenation operations on double loop
spaces.
@@ -62,7 +62,7 @@ horizontal-concat-Ω² :
horizontal-concat-Ω² α β = horizontal-concat-Id² α β
```
-### Unit laws horizontal, vertical concatination, and whiskering
+### Unit laws horizontal, vertical concatenation, and whiskering
```agda
module _
diff --git a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
index 0a33bc7e2e..a064546334 100644
--- a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
+++ b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
@@ -112,8 +112,8 @@ Eckmann-Hilton argument is often depicted as follows:
| β | | β | refl-Ω² | | refl-Ω² | α | | α |
```
-The first picture represents the vertical concatination of `Ξ±` and `Ξ²`. The
-notation ` | Ξ³ | Ξ΄ |` represents the horizontal concatination of 2-dimensional
+The first picture represents the vertical concatenation of `Ξ±` and `Ξ²`. The
+notation ` | Ξ³ | Ξ΄ |` represents the horizontal concatenation of 2-dimensional
identifications `Ξ³` and `Ξ΄`. Then `| refl | Ξ± |` is just
[`left-whisker-concat refl-Ω² α`](https://unimath.github.io/agda-unimath/foundation.path-algebra.html#7697).
The first and last equality come from the unit laws of whiskering. And the
diff --git a/src/univalent-combinatorics/inhabited-finite-types.lagda.md b/src/univalent-combinatorics/inhabited-finite-types.lagda.md
index 97ce9a3ecc..087157d9a3 100644
--- a/src/univalent-combinatorics/inhabited-finite-types.lagda.md
+++ b/src/univalent-combinatorics/inhabited-finite-types.lagda.md
@@ -68,7 +68,7 @@ module _
compute-Inhabited-π½ :
{l : Level} β
Inhabited-π½ l β
- Ξ£ (Inhabited-Type l) (Ξ» X β is-finite (type-Inhabited-Type X))
+ Ξ£ (Inhabited-Type l) (Ξ» X β is-finite (type-Inhabited-Type X))
compute-Inhabited-π½ = equiv-right-swap-Ξ£
is-finite-and-inhabited-Prop : {l : Level} β UU l β Prop l
@@ -124,8 +124,8 @@ module _
compute-Fam-Inhabited-π½ :
{l1 l2 : Level} β (X : π½ l1) β
Fam-Inhabited-Types-π½ l2 X β
- Ξ£ ( Fam-Inhabited-Types l2 (type-π½ X))
- ( Ξ» Y β (x : type-π½ X) β is-finite (type-Inhabited-Type (Y x)))
+ Ξ£ ( Fam-Inhabited-Types l2 (type-π½ X))
+ ( Ξ» Y β (x : type-π½ X) β is-finite (type-Inhabited-Type (Y x)))
compute-Fam-Inhabited-π½ X =
( distributive-Ξ -Ξ£) βe
( equiv-Ξ