diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index e62f9f5..4186068 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -12,6 +12,7 @@ open import Numbers.Integers.Integers
 open import Numbers.Integers.RingStructure.EuclideanDomain
 
 open import Lists.Lists
+open import Lists.Filter.AllTrue
 
 open import Groups.Groups
 open import Groups.Abelian.Lemmas
diff --git a/Groups/FinitePermutations.agda b/Groups/FinitePermutations.agda
index c0934bf..b509ec2 100644
--- a/Groups/FinitePermutations.agda
+++ b/Groups/FinitePermutations.agda
@@ -10,88 +10,89 @@ open import Setoids.Setoids
 --open import Groups.Actions
 
 module Groups.FinitePermutations where
-  allInsertions : {a : _} {A : Set a} (x : A) (l : List A) → List (List A)
-  allInsertions x [] = [ x ] :: []
-  allInsertions x (y :: l) = (x :: (y :: l)) :: (map (λ i → y :: i) (allInsertions x l))
 
-  permutations : {a : _} {A : Set a} (l : List A) → List (List A)
-  permutations [] = [ [] ]
-  permutations (x :: l) = flatten (map (allInsertions x) (permutations l))
+allInsertions : {a : _} {A : Set a} (x : A) (l : List A) → List (List A)
+allInsertions x [] = [ x ] :: []
+allInsertions x (y :: l) = (x :: (y :: l)) :: (map (λ i → y :: i) (allInsertions x l))
 
-  factorial : ℕ → ℕ
-  factorial zero = 1
-  factorial (succ n) = (succ n) *N factorial n
+permutations : {a : _} {A : Set a} (l : List A) → List (List A)
+permutations [] = [ [] ]
+permutations (x :: l) = flatten (map (allInsertions x) (permutations l))
 
-  factCheck : factorial 5 ≡ 120
-  factCheck = refl
+factorial : ℕ → ℕ
+factorial zero = 1
+factorial (succ n) = (succ n) *N factorial n
 
-  allInsertionsLength : {a : _} {A : Set a} (x : A) (l : List A) → length (allInsertions x l) ≡ succ (length l)
-  allInsertionsLength x [] = refl
-  allInsertionsLength x (y :: l) = applyEquality succ (transitivity (equalityCommutative (lengthMap (allInsertions x l) {f = y ::_})) (allInsertionsLength x l))
+factCheck : factorial 5 ≡ 120
+factCheck = refl
 
-  allInsertionsLength' : {a : _} {A : Set a} (x : A) (l : List A) → allTrue (λ i → length i ≡ succ (length l)) (allInsertions x l)
-  allInsertionsLength' x [] = refl ,, record {}
-  allInsertionsLength' x (y :: l) with allInsertionsLength' x l
-  ... | bl = refl ,, allTrueMap (λ i → length i ≡ succ (succ (length l))) (y ::_) (allInsertions x l) (allTrueExtension (λ z → length z ≡ succ (length l)) ((λ i → length i ≡ succ (succ (length l))) ∘ (y ::_)) (allInsertions x l) (λ {x} → λ p → applyEquality succ p) bl)
+allInsertionsLength : {a : _} {A : Set a} (x : A) (l : List A) → length (allInsertions x l) ≡ succ (length l)
+allInsertionsLength x [] = refl
+allInsertionsLength x (y :: l) = applyEquality succ (transitivity (equalityCommutative (lengthMap (allInsertions x l) {f = y ::_})) (allInsertionsLength x l))
 
-  permutationsCheck : permutations (3 :: 4 :: []) ≡ (3 :: 4 :: []) :: (4 :: 3 :: []) :: []
-  permutationsCheck = refl
+allInsertionsLength' : {a : _} {A : Set a} (x : A) (l : List A) → allTrue (λ i → length i ≡ succ (length l)) (allInsertions x l)
+allInsertionsLength' x [] = refl ,, record {}
+allInsertionsLength' x (y :: l) with allInsertionsLength' x l
+... | bl = refl ,, allTrueMap (λ i → length i ≡ succ (succ (length l))) (y ::_) (allInsertions x l) (allTrueExtension (λ z → length z ≡ succ (length l)) ((λ i → length i ≡ succ (succ (length l))) ∘ (y ::_)) (allInsertions x l) (λ {x} → λ p → applyEquality succ p) bl)
 
-  permsAllSameLength : {a : _} {A : Set a} (l : List A) → allTrue (λ i → length i ≡ length l) (permutations l)
-  permsAllSameLength [] = refl ,, record {}
-  permsAllSameLength (x :: l) with permsAllSameLength l
-  ... | bl = allTrueFlatten (λ i → length i ≡ succ (length l)) (map (allInsertions x) (permutations l)) (allTrueMap (allTrue (λ i → length i ≡ succ (length l))) (allInsertions x) (permutations l) (allTrueExtension (λ z → length z ≡ length l) (allTrue (λ i → length i ≡ succ (length l)) ∘ allInsertions x) (permutations l) lemma bl))
-    where
-      lemma : {m : List _} → (lenM=lenL : length m ≡ length l) → allTrue (λ i → length i ≡ succ (length l)) (allInsertions x m)
-      lemma {m} lm=ll rewrite equalityCommutative lm=ll = allInsertionsLength' x m
+permutationsCheck : permutations (3 :: 4 :: []) ≡ (3 :: 4 :: []) :: (4 :: 3 :: []) :: []
+permutationsCheck = refl
 
-  allTrueEqual : {a b : _} {A : Set a} {B : Set b} (f : A → B) (equalTo : B) (l : List A) → allTrue (λ i → f i ≡ equalTo) l → map f l ≡ replicate (length l) equalTo
-  allTrueEqual f equalTo [] pr = refl
-  allTrueEqual f equalTo (x :: l) (fst ,, snd) rewrite fst | allTrueEqual f equalTo l snd = refl
+permsAllSameLength : {a : _} {A : Set a} (l : List A) → allTrue (λ i → length i ≡ length l) (permutations l)
+permsAllSameLength [] = refl ,, record {}
+permsAllSameLength (x :: l) with permsAllSameLength l
+... | bl = allTrueFlatten (λ i → length i ≡ succ (length l)) (map (allInsertions x) (permutations l)) (allTrueMap (allTrue (λ i → length i ≡ succ (length l))) (allInsertions x) (permutations l) (allTrueExtension (λ z → length z ≡ length l) (allTrue (λ i → length i ≡ succ (length l)) ∘ allInsertions x) (permutations l) lemma bl))
+  where
+    lemma : {m : List _} → (lenM=lenL : length m ≡ length l) → allTrue (λ i → length i ≡ succ (length l)) (allInsertions x m)
+    lemma {m} lm=ll rewrite equalityCommutative lm=ll = allInsertionsLength' x m
 
-  totalReplicate : (l len : ℕ) → total (replicate len l) ≡ l *N len
-  totalReplicate l zero rewrite multiplicationNIsCommutative l 0 = refl
-  totalReplicate l (succ len) rewrite totalReplicate l len | multiplicationNIsCommutative l (succ len) = applyEquality (l +N_) (multiplicationNIsCommutative l len)
+allTrueEqual : {a b : _} {A : Set a} {B : Set b} (f : A → B) (equalTo : B) (l : List A) → allTrue (λ i → f i ≡ equalTo) l → map f l ≡ replicate (length l) equalTo
+allTrueEqual f equalTo [] pr = refl
+allTrueEqual f equalTo (x :: l) (fst ,, snd) rewrite fst | allTrueEqual f equalTo l snd = refl
 
