Final universal algebra (#544)

My final commit on universal algebra, I did not reach my goal of the
first homomorphism theorem as I've realized a lot of theory will be
needed for it, and I want to work on more immediate results.

----------------

For posterity, here's my thoughts on what and how to proof next (and
other stuff) if one wanted to continue this line
1. Prove that `induced-function-term` is the same as `eval-term` in the
sense more precise of commit
a070945
(lazily called `assignment-vec'`).
2. Prove that the quotient algebra is indeed an algebra: use the
previous result to say that each axiom in the quotients comes from
function application in the quotient, and then prove that this function
is one that comes from functoriality in the base algebra. (Alternatively
redefine the model in the quotient algebra so that this holds by
definition).
3. (1) is hard as a lot of workarounds (mutual recursion) have to be
made to satisfy the termination checker, alternatively one could
redefine being an algebra as one that matches the
`induced-function-term`s associated to two terms `t1` and `t2`. Notice
that the de bruijn variables in each term may be different, so that an
appropriate notion of merging and extending the induced functions must
be made.
4. Once these results hold, I think classic results should be relatively
easy, including the homomorphism theorems. My goal was proving the first
homomorphism theorem and applying it to the algebraic theory of groups,
and then transporting the result to groups (through univalance). I
wanted a general and *practical* way to study and prove stuff about all
algebraic structures. In the end, I'm still not sure if this approach
would have worked...

src/foundation/multivariable-functoriality-set-quotients.lagda.md

@@ -9,7 +9,9 @@ module foundation.multivariable-functoriality-set-quotients where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.functions
 open import foundation.functoriality-set-quotients
+open import foundation.homotopies
 open import foundation.multivariable-operations
 open import foundation.set-quotients
 open import foundation.universe-levels
@@ -41,15 +43,39 @@ equivalence relations extends uniquely to a multivariable operation from the
 module _
   { l1 l2 l3 l4 : Level}
   ( n : ℕ)
-  ( As : functional-vec (UU l1) n)
-  ( Rs : (i : Fin n) → Eq-Rel l2 (As i))
+  ( A : functional-vec (UU l1) n)
+  ( R : (i : Fin n) → Eq-Rel l2 (A i))
   { X : UU l3} (S : Eq-Rel l4 X)
   where
 
   multivariable-map-set-quotient :
-    (h : hom-Eq-Rel (all-sim-Eq-Rel n As Rs) S) →
-    set-quotient-vector n As Rs → set-quotient S
-  multivariable-map-set-quotient h as =
-    map-set-quotient (all-sim-Eq-Rel n As Rs) S h
-      ( map-equiv (equiv-set-quotient-vector n As Rs) as)
+    ( h : hom-Eq-Rel (all-sim-Eq-Rel n A R) S) →
+    set-quotient-vector n A R → set-quotient S
+  multivariable-map-set-quotient =
+    map-is-set-quotient
+      ( all-sim-Eq-Rel n A R)
+      ( set-quotient-vector-Set n A R)
+      ( reflecting-map-quotient-vector-map n A R)
+      ( S)
+      ( quotient-Set S)
+      ( reflecting-map-quotient-map S)
+      ( is-set-quotient-vector-set-quotient n A R)
+      ( is-set-quotient-set-quotient S)
+
+  compute-multivariable-map-set-quotient :
+    ( h : hom-Eq-Rel (all-sim-Eq-Rel n A R) S) →
+    ( multivariable-map-set-quotient h ∘
+      quotient-vector-map n A R ) ~
+    ( quotient-map S ∘
+      map-hom-Eq-Rel (all-sim-Eq-Rel n A R) S h)
+  compute-multivariable-map-set-quotient =
+     coherence-square-map-is-set-quotient
+      ( all-sim-Eq-Rel n A R)
+      ( set-quotient-vector-Set n A R)
+      ( reflecting-map-quotient-vector-map n A R)
+      ( S)
+      ( quotient-Set S)
+      ( reflecting-map-quotient-map S)
+      ( is-set-quotient-vector-set-quotient n A R)
+      ( is-set-quotient-set-quotient S)
 ```

src/linear-algebra/vectors.lagda.md

@@ -66,6 +66,10 @@ module _
   revert-vec : {n : ℕ} → vec A n → vec A n
   revert-vec empty-vec = empty-vec
   revert-vec (x ∷ v) = snoc-vec (revert-vec v) x
+
+  all-vec : {l2 : Level} {n : ℕ} → (P : A → UU l2) → vec A n → UU l2
+  all-vec P empty-vec = raise-unit _
+  all-vec P (x ∷ v) = P x × all-vec P v
 ```
 
 ### The functional type of vectors