-  permsLen : {a : _} {A : Set a} (l : List A) → length (permutations l) ≡ factorial (length l)
-  permsLen [] = refl
-  permsLen (x :: l) = transitivity (lengthFlatten (map (allInsertions x) (permutations l))) (transitivity (applyEquality total (mapMap (permutations l))) (transitivity (applyEquality total (mapExtension (permutations l) (length ∘ allInsertions x) (succ ∘ length) λ {y} → allInsertionsLength x y)) (transitivity (applyEquality total lemma) (transitivity (totalReplicate (succ (length l)) (length (permutations l))) ans))))
-    where
-      lemma : map (λ a → succ (length a)) (permutations l) ≡ replicate (length (permutations l)) (succ (length l))
-      lemma = allTrueEqual (λ a → succ (length a)) (succ (length l)) (permutations l) (allTrueExtension (λ z → length z ≡ length l) (λ i → succ (length i) ≡ succ (length l)) (permutations l) (λ pr → applyEquality succ pr) (permsAllSameLength l))
-      ans : length (permutations l) +N length l *N length (permutations l) ≡ factorial (length l) +N length l *N factorial (length l)
-      ans rewrite permsLen l = refl
+totalReplicate : (l len : ℕ) → fold _+N_ 0 (replicate len l) ≡ l *N len
+totalReplicate l zero rewrite multiplicationNIsCommutative l 0 = refl
+totalReplicate l (succ len) rewrite totalReplicate l len | multiplicationNIsCommutative l (succ len) = applyEquality (l +N_) (multiplicationNIsCommutative l len)
 
-  --act : GroupAction (symmetricGroup (symmetricSetoid (reflSetoid (FinSet n))))
-  --act = ?
+permsLen : {a : _} {A : Set a} (l : List A) → length (permutations l) ≡ factorial (length l)
+permsLen [] = refl
+permsLen (x :: l) = transitivity (lengthFlatten (map (allInsertions x) (permutations l))) (transitivity (applyEquality (fold _+N_ 0) (mapMap (permutations l))) (transitivity (applyEquality (fold _+N_ 0) (mapExtension (permutations l) (length ∘ allInsertions x) (succ ∘ length) λ {y} → allInsertionsLength x y)) (transitivity (applyEquality (fold _+N_ 0) lemma) (transitivity (totalReplicate (succ (length l)) (length (permutations l))) ans))))
+  where
+    lemma : map (λ a → succ (length a)) (permutations l) ≡ replicate (length (permutations l)) (succ (length l))
+    lemma = allTrueEqual (λ a → succ (length a)) (succ (length l)) (permutations l) (allTrueExtension (λ z → length z ≡ length l) (λ i → succ (length i) ≡ succ (length l)) (permutations l) (λ pr → applyEquality succ pr) (permsAllSameLength l))
+    ans : length (permutations l) +N length l *N length (permutations l) ≡ factorial (length l) +N length l *N factorial (length l)
+    ans rewrite permsLen l = refl
+
+--act : GroupAction (symmetricGroup (symmetricSetoid (reflSetoid (FinSet n))))
+--act = ?
 
 {- TODO: show that symmetricGroup acts in the obvious way on permutations FinSet
-  listElements : {a : _} {A : Set a} (l : List A) → Set
-  listElements [] = False
-  listElements (x :: l) = True || listElements l
+listElements : {a : _} {A : Set a} (l : List A) → Set
+listElements [] = False
+listElements (x :: l) = True || listElements l
 
-  listElement : {a : _} {A : Set a} {l : List A} (elt : listElements l) → A
-  listElement {l = []} ()
-  listElement {l = x :: l} (inl record {}) = x
-  listElement {l = x :: l} (inr elt) = listElement {l = l} elt
+listElement : {a : _} {A : Set a} {l : List A} (elt : listElements l) → A
+listElement {l = []} ()
+listElement {l = x :: l} (inl record {}) = x
+listElement {l = x :: l} (inr elt) = listElement {l = l} elt
 
-  backwardRange : ℕ → List ℕ
-  backwardRange zero = []
-  backwardRange (succ n) = n :: backwardRange n
+backwardRange : ℕ → List ℕ
+backwardRange zero = []
+backwardRange (succ n) = n :: backwardRange n
 
-  backwardRangeLength : {n : ℕ} → length (backwardRange n) ≡ n
-  backwardRangeLength {zero} = refl
-  backwardRangeLength {succ n} rewrite backwardRangeLength {n} = refl
+backwardRangeLength : {n : ℕ} → length (backwardRange n) ≡ n
+backwardRangeLength {zero} = refl
+backwardRangeLength {succ n} rewrite backwardRangeLength {n} = refl
 
-  applyPermutation : {n : ℕ} → (f : FinSet n → FinSet n) → listElements (permutations (backwardRange n)) → listElements (permutations (backwardRange n))
-  applyPermutation {zero} f (inl record {}) = inl (record {})
-  applyPermutation {zero} f (inr ())
-  applyPermutation {succ n} f elt = {!!}
+applyPermutation : {n : ℕ} → (f : FinSet n → FinSet n) → listElements (permutations (backwardRange n)) → listElements (permutations (backwardRange n))
+applyPermutation {zero} f (inl record {}) = inl (record {})
+applyPermutation {zero} f (inr ())
+applyPermutation {succ n} f elt = {!!}
 
-  finitePermutations : (n : ℕ) → SetoidToSet (symmetricSetoid (reflSetoid (FinSet n))) (listElements (permutations (backwardRange n)))
-  SetoidToSet.project (finitePermutations n) (sym {f} fBij) = {!!}
-  SetoidToSet.wellDefined (finitePermutations n) = {!!}
-  SetoidToSet.surj (finitePermutations n) = {!!}
-  SetoidToSet.inj (finitePermutations n) = {!!}
+finitePermutations : (n : ℕ) → SetoidToSet (symmetricSetoid (reflSetoid (FinSet n))) (listElements (permutations (backwardRange n)))
+SetoidToSet.project (finitePermutations n) (sym {f} fBij) = {!!}
+SetoidToSet.wellDefined (finitePermutations n) = {!!}
+SetoidToSet.surj (finitePermutations n) = {!!}
+SetoidToSet.inj (finitePermutations n) = {!!}
 
 -}
diff --git a/Lists/Concat.agda b/Lists/Concat.agda
new file mode 100644
index 0000000..cdd43a9
--- /dev/null
+++ b/Lists/Concat.agda
@@ -0,0 +1,25 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Functions
+open import Lists.Definition
+open import Lists.Length
+open import Numbers.Naturals.Semiring
+
+module Lists.Concat where
+
+appendEmptyList : {a : _} → {A : Set a} → (l : List A) → (l ++ [] ≡ l)
+appendEmptyList [] = refl
+appendEmptyList (x :: l) = applyEquality (_::_ x) (appendEmptyList l)
+
+concatAssoc : {a : _} → {A : Set a} → (x : List A) → (y : List A) → (z : List A) → ((x ++ y) ++ z) ≡ x ++ (y ++ z)
+concatAssoc [] m n = refl
+concatAssoc (x :: l) m n = applyEquality (_::_ x) (concatAssoc l m n)
+
+canMovePrepend : {a : _} → {A : Set a} → (l : A) → (x : List A) (y : List A) → ((l :: x) ++ y ≡ l :: (x ++ y))
+canMovePrepend l [] n = refl
+canMovePrepend l (x :: m) n = refl
+
+lengthConcat : {a : _} {A : Set a} (l1 l2 : List A) → length (l1 ++ l2) ≡ length l1 +N length l2
+lengthConcat [] l2 = refl
+lengthConcat (x :: l1) l2 = applyEquality succ (lengthConcat l1 l2)
diff --git a/Lists/Definition.agda b/Lists/Definition.agda
new file mode 100644
index 0000000..0fccbf0
--- /dev/null
+++ b/Lists/Definition.agda
@@ -0,0 +1,18 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Functions
+
+module Lists.Definition {a : _} where
+
+data List (A : Set a) : Set a where
+  [] : List A
+  _::_ : (x : A) (xs : List A) → List A
+infixr 10 _::_
+
+[_] : {A : Set a} → (a : A) → List A
+[ a ] = a :: []
+
+_++_ : {A : Set a} → List A → List A → List A
+[] ++ m = m
+(x :: l) ++ m = x :: (l ++ m)
diff --git a/Lists/Filter/AllTrue.agda b/Lists/Filter/AllTrue.agda
new file mode 100644
index 0000000..f2836c7
--- /dev/null
+++ b/Lists/Filter/AllTrue.agda
@@ -0,0 +1,38 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Functions
+open import Lists.Definition
+open import Lists.Monad
+
+module Lists.Filter.AllTrue where
+
+allTrue : {a b : _} {A : Set a} (f : A → Set b) (l : List A) → Set b
+allTrue f [] = True'
+allTrue f (x :: l) = f x && allTrue f l
+
+allTrueConcat : {a b : _} {A : Set a} (f : A → Set b) (l m : List A) → allTrue f l → allTrue f m → allTrue f (l ++ m)
+allTrueConcat f [] m fl fm = fm
+allTrueConcat f (x :: l) m (fst ,, snd) fm = fst ,, allTrueConcat f l m snd fm
+
+allTrueFlatten : {a b : _} {A : Set a} (f : A → Set b) (l : List (List A)) → allTrue (λ i → allTrue f i) l → allTrue f (flatten l)
+allTrueFlatten f [] pr = record {}
+allTrueFlatten f ([] :: ls) pr = allTrueFlatten f ls (_&&_.snd pr)
+allTrueFlatten f ((x :: l) :: ls) ((fx ,, fl) ,, snd) = fx ,, allTrueConcat f l (flatten ls) fl (allTrueFlatten f ls snd)
+
+allTrueMap : {a b c : _} {A : Set a} {B : Set b} (pred : B → Set c) (f : A → B) (l : List A) → allTrue (pred ∘ f) l → allTrue pred (map f l)
+allTrueMap pred f [] pr = record {}
+allTrueMap pred f (x :: l) pr = _&&_.fst pr ,, allTrueMap pred f l (_&&_.snd pr)
+
+allTrueExtension : {a b : _} {A : Set a} (f g : A → Set b) (l : List A) → ({x : A} → f x → g x) → allTrue f l → allTrue g l
+allTrueExtension f g [] pred t = record {}
+allTrueExtension f g (x :: l) pred (fg ,, snd) = pred {x} fg ,, allTrueExtension f g l pred snd
+
+allTrueTail : {a b : _} {A : Set a} (pred : A → Set b) (x : A) (l : List A) → allTrue pred (x :: l) → allTrue pred l
+allTrueTail pred x l (fst ,, snd) = snd
+
+filter : {a : _} {A : Set a} (l : List A) (f : A → Bool) → List A
+filter [] f = []
+filter (x :: l) f with f x
+filter (x :: l) f | BoolTrue = x :: filter l f
+filter (x :: l) f | BoolFalse = filter l f
diff --git a/Lists/Fold/Fold.agda b/Lists/Fold/Fold.agda
new file mode 100644
index 0000000..36254f3
--- /dev/null
+++ b/Lists/Fold/Fold.agda
@@ -0,0 +1,11 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Functions
+open import Lists.Definition
+
+module Lists.Fold.Fold {a b : _} {A : Set a} {B : Set b} where
+
+fold : (f : A → B → B) → B → List A → B
+fold f default [] = default
+fold f default (x :: l) = f x (fold f default l)
diff --git a/Lists/Length.agda b/Lists/Length.agda
new file mode 100644
index 0000000..bce43fd
--- /dev/null
+++ b/Lists/Length.agda
@@ -0,0 +1,22 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Functions
+open import Numbers.Naturals.Semiring -- for length
+open import Numbers.Naturals.Order
+open import Semirings.Definition
+open import Lists.Definition
+open import Lists.Fold.Fold
+
+module Lists.Length where
+
+length : {a : _} {A : Set a} (l : List A) → ℕ
+length [] = zero
+length (x :: l) = succ (length l)
+
+length' : {a : _} {A : Set a} → (l : List A) → ℕ
+length' = fold (λ _ → succ) 0
+
+length=length' : {a : _} {A : Set a} (l : List A) → length l ≡ length' l
+length=length' [] = refl
+length=length' (x :: l) = applyEquality succ (length=length' l)
diff --git a/Lists/Lists.agda b/Lists/Lists.agda
index cfe637c..7618676 100644
--- a/Lists/Lists.agda
+++ b/Lists/Lists.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --warning=error --without-K #-}
+{-# OPTIONS --warning=error --safe --without-K #-}
 
 open import LogicalFormulae
 open import Functions
@@ -9,149 +9,19 @@ open import Maybe
 
 module Lists.Lists where
 
-data List {a} (A : Set a) : Set a where
-  [] : List A
-  _::_ : (x : A) (xs : List A) → List A
-infixr 10 _::_
-
-[_] : {a : _} → {A : Set a} → (a : A) → List A
-[ a ] = a :: []
-
-_++_ : {a : _} → {A : Set a} → List A → List A → List A
-[] ++ m = m
-(x :: l) ++ m = x :: (l ++ m)
-
-appendEmptyList : {a : _} → {A : Set a} → (l : List A) → (l ++ [] ≡ l)
-appendEmptyList [] = refl
-appendEmptyList (x :: l) = applyEquality (_::_ x) (appendEmptyList l)
-
-concatAssoc : {a : _} → {A : Set a} → (x : List A) → (y : List A) → (z : List A) → ((x ++ y) ++ z) ≡ x ++ (y ++ z)
-concatAssoc [] m n = refl
-concatAssoc (x :: l) m n = applyEquality (_::_ x) (concatAssoc l m n)
-
-canMovePrepend : {a : _} → {A : Set a} → (l : A) → {m n : ℕ} → (x : List A) (y : List A) → ((l :: x) ++ y ≡ l :: (x ++ y))
-canMovePrepend l [] n = refl
-canMovePrepend l (x :: m) n = refl
-
-rev : {a : _} → {A : Set a} → List A → List A
-rev [] = []
-rev (x :: l) = (rev l) ++ [ x ]
-
-revIsHom : {a : _} → {A : Set a} → (l1 : List A) → (l2 : List A) → (rev (l1 ++ l2) ≡ (rev l2) ++ (rev l1))
-revIsHom l1 [] = applyEquality rev (appendEmptyList l1)
-revIsHom [] (x :: l2) with (rev l2 ++ [ x ])
-... | r = equalityCommutative (appendEmptyList r)
-revIsHom (w :: l1) (x :: l2) = transitivity t (equalityCommutative s)
-  where
-    s : ((rev l2 ++ [ x ]) ++ (rev l1 ++ [ w ])) ≡ (((rev l2 ++ [ x ]) ++ rev l1) ++ [ w ])
-    s = equalityCommutative (concatAssoc (rev l2 ++ (x :: [])) (rev l1) ([ w ]))
-    t' : rev (l1 ++ (x :: l2)) ≡ rev (x :: l2) ++ rev l1
-    t' = revIsHom l1 (x :: l2)
-    t : (rev (l1 ++ (x :: l2)) ++ [ w ]) ≡ ((rev l2 ++ [ x ]) ++ rev l1) ++ [ w ]
-    t = applyEquality (λ r → r ++ [ w ]) {rev (l1 ++ (x :: l2))} {((rev l2) ++ [ x ]) ++ rev l1} (transitivity t' (applyEquality (λ r → r ++ rev l1) {rev l2 ++ (x :: [])} {rev l2 ++ (x :: [])} refl))
-
-revRevIsId : {a : _} → {A : Set a} → (l : List A) → (rev (rev l) ≡ l)
-revRevIsId [] = refl
-revRevIsId (x :: l) = t
-  where
-    s : rev (rev l ++ [ x ] ) ≡ [ x ] ++ rev (rev l)
-    s = revIsHom (rev l) [ x ]
-    t : rev (rev l ++ [ x ] ) ≡ [ x ] ++ l
-    t = identityOfIndiscernablesRight _≡_ s (applyEquality (λ n → [ x ] ++ n) (revRevIsId l))
-
-fold : {a b : _} {A : Set a} {B : Set b} (f : A → B → B) → B → List A → B
-fold f default [] = default
-fold f default (x :: l) = f x (fold f default l)
-
-map : {a : _} → {b : _} → {A : Set a} → {B : Set b} → (f : A → B) → List A → List B
-map f [] = []
-map f (x :: list) = (f x) :: (map f list)
-
-map' : {a : _} → {b : _} → {A : Set a} → {B : Set b} → (f : A → B) → List A → List B
-map' f = fold (λ a → (f a) ::_ ) []
-
-map=map' : {a : _} → {b : _} → {A : Set a} → {B : Set b} → (f : A → B) → (l : List A) → (map f l ≡ map' f l)
-map=map' f [] = refl
-map=map' f (x :: l) with map=map' f l
-... | bl = applyEquality (f x ::_) bl
-
-flatten : {a : _} {A : Set a} → (l : List (List A)) → List A
-flatten [] = []
-flatten (l :: ls) = l ++ flatten ls
-
-flatten' : {a : _} {A : Set a} → (l : List (List A)) → List A
-flatten' = fold _++_ []
-
-flatten=flatten' : {a : _} {A : Set a} (l : List (List A)) → flatten l ≡ flatten' l
-flatten=flatten' [] = refl
-flatten=flatten' (l :: ls) = applyEquality (l ++_) (flatten=flatten' ls)
-
-length : {a : _} {A : Set a} (l : List A) → ℕ
-length [] = zero
-length (x :: l) = succ (length l)
-
-length' : {a : _} {A : Set a} → (l : List A) → ℕ
-length' = fold (λ _ → succ) 0
-
-length=length' : {a : _} {A : Set a} (l : List A) → length l ≡ length' l
-length=length' [] = refl
-length=length' (x :: l) = applyEquality succ (length=length' l)
-
-total : List ℕ → ℕ
-total [] = zero
-total (x :: l) = x +N total l
-
-total' : List ℕ → ℕ
-total' = fold _+N_ 0
-
-lengthConcat : {a : _} {A : Set a} (l1 l2 : List A) → length (l1 ++ l2) ≡ length l1 +N length l2
-lengthConcat [] l2 = refl
-lengthConcat (x :: l1) l2 = applyEquality succ (lengthConcat l1 l2)
-
-lengthFlatten : {a : _} {A : Set a} (l : List (List A)) → length (flatten l) ≡ total (map length l)
-lengthFlatten [] = refl
-lengthFlatten (l :: ls) rewrite lengthConcat l (flatten ls) | lengthFlatten ls = refl
-
-lengthMap : {a b : _} {A : Set a} {B : Set b} → (l : List A) → {f : A → B} → length l ≡ length (map f l)
-lengthMap [] {f} = refl
-lengthMap (x :: l) {f} rewrite lengthMap l {f} = refl
-
-mapMap : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → (l : List A) → {f : A → B} {g : B → C} → map g (map f l) ≡ map (g ∘ f) l
-mapMap [] = refl
-mapMap (x :: l) {f = f} {g} rewrite mapMap l {f} {g} = refl
-
-mapExtension : {a b : _} {A : Set a} {B : Set b} (l : List A) (f g : A → B) → ({x : A} → (f x ≡ g x)) → map f l ≡ map g l
-mapExtension [] f g pr = refl
-mapExtension (x :: l) f g pr rewrite mapExtension l f g pr | pr {x} = refl
+open import Lists.Definition public
+open import Lists.Length public
+open import Lists.Concat public
+open import Lists.Map.Map public
+open import Lists.Reversal.Reversal public
+open import Lists.Monad public
+open import Lists.Filter.AllTrue public
+open import Lists.Fold.Fold public
 
 replicate : {a : _} {A : Set a} (n : ℕ) (x : A) → List A
 replicate zero x = []
 replicate (succ n) x = x :: replicate n x
 