src/univalent-combinatorics/lists.lagda.md

@@ -11,6 +11,7 @@ open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
 
+open import foundation.booleans
 open import foundation.cartesian-product-types
 open import foundation.contractible-types
 open import foundation.coproduct-types
@@ -23,6 +24,7 @@ open import foundation.functions
 open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.negation
 open import foundation.raising-universe-levels
 open import foundation.sets
 open import foundation.truncated-types
@@ -42,22 +44,37 @@ empty list and an operation that extends a list with one element from `A`.
 
 ## Definition
 
+### The inductive definition of the type of lists
+
 ```agda
 data list {l : Level} (A : UU l) : UU l where
   nil : list A
   cons : A → list A → list A
+```
+
+### Predicates on the type of lists
+
+```agda
+is-nil-list : {l : Level} {A : UU l} → list A → UU l
+is-nil-list l = (l ＝ nil)
+
+is-nonnil-list : {l : Level} {A : UU l} → list A → UU l
+is-nonnil-list l = ¬ (is-nil-list l)
+
+is-cons-list : {l : Level} {A : UU l} → list A → UU l
+is-cons-list {l1} {A} l = Σ (A × list A) (λ (a , l') → l ＝ cons a l')
+```
+
+### Operations
 
+```agda
 snoc : {l : Level} {A : UU l} → list A → A → list A
 snoc nil a = cons a nil
 snoc (cons b l) a = cons b (snoc l a)
 
 in-list : {l : Level} {A : UU l} → A → list A
 in-list a = cons a nil
-```
 