-allTrue : {a b : _} {A : Set a} (f : A → Set b) (l : List A) → Set b
-allTrue f [] = True'
-allTrue f (x :: l) = f x && allTrue f l
-
-allTrueConcat : {a b : _} {A : Set a} (f : A → Set b) (l m : List A) → allTrue f l → allTrue f m → allTrue f (l ++ m)
-allTrueConcat f [] m fl fm = fm
-allTrueConcat f (x :: l) m (fst ,, snd) fm = fst ,, allTrueConcat f l m snd fm
-
-allTrueFlatten : {a b : _} {A : Set a} (f : A → Set b) (l : List (List A)) → allTrue (λ i → allTrue f i) l → allTrue f (flatten l)
-allTrueFlatten f [] pr = record {}
-allTrueFlatten f ([] :: ls) pr = allTrueFlatten f ls (_&&_.snd pr)
-allTrueFlatten f ((x :: l) :: ls) ((fx ,, fl) ,, snd) = fx ,, allTrueConcat f l (flatten ls) fl (allTrueFlatten f ls snd)
-
-allTrueMap : {a b c : _} {A : Set a} {B : Set b} (pred : B → Set c) (f : A → B) (l : List A) → allTrue (pred ∘ f) l → allTrue pred (map f l)
-allTrueMap pred f [] pr = record {}
-allTrueMap pred f (x :: l) pr = _&&_.fst pr ,, allTrueMap pred f l (_&&_.snd pr)
-
-allTrueExtension : {a b : _} {A : Set a} (f g : A → Set b) (l : List A) → ({x : A} → f x → g x) → allTrue f l → allTrue g l
-allTrueExtension f g [] pred t = record {}
-allTrueExtension f g (x :: l) pred (fg ,, snd) = pred {x} fg ,, allTrueExtension f g l pred snd
-
-allTrueTail : {a b : _} {A : Set a} (pred : A → Set b) (x : A) (l : List A) → allTrue pred (x :: l) → allTrue pred l
-allTrueTail pred x l (fst ,, snd) = snd
-
 head : {a : _} {A : Set a} (l : List A) (pr : 0 <N length l) → A
 head [] (le x ())
 head (x :: l) pr = x