-## Operations
-
-```agda
 fold-list :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (b : B) (μ : A → (B → B)) →
   list A → B
@@ -88,6 +105,24 @@ reverse-list : {l : Level} {A : UU l} → list A → list A
 reverse-list nil = nil
 reverse-list (cons a l) = concat-list (reverse-list l) (in-list a)
 
+elem-list :
+  {l1 : Level} {A : UU l1} →
+  has-decidable-equality A →
+  A → list A → bool
+elem-list d x nil = false
+elem-list d x (cons x' l) with (d x x')
+... | inl _ = true
+... | inr _ = elem-list d x l
+
+union-list :
+  {l1 : Level} {A : UU l1} →
+  has-decidable-equality A →
+  list A → list A → list A
+union-list d nil l' = l'
+union-list d (cons x l) l' with (elem-list d x l')
+... | true = l'
+... | false = cons x l'
+
 data _∈-list_ {l : Level} {A : UU l} : A → list A → UU l where
   is-head : (a : A) (l : list A) → a ∈-list (cons a l)
   is-in-tail : (a x : A) (l : list A) → a ∈-list l → a ∈-list (cons x l)
@@ -98,6 +133,43 @@ unit-list a = cons a nil
 
 ## Properties
 
+### A list that uses cons is not nil
+
+```agda
+is-nonnil-cons-list :
+  {l : Level} {A : UU l} →
+  (a : A) → (l : list A) → is-nonnil-list (cons a l)
+is-nonnil-cons-list a l ()
+
+is-nonnil-is-cons-list :
+  {l : Level} {A : UU l} →
+  (l : list A) → is-cons-list l → is-nonnil-list l
+is-nonnil-is-cons-list l ((a , l') , refl) q =
+  is-nonnil-cons-list a l' q
+```
+
+### A list that uses cons is not nil
+
+```agda
+is-cons-is-nonnil-list :
+  {l : Level} {A : UU l} →
+  (l : list A) → is-nonnil-list l → is-cons-list l
+is-cons-is-nonnil-list nil p = ex-falso (p refl)
+is-cons-is-nonnil-list (cons x l) p = ((x , l) , refl)
+
+head-is-nonnil-list :
+  {l : Level} {A : UU l} →
+  (l : list A) → is-nonnil-list l → A
+head-is-nonnil-list l p =
+  pr1 (pr1 (is-cons-is-nonnil-list l p))
+
+tail-is-nonnil-list :
+  {l : Level} {A : UU l} →
+  (l : list A) → is-nonnil-list l → list A
+tail-is-nonnil-list l p =
+  pr2 (pr1 (is-cons-is-nonnil-list l p))
+```
+
 ### Characterizing the identity type of lists
 
 ```agda
@@ -326,6 +398,36 @@ length-functor-list :
 length-functor-list f nil = refl
 length-functor-list f (cons x l) =
   ap succ-ℕ (length-functor-list f l)
+
+is-nil-is-zero-length-list :
+  {l1 : Level} {A : UU l1}
+  (l : list A) →
+  is-zero-ℕ (length-list l) →
+  is-nil-list l
+is-nil-is-zero-length-list nil p = refl
+
+is-nonnil-is-nonzero-length-list :
+  {l1 : Level} {A : UU l1}
+  (l : list A) →
+  is-nonzero-ℕ (length-list l) →
+  is-nonnil-list l
+is-nonnil-is-nonzero-length-list nil p q = p refl
+is-nonnil-is-nonzero-length-list (cons x l) p ()
+
+is-nonzero-length-is-nonnil-list :
+  {l1 : Level} {A : UU l1}
+  (l : list A) →
+  is-nonnil-list l →
+  is-nonzero-ℕ (length-list l)
+is-nonzero-length-is-nonnil-list nil p q = p refl
+
+lenght-tail-is-nonnil-list :
+  {l1 : Level} {A : UU l1}
+  (l : list A) → (p : is-nonnil-list l) →
+  succ-ℕ (length-list (tail-is-nonnil-list l p)) ＝
+    length-list l
+lenght-tail-is-nonnil-list nil p = ex-falso (p refl)
+lenght-tail-is-nonnil-list (cons x l) p = refl
 ```
 
 ### Properties of flattening
@@ -629,6 +731,38 @@ module _
     ap (cons (f x)) (preserves-concat-map-list l k)
 ```
 
+### If a list has an element then it is non empty
+
+```agda
+is-nonnil-elem-list :
+  {l : Level} {A : UU l} →
+  (d : has-decidable-equality A) →
+  (a : A) →
+  (l : list A) →
+  elem-list d a l ＝ true →
+  is-nonnil-list l
+is-nonnil-elem-list d a nil ()
+is-nonnil-elem-list d a (cons x l) p ()
+```
+
+### If the union of two lists is empty, then these two lists are empty
+
+```agda
+is-nil-union-is-nil-list :
+  {l : Level} {A : UU l} →
+  (d : has-decidable-equality A) →
+  (l l' : list A) →
+  union-list d l l' ＝ nil →
+  is-nil-list l × is-nil-list l'
+is-nil-union-is-nil-list d nil l' p = (refl , p)
+is-nil-union-is-nil-list d (cons x l) l' p with (elem-list d x l') in q
+... | true =
+  ex-falso (is-nonnil-elem-list d x l' q p )
+    -- ( is-nonnil-elem-list d x l' q
+    --   (pr2 (is-nil-union-is-nil-list d l l' p)))
+... | false = ex-falso (is-nonnil-cons-list x l' p) -- (is-nonnil-cons-list x (union-list d l l') p)
+```
+
 ### Multiplication of a list of elements in a monoid
 
 ```agda

src/universal-algebra.lagda.md

@@ -9,6 +9,7 @@ open import universal-algebra.algebraic-theory-of-groups public
 open import universal-algebra.algebras-of-theories public
 open import universal-algebra.congruences public
 open import universal-algebra.homomorphisms-of-algebras public
+open import universal-algebra.kernels public
 open import universal-algebra.models-of-signatures public
 open import universal-algebra.quotient-algebras public
 open import universal-algebra.signatures public

src/universal-algebra/congruences.lagda.md

@@ -77,4 +77,10 @@ module _
     { l4 : Level } →
     congruence-Algebra l4 → ( Eq-Rel l4 (type-Algebra Sg Th Alg))
   eq-rel-congruence-Algebra = pr1
+
+  respects-operations-congruence-Algebra :
+    { l4 : Level } →
+    ( R : congruence-Algebra l4) →
+    ( respects-operations (eq-rel-congruence-Algebra R))
+  respects-operations-congruence-Algebra = pr2
 ```

src/universal-algebra/kernels.lagda.md

@@ -0,0 +1,87 @@
+# Kernels of homomorphisms of algebras
+
+```agda
+module universal-algebra.kernels where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
+open import foundation.equational-reasoning
+open import foundation.equivalence-relations
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import linear-algebra.functoriality-vectors
+open import linear-algebra.vectors
+
+open import universal-algebra.algebraic-theories
+open import universal-algebra.algebras-of-theories
+open import universal-algebra.congruences
+open import universal-algebra.homomorphisms-of-algebras
+open import universal-algebra.signatures
+```
+
+</details>
+
+## Idea
+
+The kernel of a homomorphism `f` of algebras is the congruence relation given by
+`x ~ y` iff `f x ~ f y`.
+
+## Definitions
+
+```agda
+module _
+  { l1 : Level} ( Sg : signature l1)
+  { l2 : Level } ( Th : Theory Sg l2)
+  { l3 l4 : Level }
+  ( Alg1 : Algebra Sg Th l3)
+  ( Alg2 : Algebra Sg Th l4)
+  ( F : type-hom-Algebra Sg Th Alg1 Alg2)
+  where
+
+  rel-prop-kernel-hom-Algebra :
+    Rel-Prop l4 (type-Algebra Sg Th Alg1)
+  pr1 (rel-prop-kernel-hom-Algebra x y) =
+    map-hom-Algebra Sg Th Alg1 Alg2 F x ＝
+      map-hom-Algebra Sg Th Alg1 Alg2 F y
+  pr2 (rel-prop-kernel-hom-Algebra x y) =
+    is-set-Algebra Sg Th Alg2 _ _
+
+  eq-rel-kernel-hom-Algebra :
+    Eq-Rel l4 (type-Algebra Sg Th Alg1)
+  pr1 eq-rel-kernel-hom-Algebra =
+    rel-prop-kernel-hom-Algebra
+  pr1 (pr2 eq-rel-kernel-hom-Algebra) = refl
+  pr1 (pr2 (pr2 eq-rel-kernel-hom-Algebra)) = inv
+  pr2 (pr2 (pr2 eq-rel-kernel-hom-Algebra)) = _∙_
+
+  kernel-hom-Algebra :
+    congruence-Algebra Sg Th Alg1 l4
+  pr1 kernel-hom-Algebra = eq-rel-kernel-hom-Algebra
+  pr2 kernel-hom-Algebra op v v' p =
+    equational-reasoning
+      f (is-model-set-Algebra Sg Th Alg1 op v)
+        ＝ is-model-set-Algebra Sg Th Alg2 op (map-vec f v)
+          by preserves-operations-hom-Algebra Sg Th Alg1 Alg2 F op v
+        ＝ is-model-set-Algebra Sg Th Alg2 op (map-vec f v')
+          by ap ( is-model-set-Algebra Sg Th Alg2 op)
+                ( map-hom-Algebra-lemma (pr2 Sg op) v v' p)
+        ＝ f (is-model-set-Algebra Sg Th Alg1 op v')
+          by inv (preserves-operations-hom-Algebra Sg Th Alg1 Alg2 F op v')
+    where
+    f = map-hom-Algebra Sg Th Alg1 Alg2 F
+    map-hom-Algebra-lemma :
+     ( n : ℕ) →
+     ( v v' : vec (type-Algebra Sg Th Alg1) n) →
+     ( relation-holds-all-vec Sg Th Alg1 eq-rel-kernel-hom-Algebra v v') →
+     (map-vec f v) ＝ (map-vec f v')
+    map-hom-Algebra-lemma zero-ℕ empty-vec empty-vec p = refl
+    map-hom-Algebra-lemma (succ-ℕ n) (x ∷ v) (x' ∷ v') (p , p') =
+     ap-binary (_∷_) p (map-hom-Algebra-lemma n v v' p')
+```