@@ -160,12 +30,6 @@ lengthRev : {a : _} {A : Set a} (l : List A) → length (rev l) ≡ length l
 lengthRev [] = refl
 lengthRev (x :: l) rewrite lengthConcat (rev l) (x :: []) | lengthRev l | Semiring.commutative ℕSemiring (length l) 1 = refl
 
-filter : {a : _} {A : Set a} (l : List A) (f : A → Bool) → List A
-filter [] f = []
-filter (x :: l) f with f x
-filter (x :: l) f | BoolTrue = x :: filter l f
-filter (x :: l) f | BoolFalse = filter l f
-
 listLast : {a : _} {A : Set a} (l : List A) → Maybe A
 listLast [] = no
 listLast (x :: []) = yes x
@@ -175,7 +39,3 @@ listZip : {a b c : _} {A : Set a} {B : Set b} {C : Set c} (f : A → B → C) 
 listZip f f1 f2 [] l2 = map f2 l2
 listZip f f1 f2 (x :: l1) [] = map f1 (x :: l1)
 listZip f f1 f2 (x :: l1) (y :: l2) = (f x y) :: listZip f f1 f2 l1 l2
-
-mapId : {a : _} {A : Set a} (l : List A) → map id l ≡ l
-mapId [] = refl
-mapId (x :: l) rewrite mapId l = refl
diff --git a/Lists/Map/Map.agda b/Lists/Map/Map.agda
new file mode 100644
index 0000000..1668510
--- /dev/null
+++ b/Lists/Map/Map.agda
@@ -0,0 +1,37 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Functions
+open import Lists.Definition
+open import Lists.Fold.Fold
+open import Lists.Length
+
+module Lists.Map.Map where
+
+map : {a b : _} {A : Set a} {B : Set b} (f : A → B) → List A → List B
+map f [] = []
+map f (x :: list) = (f x) :: (map f list)
+
+map' : {a b : _} {A : Set a} {B : Set b} (f : A → B) → List A → List B
+map' f = fold (λ a → (f a) ::_ ) []
+
+map=map' : {a b : _} {A : Set a} {B : Set b} (f : A → B) → (l : List A) → (map f l ≡ map' f l)
+map=map' f [] = refl
+map=map' f (x :: l) with map=map' f l
+... | bl = applyEquality (f x ::_) bl
+
+mapId : {a : _} {A : Set a} (l : List A) → map id l ≡ l
+mapId [] = refl
+mapId (x :: l) rewrite mapId l = refl
+
+mapMap : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → (l : List A) → {f : A → B} {g : B → C} → map g (map f l) ≡ map (g ∘ f) l
+mapMap [] = refl
+mapMap (x :: l) {f = f} {g} rewrite mapMap l {f} {g} = refl
+
+mapExtension : {a b : _} {A : Set a} {B : Set b} (l : List A) (f g : A → B) → ({x : A} → (f x ≡ g x)) → map f l ≡ map g l
+mapExtension [] f g pr = refl
+mapExtension (x :: l) f g pr rewrite mapExtension l f g pr | pr {x} = refl
+
+lengthMap : {a b : _} {A : Set a} {B : Set b} → (l : List A) → {f : A → B} → length l ≡ length (map f l)
+lengthMap [] {f} = refl
+lengthMap (x :: l) {f} rewrite lengthMap l {f} = refl
diff --git a/Lists/Monad.agda b/Lists/Monad.agda
new file mode 100644
index 0000000..85f468e
--- /dev/null
+++ b/Lists/Monad.agda
@@ -0,0 +1,28 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Functions
+open import Lists.Definition
+open import Lists.Fold.Fold
+open import Lists.Concat
+open import Lists.Length
+open import Numbers.Naturals.Semiring
+
+module Lists.Monad where
+
+open import Lists.Map.Map public
+
+flatten : {a : _} {A : Set a} → (l : List (List A)) → List A
+flatten [] = []
+flatten (l :: ls) = l ++ flatten ls
+
+flatten' : {a : _} {A : Set a} → (l : List (List A)) → List A
+flatten' = fold _++_ []
+
+flatten=flatten' : {a : _} {A : Set a} (l : List (List A)) → flatten l ≡ flatten' l
+flatten=flatten' [] = refl
+flatten=flatten' (l :: ls) = applyEquality (l ++_) (flatten=flatten' ls)
+
+lengthFlatten : {a : _} {A : Set a} (l : List (List A)) → length (flatten l) ≡ (fold _+N_ zero (map length l))
+lengthFlatten [] = refl
+lengthFlatten (l :: ls) rewrite lengthConcat l (flatten ls) | lengthFlatten ls = refl
diff --git a/Lists/Permutations.agda b/Lists/Permutations.agda
new file mode 100644
index 0000000..e6f9dfe
--- /dev/null
+++ b/Lists/Permutations.agda
@@ -0,0 +1,45 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Sets.EquivalenceRelations
+open import Functions
+open import Lists.Definition
+open import Lists.Fold.Fold
+open import Lists.Concat
+open import Lists.Length
+open import Setoids.Setoids
+open import Maybe
+open import Numbers.Naturals.Semiring
+
+module Lists.Permutations {a b : _} {A : Set a} (S : Setoid {a} {b} A) (decidable : (x y : A) → (Setoid._∼_ S x y) || ((Setoid._∼_ S x y) → False)) where
+
+open Setoid S
+open Equivalence eq
+
+indexOf : (a : A) → (l : List A) → Maybe ℕ
+indexOf a [] = no
+indexOf a (x :: l) with decidable a x
+... | inl eq = yes 0
+... | inr noneq = mapMaybe succ (indexOf a l)
+
+eltAt : (n : ℕ) → (l : List A) → Maybe A
+eltAt n [] = no
+eltAt zero (x :: l) = yes x
+eltAt (succ n) (x :: l) = eltAt n l
+
+indexOfIsIndexOf : (a : A) → (l : List A) → {n : ℕ} → indexOf a l ≡ yes n → Sg A (λ b → (eltAt n l ≡ yes b) && (b ∼ a))
+indexOfIsIndexOf a (x :: l) {n} ind with decidable a x
+indexOfIsIndexOf a (x :: l) {.0} refl | inl a=x = x , (refl ,, symmetric a=x)
+indexOfIsIndexOf a (x :: l) {zero} ind | inr a!=x with indexOf a l
+indexOfIsIndexOf a (x :: l) {zero} () | inr a!=x | no
+indexOfIsIndexOf a (x :: l) {zero} () | inr a!=x | yes _
+indexOfIsIndexOf a (x :: l) {succ n} ind | inr a!=x with mapMaybePreservesYes ind
+... | m , (pr ,, z=n) = indexOfIsIndexOf a l (transitivity pr (applyEquality yes (succInjective z=n)))
+
+Permutation : (List A) → (List A) → Set
+Permutation [] [] = True
+Permutation [] (x :: l2) = False
+Permutation (x :: l1) [] = False
+Permutation (a :: as) (b :: bs) with decidable a b
+Permutation (a :: as) (b :: bs) | inl a=b = Permutation as bs
+Permutation (a :: as) (b :: bs) | inr a!=b = {!!}
diff --git a/Lists/Reversal/Reversal.agda b/Lists/Reversal/Reversal.agda
new file mode 100644
index 0000000..93df361
--- /dev/null
+++ b/Lists/Reversal/Reversal.agda
@@ -0,0 +1,38 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Functions
+open import Numbers.Naturals.Semiring -- for length
+open import Numbers.Naturals.Order
+open import Semirings.Definition
+open import Maybe
+open import Lists.Definition
+open import Lists.Concat
+
+module Lists.Reversal.Reversal where
+
+rev : {a : _} → {A : Set a} → List A → List A
+rev [] = []
+rev (x :: l) = (rev l) ++ [ x ]
+
+revIsHom : {a : _} → {A : Set a} → (l1 : List A) → (l2 : List A) → (rev (l1 ++ l2) ≡ (rev l2) ++ (rev l1))
+revIsHom l1 [] = applyEquality rev (appendEmptyList l1)
+revIsHom [] (x :: l2) with (rev l2 ++ [ x ])
+... | r = equalityCommutative (appendEmptyList r)
+revIsHom (w :: l1) (x :: l2) = transitivity t (equalityCommutative s)
+  where
+    s : ((rev l2 ++ [ x ]) ++ (rev l1 ++ [ w ])) ≡ (((rev l2 ++ [ x ]) ++ rev l1) ++ [ w ])
+    s = equalityCommutative (concatAssoc (rev l2 ++ (x :: [])) (rev l1) ([ w ]))
+    t' : rev (l1 ++ (x :: l2)) ≡ rev (x :: l2) ++ rev l1
+    t' = revIsHom l1 (x :: l2)
+    t : (rev (l1 ++ (x :: l2)) ++ [ w ]) ≡ ((rev l2 ++ [ x ]) ++ rev l1) ++ [ w ]
+    t = applyEquality (λ r → r ++ [ w ]) {rev (l1 ++ (x :: l2))} {((rev l2) ++ [ x ]) ++ rev l1} (transitivity t' (applyEquality (λ r → r ++ rev l1) {rev l2 ++ (x :: [])} {rev l2 ++ (x :: [])} refl))
+
+revRevIsId : {a : _} → {A : Set a} → (l : List A) → (rev (rev l) ≡ l)
+revRevIsId [] = refl
+revRevIsId (x :: l) = t
+  where
+    s : rev (rev l ++ [ x ] ) ≡ [ x ] ++ rev (rev l)
+    s = revIsHom (rev l) [ x ]
+    t : rev (rev l ++ [ x ] ) ≡ [ x ] ++ l
+    t = identityOfIndiscernablesRight _≡_ s (applyEquality (λ n → [ x ] ++ n) (revRevIsId l))
diff --git a/Maybe.agda b/Maybe.agda
index 5daa33d..f7edbcd 100644
--- a/Maybe.agda
+++ b/Maybe.agda
@@ -4,36 +4,41 @@ open import LogicalFormulae
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
 module Maybe where
-  data Maybe {a : _} (A : Set a) : Set a where
-    no : Maybe A
-    yes : A → Maybe A
 
-  joinMaybe : {a : _} → {A : Set a} → Maybe (Maybe A) → Maybe A
-  joinMaybe no = no
-  joinMaybe (yes s) = s
+data Maybe {a : _} (A : Set a) : Set a where
+  no : Maybe A
+  yes : A → Maybe A
 
-  bindMaybe : {a b : _} → {A : Set a} → {B : Set b} → Maybe A → (A → Maybe B) → Maybe B
-  bindMaybe no f = no
-  bindMaybe (yes x) f = f x
+joinMaybe : {a : _} → {A : Set a} → Maybe (Maybe A) → Maybe A
+joinMaybe no = no
+joinMaybe (yes s) = s
 
-  applyMaybe : {a b : _} → {A : Set a} → {B : Set b} → Maybe (A → B) → Maybe A → Maybe B
-  applyMaybe f no = no
-  applyMaybe no (yes x) = no
-  applyMaybe (yes f) (yes x) = yes (f x)
+bindMaybe : {a b : _} → {A : Set a} → {B : Set b} → Maybe A → (A → Maybe B) → Maybe B
+bindMaybe no f = no
+bindMaybe (yes x) f = f x
 
-  yesInjective : {a : _} → {A : Set a} → {x y : A} → (yes x ≡ yes y) → x ≡ y
-  yesInjective {a} {A} {x} {.x} refl = refl
+applyMaybe : {a b : _} → {A : Set a} → {B : Set b} → Maybe (A → B) → Maybe A → Maybe B
+applyMaybe f no = no
+applyMaybe no (yes x) = no
+applyMaybe (yes f) (yes x) = yes (f x)
 
-  mapMaybe : {a b : _} → {A : Set a} → {B : Set b} → (f : A → B) → Maybe A → Maybe B
-  mapMaybe f no = no
-  mapMaybe f (yes x) = yes (f x)
+yesInjective : {a : _} → {A : Set a} → {x y : A} → (yes x ≡ yes y) → x ≡ y
+yesInjective {a} {A} {x} {.x} refl = refl
 
-  defaultValue : {a : _} → {A : Set a} → (default : A) → Maybe A → A
-  defaultValue default no = default
-  defaultValue default (yes x) = x
+mapMaybe : {a b : _} → {A : Set a} → {B : Set b} → (f : A → B) → Maybe A → Maybe B
+mapMaybe f no = no
+mapMaybe f (yes x) = yes (f x)
 
-  noNotYes : {a : _} {A : Set a} {b : A} → (no ≡ yes b) → False
-  noNotYes ()
+defaultValue : {a : _} → {A : Set a} → (default : A) → Maybe A → A
+defaultValue default no = default
+defaultValue default (yes x) = x
 
-  mapMaybePreservesNo : {a b : _} {A : Set a} {B : Set b} {f : A → B} {x : Maybe A} → mapMaybe f x ≡ no → x ≡ no
-  mapMaybePreservesNo {f = f} {no} pr = refl
+noNotYes : {a : _} {A : Set a} {b : A} → (no ≡ yes b) → False
+noNotYes ()
+
+mapMaybePreservesNo : {a b : _} {A : Set a} {B : Set b} {f : A → B} {x : Maybe A} → mapMaybe f x ≡ no → x ≡ no
+mapMaybePreservesNo {f = f} {no} pr = refl
+
+mapMaybePreservesYes : {a b : _} {A : Set a} {B : Set b} {f : A → B} {x : Maybe A} {y : B} → mapMaybe f x ≡ yes y → Sg A (λ z → (x ≡ yes z) && (f z ≡ y))
+mapMaybePreservesYes {f = f} {x} {y} map with x
+mapMaybePreservesYes {f = f} {x} {y} map | yes z = z , (refl ,, yesInjective map)
diff --git a/Rings/Ideals/Lemmas.agda b/Rings/Ideals/Lemmas.agda
index 8a4d162..04b6dfa 100644
--- a/Rings/Ideals/Lemmas.agda
+++ b/Rings/Ideals/Lemmas.agda
@@ -70,3 +70,6 @@ Ideal.accumulatesTimes (inverseImageIsIdeal {_*2_ = _*2_} {f = f} fHom i) {g} {h
 
 memberDividesImpliesMember : {a b : A} → {c : _} → {pred : A → Set c} → (i : Ideal R pred) → pred a → a ∣ b → pred b
 memberDividesImpliesMember {a} {b} i pA (s , as=b) = Ideal.isSubset i as=b (Ideal.accumulatesTimes i pA)
+
+generatorZeroImpliesMembersZero : {x : A} → generatedIdealPred R 0R x → x ∼ 0R
+generatorZeroImpliesMembersZero {x} (a , b) = transitive (symmetric b) (transitive *Commutative timesZero)
diff --git a/Rings/Ideals/Maximal/Lemmas.agda b/Rings/Ideals/Maximal/Lemmas.agda
index 96d432e..b972b53 100644
--- a/Rings/Ideals/Maximal/Lemmas.agda
+++ b/Rings/Ideals/Maximal/Lemmas.agda
@@ -26,7 +26,9 @@ open import Rings.Ideals.Prime.Lemmas
 
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
-module Rings.Ideals.Maximal.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {pred : A → Set c} (i : Ideal R pred) (proper : A) (isProper : pred proper → False) where
+module Rings.Ideals.Maximal.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {pred : A → Set c} (i : Ideal R pred)  where
+
+open import Rings.Divisible.Definition R
 
 open Ring R
 open Group additiveGroup
@@ -56,7 +58,7 @@ Field.allInvertible (idealMaximalImpliesQuotientField max) cosetA cosetA!=0 = an
     ans'' : pred (inverse (Ring.1R (cosetRing R i)) + (ans' * cosetA))
     ans'' with ans {1R}
     ans'' | a , ((b , predCAb-a) ,, pred1-a) = Ideal.isSubset i (transitive (+WellDefined (invContravariant additiveGroup) reflexive) (transitive +Associative (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) *Commutative))) (Ideal.closedUnderPlus i (Ideal.closedUnderInverse i pred1-a) predCAb-a)
-Field.nontrivial (idealMaximalImpliesQuotientField max) 1=0 = isProper (Ideal.isSubset i (identIsIdent {proper}) (Ideal.accumulatesTimes i p))
+Field.nontrivial (idealMaximalImpliesQuotientField max) 1=0 = MaximalIdeal.notContainedIsNotContained max (Ideal.isSubset i (identIsIdent {MaximalIdeal.notContained (max {lzero})}) (Ideal.accumulatesTimes i p))
   where
     have : pred (inverse 1R)
     have = Ideal.isSubset i identRight 1=0
@@ -64,8 +66,8 @@ Field.nontrivial (idealMaximalImpliesQuotientField max) 1=0 = isProper (Ideal.is
     p = Ideal.isSubset i (invTwice additiveGroup 1R) (Ideal.closedUnderInverse i have)
 
 quotientFieldImpliesIdealMaximal : Field (cosetRing R i) → ({d : _} → MaximalIdeal i {d})
-MaximalIdeal.notContained (quotientFieldImpliesIdealMaximal f) = proper
-MaximalIdeal.notContainedIsNotContained (quotientFieldImpliesIdealMaximal f) = isProper
+MaximalIdeal.notContained (quotientFieldImpliesIdealMaximal f) = Ring.1R (cosetRing R i)
+MaximalIdeal.notContainedIsNotContained (quotientFieldImpliesIdealMaximal f) p1R = Field.nontrivial f (memberDividesImpliesMember R i p1R ((inverse 1R + 0R) , identIsIdent))
 MaximalIdeal.isMaximal (quotientFieldImpliesIdealMaximal f) {bigger} biggerIdeal contained (a , (biggerA ,, notPredA)) = Ideal.isSubset biggerIdeal identIsIdent (Ideal.accumulatesTimes biggerIdeal v)
   where
     inv : Sg A (λ t → pred (inverse 1R + (t * a)))
@@ -89,3 +91,8 @@ idealMaximalImpliesIdealPrime max = quotientIntDomImpliesIdealPrime i f'
     f = idealMaximalImpliesQuotientField max
     f' : IntegralDomain (cosetRing R i)
     f' = fieldIsIntDom f (λ p → Field.nontrivial f (Equivalence.symmetric (Setoid.eq (cosetSetoid additiveGroup (Ideal.isSubgroup i))) p))
+
+maximalIdealWellDefined : {d : _} {pred2 : A → Set d} (i2 : Ideal R pred2) → ({x : A} → pred x → pred2 x) → ({x : A} → pred2 x → pred x) → {e : _} → MaximalIdeal i {e} → MaximalIdeal i2 {e}
+MaximalIdeal.notContained (maximalIdealWellDefined i2 pToP2 p2ToP record { notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained ; isMaximal = isMaximal }) = notContained
+MaximalIdeal.notContainedIsNotContained (maximalIdealWellDefined i2 pToP2 p2ToP record { notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained ; isMaximal = isMaximal }) p2Not = notContainedIsNotContained (p2ToP p2Not)
+MaximalIdeal.isMaximal (maximalIdealWellDefined i2 pToP2 p2ToP record { notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained ; isMaximal = isMaximal }) {biggerPred} bigger pred2InBigger (r , (biggerPredR ,, notP2r)) {x} = isMaximal bigger (λ p → pred2InBigger (pToP2 p)) (r , (biggerPredR ,, λ p → notP2r (pToP2 p)))
diff --git a/Rings/Ideals/Prime/Lemmas.agda b/Rings/Ideals/Prime/Lemmas.agda
index 55dff28..313832b 100644
--- a/Rings/Ideals/Prime/Lemmas.agda
+++ b/Rings/Ideals/Prime/Lemmas.agda
@@ -64,3 +64,8 @@ PrimeIdeal.isPrime (intDomImpliesZeroIdealPrime intDom) (c , 0=ab) 0not|a with I
 ... | b=0 = 0R , transitive timesZero (symmetric b=0)
 PrimeIdeal.notContained (intDomImpliesZeroIdealPrime intDom) = 1R
 PrimeIdeal.notContainedIsNotContained (intDomImpliesZeroIdealPrime intDom) (c , 0c=1) = IntegralDomain.nontrivial intDom (symmetric (transitive (symmetric (transitive *Commutative timesZero)) 0c=1))
+
+primeIdealWellDefined : {c : _} {pred2 : A → Set c} (ideal2 : Ideal R pred2) → ({x : A} → pred x → pred2 x) → ({x : A} → pred2 x → pred x) → PrimeIdeal i → PrimeIdeal ideal2
+PrimeIdeal.isPrime (primeIdealWellDefined ideal2 predToPred2 pred2ToPred record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) p2ab notP2a = predToPred2 (isPrime (pred2ToPred p2ab) λ p → notP2a (predToPred2 p))
+PrimeIdeal.notContained (primeIdealWellDefined ideal2 predToPred2 pred2ToPred record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) = notContained
+PrimeIdeal.notContainedIsNotContained (primeIdealWellDefined ideal2 predToPred2 pred2ToPred record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) pred2Not = notContainedIsNotContained (pred2ToPred pred2Not)
diff --git a/Rings/Ideals/Principal/Definition.agda b/Rings/Ideals/Principal/Definition.agda
index 6cccfda..2351f8c 100644
--- a/Rings/Ideals/Principal/Definition.agda
+++ b/Rings/Ideals/Principal/Definition.agda
@@ -1,17 +1,11 @@
 {-# OPTIONS --safe --warning=error --without-K #-}
 
 open import LogicalFormulae
-open import Groups.Groups
-open import Groups.Homomorphisms.Definition
-open import Groups.Definition
-open import Numbers.Naturals.Naturals
 open import Setoids.Orders
 open import Setoids.Setoids
 open import Functions
 open import Sets.EquivalenceRelations
 open import Rings.Definition
-open import Rings.Homomorphisms.Definition
-open import Groups.Homomorphisms.Lemmas
 
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
diff --git a/Rings/Ideals/Principal/Lemmas.agda b/Rings/Ideals/Principal/Lemmas.agda
new file mode 100644
index 0000000..08ae9d5
--- /dev/null
+++ b/Rings/Ideals/Principal/Lemmas.agda
@@ -0,0 +1,23 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.Ideals.Principal.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
+
+open Setoid S
+open Ring R
+open Equivalence eq
+open import Rings.Ideals.Principal.Definition R
+open import Rings.Ideals.Definition R
+open import Rings.Ideals.Lemmas R
+open import Rings.Divisible.Definition R
+
+generatorZeroImpliesAllZero : {c : _} {pred : A → Set c} → {i : Ideal pred} → (princ : PrincipalIdeal i) → PrincipalIdeal.generator princ ∼ 0R → {x : A} → pred x → x ∼ 0R
+generatorZeroImpliesAllZero record { generator = gen ; genIsInIdeal = genIsInIdeal ; genGenerates = genGenerates } gen=0 {x} predX = generatorZeroImpliesMembersZero {x} (divisibleWellDefined gen=0 reflexive (genGenerates predX))
diff --git a/Rings/PrincipalIdealDomains/Lemmas.agda b/Rings/PrincipalIdealDomains/Lemmas.agda
index f8f6103..5bbafc8 100644
--- a/Rings/PrincipalIdealDomains/Lemmas.agda
+++ b/Rings/PrincipalIdealDomains/Lemmas.agda
@@ -20,15 +20,21 @@ open import Rings.Ideals.Lemmas R
 open import Rings.Units.Definition R
 open import Rings.Irreducibles.Lemmas intDom
 open import Rings.Units.Lemmas R
+open import Rings.Ideals.Prime.Definition {R = R}
+open import Rings.Ideals.Prime.Lemmas {R = R}
+open import Rings.Primes.Definition intDom
+open import Rings.Primes.Lemmas intDom
+open import Rings.Ideals.Principal.Lemmas R
+open import Rings.Ideals.Maximal.Lemmas {R = R}
 
 open Ring R
 open Setoid S
 open Equivalence eq
 
-irreducibleImpliesMaximalIdeal : (r : A) → Irreducible r → {d : _} → MaximalIdeal (generatedIdeal r) {d}
-MaximalIdeal.notContained (irreducibleImpliesMaximalIdeal r irred {d}) = 1R
-MaximalIdeal.notContainedIsNotContained (irreducibleImpliesMaximalIdeal r irred {d}) = Irreducible.nonunit irred
-MaximalIdeal.isMaximal (irreducibleImpliesMaximalIdeal r irred {d}) {biggerPred} bigger biggerContains (outsideR , (biggerContainsOutside ,, notInR)) {x} = biggerPrincipal' (unitImpliesGeneratedIdealEverything w {x})
+irreducibleImpliesMaximalIdeal : {r : A} → Irreducible r → {d : _} → MaximalIdeal (generatedIdeal r) {d}
+MaximalIdeal.notContained (irreducibleImpliesMaximalIdeal {r} irred {d}) = 1R
+MaximalIdeal.notContainedIsNotContained (irreducibleImpliesMaximalIdeal {r} irred {d}) = Irreducible.nonunit irred
+MaximalIdeal.isMaximal (irreducibleImpliesMaximalIdeal {r} irred {d}) {biggerPred} bigger biggerContains (outsideR , (biggerContainsOutside ,, notInR)) {x} = biggerPrincipal' (unitImpliesGeneratedIdealEverything w {x})
   where
     biggerGen : A
     biggerGen = PrincipalIdeal.generator (pid bigger)
@@ -51,3 +57,18 @@ MaximalIdeal.isMaximal (irreducibleImpliesMaximalIdeal r irred {d}) {biggerPred}
     v r|bg | assoc = notInR (associateImpliesGeneratedIdealsEqual' assoc (PrincipalIdeal.genGenerates (pid bigger) biggerContainsOutside))
     w : Unit biggerGen
     w = dividesIrreducibleImpliesUnit irred u v
+
+primeIdealIsMaximal : {c : _} {pred : A → Set c} → {i : Ideal pred} → (nonzero : Sg A (λ a → ((a ∼ 0R) → False) && pred a)) → PrimeIdeal i → {d : _} → MaximalIdeal i {d}
+primeIdealIsMaximal {pred = pred} {i} (m , (m!=0 ,, predM)) prime {d = d} = maximalIdealWellDefined (generatedIdeal (PrincipalIdeal.generator princ)) i (memberDividesImpliesMember i (PrincipalIdeal.genIsInIdeal princ)) (PrincipalIdeal.genGenerates princ) isMaximal
+  where
+    princ : PrincipalIdeal i
+    princ = pid i
+    isPrime : Prime (PrincipalIdeal.generator princ)
+    isPrime = primeIdealImpliesPrime (λ gen=0 → PrimeIdeal.notContainedIsNotContained prime (exFalso (m!=0 (generatorZeroImpliesAllZero princ gen=0 predM)))) (primeIdealWellDefined i (generatedIdeal (PrincipalIdeal.generator princ)) (PrincipalIdeal.genGenerates princ) (memberDividesImpliesMember i (PrincipalIdeal.genIsInIdeal princ)) prime)
+    isIrreducible : Irreducible (PrincipalIdeal.generator princ)
+    isIrreducible = primeIsIrreducible isPrime
+    isMaximal : MaximalIdeal (generatedIdeal (PrincipalIdeal.generator princ)) {d}
+    isMaximal = irreducibleImpliesMaximalIdeal isIrreducible {d}
+
+irreducibleImpliesPrime : {x : A} → Irreducible x → Prime x
+irreducibleImpliesPrime {x} irred = primeIdealImpliesPrime (Irreducible.nonzero irred) (idealMaximalImpliesIdealPrime (generatedIdeal x) (irreducibleImpliesMaximalIdeal irred))
diff --git a/Rings/UniqueFactorisationDomains/Definition.agda b/Rings/UniqueFactorisationDomains/Definition.agda
new file mode 100644
index 0000000..8a370c2
--- /dev/null
+++ b/Rings/UniqueFactorisationDomains/Definition.agda
@@ -0,0 +1,27 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Setoids.Setoids
+open import Rings.Definition
+open import Rings.IntegralDomains.Definition
+open import Lists.Lists
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.UniqueFactorisationDomains.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where
+
+open import Rings.Units.Definition R
+open import Rings.Irreducibles.Definition intDom
+open Ring R
+open Setoid S
+
+record Factorisation {r : A} (nonzero : (r ∼ 0R) → False) (nonunit : (Unit r) → False) : Set (a ⊔ b) where
+  field
+    factorise : List A
+    factoriseIsFactorisation : fold (_*_) 1R factorise ∼ r
+    factoriseIsIrreducibles : allTrue Irreducible factorise
+
+record UFD : Set (a ⊔ b) where
+  field
+    factorisation : {r : A} → (nonzero : (r ∼ 0R) → False) → (nonunit : (Unit r) → False) → Factorisation nonzero nonunit
+    uniqueFactorisation : {r : A} → (nonzero : (r ∼ 0R) → False) → (nonunit : (Unit r) → False) → (f1 f2 : Factorisation nonzero nonunit) → {!Sg !}