diff --git a/theories/Basics.v b/theories/Basics.v
index 86897b44078..09f1c866556 100644
--- a/theories/Basics.v
+++ b/theories/Basics.v
@@ -8,6 +8,7 @@ Require Export Basics.Utf8.
 Require Export Basics.Notations.
 Require Export Basics.Tactics.
 Require Export Basics.Classes.
+Require Export Basics.Iff.
 
 Require Export Basics.Nat.
 Require Export Basics.Numeral.
diff --git a/theories/Basics/Decidable.v b/theories/Basics/Decidable.v
index 7ad5460235d..2f7614351f3 100644
--- a/theories/Basics/Decidable.v
+++ b/theories/Basics/Decidable.v
@@ -3,7 +3,8 @@ Require Import
   Basics.Overture
   Basics.PathGroupoids
   Basics.Trunc
-  Basics.Tactics.
+  Basics.Tactics
+  Basics.Iff.
 Local Open Scope trunc_scope.
 Local Open Scope path_scope.
 
@@ -85,6 +86,13 @@ Proof.
   exact (nnnp (fun np => np p)).
 Defined.
 
+Definition iff_stable P `(Stable P) : ~~P <-> P.
+Proof.
+  split.
+  - apply stable.
+  - exact (fun x f => f x).
+Defined.
+
 (**
   Because [vm_compute] evaluates terms in [PROP] eagerly
   and does not remove dead code we
@@ -122,21 +130,21 @@ Global Instance decidable_empty : Decidable Empty
 
 (** ** Transfer along equivalences *)
 
-Definition decidable_iff {A B} (f : A -> B) (f' : B -> A)
+Definition decidable_iff {A B} (f : A <-> B)
   : Decidable A -> Decidable B.
 Proof.
   intros [a|na].
-  - exact (inl (f a)).
-  - exact (inr (fun b => na (f' b))).
+  - exact (inl (fst f a)).
+  - exact (inr (fun b => na (snd f b))).
 Defined.
 
-Definition decidable_equiv (A : Type) {B : Type} (f : A -> B) `{IsEquiv A B f}
-  : Decidable A -> Decidable B
-  := decidable_iff f f^-1.
-
 Definition decidable_equiv' (A : Type) {B : Type} (f : A <~> B)
 : Decidable A -> Decidable B
-  := decidable_equiv A f.
+  := decidable_iff f.
+
+Definition decidable_equiv (A : Type) {B : Type} (f : A -> B) `{!IsEquiv f}
+: Decidable A -> Decidable B
+  := decidable_equiv' _ (Build_Equiv _ _ f _).
 
 Definition decidablepaths_equiv
            (A : Type) {B : Type} (f : A -> B) `{IsEquiv A B f}
@@ -261,3 +269,37 @@ Proof.
   - elim (nd d').
   - apply ap, path_forall; intros p; elim (nd p).
 Defined.
+
+(** ** Logical Laws *)
+
+(** Various logical laws don't hold constructively as they do classically due to a required use of excluded middle. For us, this means that some laws require further assumptions on the decidability of propositions. *)
+
+(** Here we give the dual De Morgan's Law which complements the one given in Iff.v.  One direction requires that one of the two propositions be decidable, while the other direction needs no assumption.  We state the latter property first, to avoid duplication in the proof. *)
+Definition not_prod_sum_not A B : ~ A + ~ B -> ~ (A * B).
+Proof.
+  intros [na|nb] [a b].
+  - exact (na a).
+  - exact (nb b).
+Defined.
+
+Definition iff_not_prod A B `{Decidable A}
+  : ~ (A * B) <-> ~ A + ~ B.
+Proof.
+  split.
+  - intros np.
+    destruct (dec A) as [a|na].
+    + exact (inr (fun b => np (a, b))).
+    + exact (inl na).
+  - apply not_prod_sum_not.
+Defined.
+
+Definition iff_not_prod' A B `{Decidable B}
+  : ~ (A * B) <-> ~ A + ~ B.
+Proof.
+  split.
+  - intros np.
+    destruct (dec B) as [b|nb].
+    + exact (inl (fun a => np (a, b))).
+    + exact (inr nb).
+  - apply not_prod_sum_not.
+Defined.
diff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v
index 523e94a7991..9384495d478 100644
--- a/theories/Basics/Equivalences.v
+++ b/theories/Basics/Equivalences.v
@@ -80,9 +80,6 @@ Ltac change_apply_equiv_compose :=
     change ((f oE g) x) with (f (g x))
   end.
 
-Definition iff_equiv {A B : Type} (f : A <~> B)
-  : A <-> B := (equiv_fun f, f^-1).
-
 (** Transporting is an equivalence. *)
 Section EquivTransport.
 
diff --git a/theories/Basics/Iff.v b/theories/Basics/Iff.v
new file mode 100644
index 00000000000..bcc53a624c1
--- /dev/null
+++ b/theories/Basics/Iff.v
@@ -0,0 +1,60 @@
+Require Import Basics.Overture Basics.Tactics.
+
+Local Set Universe Minimization ToSet.
+
+(** * If and only if *)
+
+(** ** Definition *)
+
+(** [iff A B], written [A <-> B], expresses the logical equivalence of [A] and [B] *)
+Definition iff (A B : Type) := prod (A -> B) (B -> A).
+
+Notation "A <-> B" := (iff A B) : type_scope.
+
+(** ** Basic Properties *)
+
+(** Everything is logically equivlaent to itself. *)
+Definition iff_refl {A} : A <-> A
+  := (idmap , idmap).
+
+(** [iff] is a reflexive relation. *)
+Global Instance iff_reflexive : Reflexive iff | 1
+  := @iff_refl.
+
+(** Logical equivalences can be inverted. *)
+Definition iff_inverse {A B} : (A <-> B) -> (B <-> A)
+  :=  fun f => (snd f , fst f).
+
+(** [iff] is a symmetric relation. *)
+Global Instance symmetric_iff : Symmetric iff | 1
+  := @iff_inverse.
+
+(** Logical equivalences can be composed. *)
+Definition iff_compose {A B C} (f : A <-> B) (g : B <-> C) : A <-> C
+  := (fst g o fst f , snd f o snd g).
+
+(** [iff] is a transitive relation. *)
+Global Instance transitive_iff : Transitive iff | 1
+  := @iff_compose.
+
+(** Any equivalence can be considered a logical equivalence by discarding everything but the maps. We make this a coercion so that equivalences can be used in place of logical equivalences. *)
+Coercion iff_equiv {A B : Type} (f : A <~> B)
+  : A <-> B := (equiv_fun f, f^-1).
+
+(** ** Logical Laws *)
+
+(** One of De Morgan's Laws.  The dual statement about negating a product appears in Decidable.v due to decidability requirements. *)
+Definition iff_not_sum A B : ~ (A + B) <-> ~ A * ~ B.
+Proof.
+  split.
+  - intros ns.
+    exact (ns o inl, ns o inr).
+  - by intros []; snrapply sum_ind.
+Defined.
+
+Definition iff_contradiction A : A * ~A <-> Empty.
+Proof.
+  split.
+  - intros [a na]; exact (na a).
+  - intros e; exact (Empty_rec _ e).
+Defined.
diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v
index c0f3b0150d7..779cda59d5e 100644
--- a/theories/Basics/Overture.v
+++ b/theories/Basics/Overture.v
@@ -73,13 +73,6 @@ Notation conj := pair (only parsing).
 
 #[export] Hint Resolve pair inl inr : core.
 
-(** If and only if *)
-
-(** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
-Definition iff (A B : Type) := prod (A -> B) (B -> A).
-
-Notation "A <-> B" := (iff A B) : type_scope.
-
 (** ** Type classes *)
 
 (** This command prevents Coq from trying to guess the values of existential variables while doing typeclass resolution.  If you don't know what that means, ignore it. *)
@@ -224,20 +217,6 @@ Notation "g 'o' f" := (compose g%function f%function) : function_scope.
 (** This definition helps guide typeclass inference. *)
 Definition Compose {A B C : Type} (g : B -> C) (f : A -> B) : A -> C := compose g f.
 
-(** Composition of logical equivalences *)
-Global Instance iff_compose : Transitive iff | 1
-  := fun A B C f g => (fst g o fst f , snd f o snd g).
-Arguments iff_compose {A B C} f g : rename.
-
-(** While we're at it, inverses of logical equivalences *)
-Global Instance iff_inverse : Symmetric iff | 1
-  := fun A B f => (snd f , fst f).
-Arguments iff_inverse {A B} f : rename.
-
-(** And reflexivity of them *)
-Global Instance iff_reflexive : Reflexive iff | 1
-  := fun A => (idmap , idmap).
-
 (** Dependent composition of functions. *)
 Definition composeD {A B C} (g : forall b, C b) (f : A -> B) := fun x : A => g (f x).
 
diff --git a/theories/Basics/Trunc.v b/theories/Basics/Trunc.v
index 48f1758184c..508f323391b 100644
--- a/theories/Basics/Trunc.v
+++ b/theories/Basics/Trunc.v
@@ -7,7 +7,8 @@ Require Import
   Basics.Contractible
   Basics.Equivalences
   Basics.Tactics
-  Basics.Nat.
+  Basics.Nat
+  Basics.Iff.
 
 Local Set Universe Minimization ToSet.
 
diff --git a/theories/Categories/Structure/IdentityPrinciple.v b/theories/Categories/Structure/IdentityPrinciple.v
index 5da2d87b743..dd3e7900c10 100644
--- a/theories/Categories/Structure/IdentityPrinciple.v
+++ b/theories/Categories/Structure/IdentityPrinciple.v
@@ -2,7 +2,7 @@
 Require Import Category.Core Category.Univalent Category.Morphisms.
 Require Import Structure.Core.
 Require Import Types.Sigma Trunc Equivalences.
-Require Import Basics.Tactics.
+Require Import Basics.Iff Basics.Tactics.
 
 Set Universe Polymorphism.
 Set Implicit Arguments.
diff --git a/theories/PropResizing/Nat.v b/theories/PropResizing/Nat.v
index 06e53f469ca..6b71aa35cfc 100644
--- a/theories/PropResizing/Nat.v
+++ b/theories/PropResizing/Nat.v
@@ -149,8 +149,7 @@ Section AssumeStuff.
     Qed.
 
     Definition graph_unsucc_equiv_vert@{} : vert A <~> vert B
-      := equiv_unfunctor_sum_l@{s s s s s  s Set Set Set Set}
-                              f Ha Hb.
+      := equiv_unfunctor_sum_l@{s s s s s s} f Ha Hb.
 
     Definition graph_unsucc_equiv_edge@{} (x y : vert A)
       : iff@{s s s} (edge A x y) (edge B (graph_unsucc_equiv_vert x) (graph_unsucc_equiv_vert y)).
diff --git a/theories/Spaces/Finite/Fin.v b/theories/Spaces/Finite/Fin.v
index 75a44e16757..afff1f75d04 100644
--- a/theories/Spaces/Finite/Fin.v
+++ b/theories/Spaces/Finite/Fin.v
@@ -267,7 +267,7 @@ Proof.
   assert (p' := (moveL_equiv_V _ _ p)^).
   exists y.
   destruct y as [y|[]].
-  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set Set Set Set Set}
+  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set}
               (fin_transpose_last_with m (inl y) oE e)
               _ _ ; _).
     { intros a. ev_equiv.
@@ -286,7 +286,7 @@ Proof.
     * rewrite unfunctor_sum_l_beta.
       apply fin_transpose_last_with_invol.
     * refine (fin_transpose_last_with_last _ _ @ p^).
-  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set Set Set Set Set} e _ _ ; _).
+  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set} e _ _ ; _).
     { intros a.
       destruct (is_inl_or_is_inr (e (inl a))) as [l|r].
       - exact l.
diff --git a/theories/Spaces/Int.v b/theories/Spaces/Int.v
index ae7f0130a86..5924f0b1699 100644
--- a/theories/Spaces/Int.v
+++ b/theories/Spaces/Int.v
@@ -124,8 +124,9 @@ Proof.
   2-4,6-8: right; intros; discriminate.
   2: by left.
   1,2: nrapply decidable_iff.
-  1,4: nrapply ap.
-  1,3: intros H; by injection H.
+  1,3: split.
+  1,3: nrapply ap.
+  1,2: intros H; by injection H.
   1,2: exact _.
 Defined.
 
diff --git a/theories/Spaces/List/Core.v b/theories/Spaces/List/Core.v
index 2058eadee51..d8fec4c5761 100644
--- a/theories/Spaces/List/Core.v
+++ b/theories/Spaces/List/Core.v
@@ -193,3 +193,12 @@ Fixpoint for_all@{i j|} {A : Type@{i}} (P : A -> Type@{j}) l : Type@{j} :=
   | nil => Unit
   | x :: l => P x /\ for_all P l
   end.
+
+(** ** Exists *)
+
+(** Apply a predicate to all elements of a list and take their disjunction. *)
+Fixpoint list_exists@{i j|} {A : Type@{i}} (P : A -> Type@{j}) l : Type@{j} :=
+  match l with
+  | nil => Empty
+  | x :: l => P x + list_exists P l
+  end.
diff --git a/theories/Spaces/List/Theory.v b/theories/Spaces/List/Theory.v
index 03331854595..b20ccc15f61 100644
--- a/theories/Spaces/List/Theory.v
+++ b/theories/Spaces/List/Theory.v
@@ -1,5 +1,5 @@
 Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc
-  Basics.Equivalences Basics.Decidable.
+  Basics.Equivalences Basics.Decidable Basics.Iff.
 Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum
   Types.Empty Types.Option.
 Require Export Spaces.List.Core Spaces.Nat.Core.
@@ -719,7 +719,7 @@ Defined.
 (** *** Filter *)
 
 (** Produce the list of elements of a list that satisfy a decidable predicate. *)
-Fixpoint list_filter {A : Type} (l : list A) (P : A -> Type)
+Fixpoint list_filter@{u v|} {A : Type@{u}} (l : list A) (P : A -> Type@{v})
   (dec : forall x, Decidable (P x))
   : list A
   := match l with
@@ -729,33 +729,37 @@ Fixpoint list_filter {A : Type} (l : list A) (P : A -> Type)
         else list_filter l P dec
     end.
 
-Definition inlist_filter {A : Type} (l : list A) (P : A -> Type)
-  (dec : forall x, Decidable (P x)) (x : A)
-  : InList x (list_filter l P dec) <-> InList x l /\ P x.
+Definition inlist_filter@{u v k | u <= k, v <= k} {A : Type@{u}} (l : list A)
+  (P : A -> Type@{v}) (dec : forall x, Decidable (P x)) (x : A)
+  : iff@{u k k} (InList x (list_filter l P dec)) (InList x l /\ P x).
 Proof.
   simple_list_induction l a l IHl.
   - simpl.
-    symmetry.
+    apply iff_inverse.
     apply iff_equiv.
-    snrapply prod_empty_l.
+    snrapply prod_empty_l@{v}.
   - simpl.
-    etransitivity.
-    2: { apply iff_equiv.
-         exact ((sum_distrib_r _ _ _)^-1%equiv). }
+    nrapply iff_compose.
+    2: { apply iff_inverse.
+         apply iff_equiv.
+         exact (sum_distrib_r@{k k k _ _ _ k k} _ _ _). }
     destruct (dec a) as [p|p].
     + simpl.
-      transitivity ((a = x) + InList x l * P x).
+      snrapply iff_compose.
+      1: exact (sum (a = x) (prod (InList@{u} x l) (P x))).
       1: split; apply functor_sum; only 1,3: exact idmap; apply IHl.
-      split; apply functor_sum; only 2,4: apply idmap.
-      * intros []; by split.
+      split; apply functor_sum@{k k k k}; only 2,4: apply idmap.
+      * intros [].
+        exact (idpath, p).
       * exact fst.
-    + etransitivity.
+    + nrapply iff_compose.
       1: apply IHl.
+      apply iff_inverse.
       apply iff_equiv.
-      nrefine (_ oE (sum_empty_l _)^-1%equiv).
-      snrapply equiv_functor_sum'.
-      2: reflexivity.
-      symmetry; apply equiv_to_empty.
+      nrefine (equiv_compose'@{k k k} (sum_empty_l@{k} _) _).
+      snrapply equiv_functor_sum'@{k k k k k k}.
+      2: exact equiv_idmap.
+      apply equiv_to_empty.
       by intros [[] r].
 Defined.
 
@@ -920,7 +924,7 @@ Proof.
   nrefine (_ oE (equiv_inlist_app _ _ _)^-1).
   nrefine (_ oE equiv_functor_sum' (B':=x = n) IHn _).
   2: { simpl.
-       exact (equiv_path_inverse _ _ oE sum_empty_r@{Set Set Set} _). }
+       exact (equiv_path_inverse _ _ oE sum_empty_r@{Set} _). }
   nrefine (_ oE equiv_leq_lt_or_eq^-1).
   rapply equiv_iff_hprop.
 Defined.
@@ -993,7 +997,7 @@ Proof.
   by apply for_all_list_map.
 Defined.
 
-(** If a predicate [P] and a prediate [Q] together imply a predicate [R], then [for_all P l] and [for_all Q l] together imply [for_all R l]. There are also some side conditions for the default elements. *)
+(** If a predicate [P] and a predicate [Q] together imply a predicate [R], then [for_all P l] and [for_all Q l] together imply [for_all R l]. There are also some side conditions for the default elements. *)
 Lemma for_all_list_map2 {A B C : Type}
   (P : A -> Type) (Q : B -> Type) (R : C -> Type)
   (f : A -> B -> C) (Hf : forall x y, P x -> Q y -> R (f x y))
@@ -1111,11 +1115,67 @@ Global Instance decidable_for_all {A : Type} (P : A -> Type)
   `{forall x, Decidable (P x)} (l : list A)
   : Decidable (for_all P l).
 Proof.
-  induction l as [|x l IHl].
-  - exact (inl tt).
-  - destruct IHl as [Hl | Hl].
-    + destruct (dec (P x)) as [Hx | Hx].
-      * exact (inl (Hx, Hl)).
-      * exact (inr (fun H => Hx (fst H))).
-    + exact (inr (fun H => Hl (snd H))).
+  simple_list_induction l x l IHl; exact _.
+Defined.
+
+(** If a predicate [P] is decidable then so is [list_exists P]. *)
+Global Instance decidable_list_exists {A : Type} (P : A -> Type)
+  `{forall x, Decidable (P x)} (l : list A)
+  : Decidable (list_exists P l).
+Proof.
+  simple_list_induction l x l IHl; exact _.
+Defined.
+
+Definition inlist_list_exists {A : Type} (P : A -> Type) (l : list A)
+  : list_exists P l -> exists (x : A), InList x l /\ P x.
+Proof.
+  simple_list_induction l x l IHl.
+  1: done.
+  simpl.
+  intros [Px | ex].
+  - exists x.
+    by split; [left|].
+  - destruct (IHl ex) as [x' [H Px']].
+    exists x'.
+    by split; [right|].
+Defined.
+
+Definition list_exists_inlist {A : Type} (P : A -> Type) (l : list A)
+  : forall (x : A), InList x l -> P x -> list_exists P l.
+Proof.
+  simple_list_induction l x l IHl.
+  1: trivial.
+  simpl; intros y H p; revert H.
+  apply functor_sum.
+  - exact (fun r => r^ # p).
+  - intros H.
+    by apply (IHl y).
+Defined.
+
+Definition list_exists_seq {n : nat} (P : nat -> Type)
+  (H : forall k, P k -> (k < n)%nat)
+  : (exists k, P k) <-> list_exists P (seq n).
+Proof.
+  split.
+  - intros [k p].
+    snrapply (list_exists_inlist P _ k _ p).
+    apply inlist_seq, H.
+    exact p.
+  - intros H1.
+    apply inlist_list_exists in H1.
+    destruct H1 as [k [Hk p]].
+    exists k.
+    exact p.
+Defined.
+
+(** An upper bound on witnesses of a decidable predicate makes the sigma type decidable. *)
+Definition decidable_exists_nat (n : nat) (P : nat -> Type)
+  (H1 : forall k, P k -> (k < n)%nat)
+  (H2 : forall k, Decidable (P k))
+  : Decidable (exists k, P k).
+Proof.
+  nrapply decidable_iff.
+  1: apply iff_inverse; nrapply list_exists_seq.
+  1: exact H1.
+  exact _.
 Defined.
diff --git a/theories/Spaces/Nat/Core.v b/theories/Spaces/Nat/Core.v
index e2cb9dffb45..8a209d3107a 100644
--- a/theories/Spaces/Nat/Core.v
+++ b/theories/Spaces/Nat/Core.v
@@ -1,6 +1,6 @@
 Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids
   Basics.Decidable Basics.Trunc Basics.Equivalences Basics.Nat
-  Basics.Classes Types.Prod Types.Sum Types.Sigma.
+  Basics.Classes Basics.Iff Types.Prod Types.Sum Types.Sigma.
 Export Basics.Nat.
 
 Local Set Universe Minimization ToSet.
@@ -487,6 +487,14 @@ Global Instance antisymmetric_leq : AntiSymmetric leq := @leq_antisym.
 Global Instance antisymemtric_geq : AntiSymmetric geq
   := fun _ _ p q => leq_antisym q p.
 
+(** Every natural number is zero or greater than zero. *)
+Definition nat_zero_or_gt_zero n : (0 = n) + (0 < n).
+Proof.
+  induction n as [|n IHn].
+  1: left; reflexivity.
+  right; exact _.
+Defined.
+
 (** Being less than or equal to [0] implies being [0]. *)
 Definition path_zero_leq_zero_r n : n <= 0 -> n = 0.
 Proof.
@@ -590,6 +598,7 @@ Hint Immediate leq_lt : typeclass_instances.
 
 Definition lt_trans {n m k} : n < m -> m < k -> n < k
   := fun H1 H2 => leq_lt (lt_leq_lt_trans H1 H2).
+Hint Immediate lt_trans : typeclass_instances.
 
 Global Instance transitive_lt : Transitive lt := @lt_trans.
 Global Instance ishprop_lt n m : IsHProp (n < m) := _.
diff --git a/theories/Spaces/Nat/Division.v b/theories/Spaces/Nat/Division.v
index ba22c782447..ad4905372fd 100644
--- a/theories/Spaces/Nat/Division.v
+++ b/theories/Spaces/Nat/Division.v
@@ -1,6 +1,6 @@
 Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes
   Basics.PathGroupoids Basics.Equivalences Types.Sigma Spaces.Nat.Core
-  Basics.Decidable Types.Prod List.Theory Types.Sum.
+  Basics.Decidable Basics.Iff Types.Prod List.Theory Types.Sum Types.Arrow.
 
 Local Set Universe Minimization ToSet.
 Local Open Scope nat_scope.
@@ -93,6 +93,20 @@ Proof.
   nrapply nat_dist_sub_r.
 Defined.
 
+(** The divisor is greater than zero when the divident is greater than zero. *)
+Definition gt_zero_divides n m (d : (n | m)) (gt0 : 0 < m)
+  : 0 < n.
+Proof.
+  destruct d as [d H].
+  destruct H.
+  destruct (nat_zero_or_gt_zero n) as [z | s].
+  2: exact s.
+  (* The remaining case is impossible. *)
+  destruct z; cbn in gt0.
+  rewrite nat_mul_zero_r in gt0.
+  exact gt0.
+Defined.
+
 (** Divisibility implies that the divisor is less than or equal to the dividend. *)
 Definition leq_divides n m : 0 < m -> (n | m) -> n <= m.
 Proof.
@@ -102,6 +116,17 @@ Proof.
   rapply (leq_mul_l _ _ 0).
 Defined.
 
+(** The divisor is strictly less than the dividend when the other factor is greater than one. *)
+Definition lt_divides n m (d : (n | m)) (gt0 : 0 < m) (gt1 : 1 < d.1)
+  : n < m.
+Proof.
+  rewrite <- d.2.
+  snrapply (lt_leq_lt_trans (m:=1*n)).
+  1: rapply (leq_mul_l _ _ 0).
+  srapply (nat_mul_r_strictly_monotone (l:=0)).
+  rapply (gt_zero_divides n m).
+Defined.
+
 (** Divisibility is antisymmetric *)
 Definition nat_divides_antisym n m : (n | m) -> (m | n) -> n = m.
 Proof.
@@ -114,6 +139,14 @@ Defined.
 Global Instance antisymmetric_divides : AntiSymmetric NatDivides
   := nat_divides_antisym.
 
+(** If [n] divides [m], then the other factor also divides [m]. *)
+Global Instance divides_divisor n m (H : (n | m)) : (H.1 | m).
+Proof.
+  exists n.
+  lhs nrapply nat_mul_comm.
+  exact H.2.
+Defined.
+
 (** ** Properties of division *)
 
 Local Definition nat_div_mod_unique_helper b q1 q2 r1 r2
@@ -335,7 +368,7 @@ Defined.
 Global Instance decidable_nat_divides n m : Decidable (n | m).
 Proof.
   nrapply decidable_iff.
-  1, 2: apply nat_mod_iff_divides.
+  1: apply nat_mod_iff_divides.
   exact _.
 Defined.
 
@@ -640,6 +673,22 @@ Class IsPrime (n : nat) : Type0 := {
 
 Definition issig_IsPrime n : _ <~> IsPrime n := ltac:(issig).
 
+Global Instance ishprop_isprime `{Funext} n : IsHProp (IsPrime n).
+Proof.
+  nrapply istrunc_equiv_istrunc.
+  1: apply issig_IsPrime.
+  rapply istrunc_sigma.
+  intros H1.
+  snrapply istrunc_forall.
+  intros m.
+  snrapply istrunc_forall.
+  intros d.
+  rapply ishprop_sum.
+  intros p q.
+  nrapply (snd neq_iff_lt_or_gt _ (p^ @ q)).
+  by left.
+Defined.
+
 (** [0] is not a prime number. *)
 Definition not_isprime_zero : ~ IsPrime 0.
 Proof.
@@ -655,7 +704,7 @@ Proof.
 Defined.
 
 (** Being prime is a decidable property. We give an inefficient procedure for determining primality. More efficient procedures can be given, but for proofs this suffices. *)
-Global Instance decidable_isprime n : Decidable (IsPrime n).
+Global Instance decidable_isprime@{} n : Decidable (IsPrime n).
 Proof.
   (** First we begin by discarding the [n = 0] case as we can easily prove that [0] is not prime. *)
   destruct n.
@@ -669,10 +718,10 @@ Proof.
   snrapply decidable_prod.
   1: exact _.
   (** In order to show that this [forall] is decidable, we will exhibit it as a [for_all] statement over a given list. The predicate will be the conclusion we wish to reach here, and the list will consist of all numbers with a condition equivalent to the divisibility condition. *)
-  pose (P := fun m => ((m = 1) + (m = n.+1))%type).
+  pose (P := fun m => ((m = 1) + (m = n.+1))%type : Type0).
   pose (l := list_filter (seq n.+2) (fun x => (x | n.+1)) _).
-  snrapply decidable_iff.
-  - exact (for_all P l).
+  rapply (decidable_iff (A := for_all P l)).
+  split.
   - intros Pl x d.
     apply inlist_for_all with l x in Pl.
     1: exact Pl.
@@ -688,7 +737,6 @@ Proof.
     destruct H' as [p H'].
     apply inlist_seq in p.
     rapply H.
-  - exact _.
 Defined.
 
 (** We can show that the first 8 primes are prime as expected. *)
@@ -760,3 +808,140 @@ Proof.
   apply nat_moveR_nV.
   exact q.
 Defined.
+
+(** ** Composite Numbers *)
+
+(** A natural number larger than [1] is composite if it has a divisor other than [1] and itself. *)
+Class IsComposite n : Type0
+  := iscomposite : exists a, 1 < a < n /\ (a | n).
+
+Definition gt_1_iscomposite@{} n : IsComposite n -> 1 < n.
+Proof.
+  intros [a [[H1 H2] H3]].
+  exact _.
+Defined.
+Hint Immediate gt_1_iscomposite : typeclass_instances.
+
+(** Being composite is a decidable property. *)
+Global Instance decidable_iscomposite@{} n : Decidable (IsComposite n).
+Proof.
+  unfold IsComposite.
+  rapply (decidable_exists_nat n).
+  intros k c.
+  exact (snd (fst c)).
+Defined.
+
+(** For a number larger than [1], being prime is equivalent to not being composite. *)
+Definition isprime_iff_not_iscomposite@{} n
+  : IsPrime n <-> 1 < n /\ ~ IsComposite n.
+Proof.
+  split.
+  - intros H.
+    split; only 1: exact _.
+    intros [a [[H2 H3] H4]].
+    apply isprime in H4.
+    destruct H4 as [H4|H4]; destruct H4; exact (lt_irrefl _ _).
+  - intros [H1 H].
+    rapply Build_IsPrime.
+    intros m d.
+    destruct (dec (1 < d.1)) as [H2|H2].
+    + pose proof (divides_divisor _ _ d) as d'.
+      apply leq_divides in d'.
+      2: exact _.
+      apply equiv_leq_lt_or_eq in d'.
+      destruct d' as [d'|d'].
+      * assert (H' : IsComposite n).
+        { exists d.1.
+          split; only 1: split; exact _. }
+          contradiction H.
+      * destruct d as [d r].
+        simpl in *.
+        destruct d'.
+         left.
+         rewrite <- nat_div_cancel with d.
+         2: exact _.
+         rewrite <- nat_div_mul_cancel_l with d m.
+         2: exact _.
+         by apply (ap (fun x => x / d)).
+    + apply geq_iff_not_lt in H2.
+      destruct d as [d r].
+      simpl in *; hnf in H2.
+      destruct d.
+      { rewrite nat_mul_zero_l in r.
+        destruct n.
+        1: contradiction (not_lt_zero_r _ H1).
+        contradiction (neq_nat_zero_succ _ r). }
+      destruct d.
+      { rewrite nat_mul_one_l in r.
+        by right. }
+      apply leq_pred' in H2.
+      contradiction (not_lt_zero_r d).
+Defined.
+
+(** And since [IsComposite] is decidable, we can show that being not prime is equivalent to being composite. *)
+Definition not_isprime_iff_iscomposite@{} n
+  : 1 < n /\ ~ IsPrime n <-> IsComposite n.
+Proof.
+  nrapply iff_compose.
+  - nrapply iff_functor_prod.
+    1: nrapply iff_refl.
+    nrapply iff_compose.
+    + apply iff_not.
+      rapply isprime_iff_not_iscomposite.
+    + rapply iff_not_prod.
+  - nrapply iff_compose.
+    1: nrapply sum_distrib_l.
+    nrapply iff_compose.
+    + nrapply iff_functor_sum.
+      1: apply iff_contradiction.
+      nrapply iff_functor_prod.
+      1: nrapply iff_refl.
+      rapply iff_stable.
+    + nrapply iff_compose.
+      1: rapply sum_empty_l.
+      split; only 1: exact snd.
+      intros H; split; only 2: exact H.
+      exact _.
+Defined.
+
+(** ** Fundamental theorem of arithmetic *)
+
+(** Every natural number greater than [1] has a prime divisor. *)
+Definition exists_prime_divisor@{} n
+  : 1 < n -> exists (p : Prime), (p | n).
+Proof.
+  revert n; snrapply nat_ind_strong; hnf; intros n IHn H.
+  destruct (dec (IsPrime n)) as [x|x].
+  1: exists (_; x); exact _.
+  pose (r := (H, x)).
+  apply not_isprime_iff_iscomposite in r.
+  destruct r as [d [[H1 H2] H3]].
+  destruct (IHn d _ _) as [p r].
+  exists p.
+  exact _.
+Defined.
+
+(** Any natural number can either be written as a product of primes or is zero. *)
+Definition prime_factorization@{} n
+  : 0 < n
+    -> exists (l : list Prime),
+      n = fold_right (fun (p : Prime) n => nat_mul p n) 1 l.
+Proof.
+  revert n; snrapply nat_ind_strong; hnf; intros n IHn H.
+  destruct H as [|n IH].
+  1: exists nil; reflexivity.
+  destruct (exists_prime_divisor n.+1 _) as [p d].
+  pose proof (l := lt_divides d.1 n.+1 _ _ _).
+  destruct d as [k H].
+  destruct (IHn k l) as [f r].
+  { destruct H, k.
+    1: contradiction (lt_irrefl 0).
+    exact _. }
+  exists (p :: f)%list.
+  simpl; destruct r.
+  symmetry.
+  lhs nrapply nat_mul_comm.
+  exact H.
+Defined.
+
+(** TODO: show that any two prime factorizations are unique up to permutation of the lists. *)
diff --git a/theories/Types/Arrow.v b/theories/Types/Arrow.v
index f196622b453..9b56ad49b7b 100644
--- a/theories/Types/Arrow.v
+++ b/theories/Types/Arrow.v
@@ -2,10 +2,11 @@
 (** * Theorems about Non-dependent function types *)
 
 Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable
-               Basics.Equivalences Basics.Trunc Basics.Tactics.
+               Basics.Equivalences Basics.Trunc Basics.Tactics Basics.Iff.
 Require Import Types.Forall.
 Local Open Scope path_scope.
 
+Local Set Universe Minimization ToSet.
 
 Generalizable Variables A B C D f g n.
 
@@ -208,6 +209,13 @@ Definition not_contrapositive `(f : B -> A)
   : not A -> not B
   := functor_arrow f idmap.
 
+Definition iff_not@{u v k | u <= k, v <= k}
+  (A : Type@{u}) (B : Type@{v})
+  : A <-> B -> iff@{u v k} (~A) (~B).
+Proof.
+  intros e; split; apply not_contrapositive@{_ k}, e.
+Defined.
+
 Definition ap_functor_arrow `(f : B -> A) `(g : C -> D)
   (h h' : A -> C) (p : h == h')
   : ap (functor_arrow f g) (path_arrow _ _ p)
diff --git a/theories/Types/Forall.v b/theories/Types/Forall.v
index 1aff29ca05d..8b30a5247ac 100644
--- a/theories/Types/Forall.v
+++ b/theories/Types/Forall.v
@@ -2,7 +2,7 @@
 (** * Theorems about dependent products *)
 
 Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids
-               Basics.Tactics Basics.Contractible.
+               Basics.Tactics Basics.Contractible Basics.Iff.
 
 Require Export Basics.Trunc (istrunc_forall).
 
@@ -314,12 +314,9 @@ Defined.
 (** At least over a fixed base *)
 Definition iff_functor_forall {A : Type} {P Q : A -> Type}
            (f : forall a, P a <-> Q a)
-  : (forall a, P a) <-> (forall a, Q a).
-Proof.
-  split.
-  - intros g a; exact (fst (f a) (g a)).
-  - intros h a; exact (snd (f a) (h a)).
-Defined.
+  : (forall a, P a) <-> (forall a, Q a)
+  := (functor_forall idmap (fun a => fst (f a)),
+    functor_forall idmap (fun a => snd (f a))).
 
 (** ** Two variable versions for function extensionality. *)
 
diff --git a/theories/Types/Prod.v b/theories/Types/Prod.v
index 4ff20b28431..cb406ea19c1 100644
--- a/theories/Types/Prod.v
+++ b/theories/Types/Prod.v
@@ -2,10 +2,12 @@
 (** * Theorems about cartesian products *)
 
 Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids
-               Basics.Tactics Basics.Trunc Basics.Decidable.
+               Basics.Tactics Basics.Trunc Basics.Decidable Basics.Iff.
 Require Import Types.Empty.
 Local Open Scope path_scope.
 
+Local Set Universe Minimization ToSet.
+
 Generalizable Variables X A B f g n.
 
 Scheme prod_ind := Induction for prod Sort Type.
@@ -300,11 +302,11 @@ Defined.
 
 (** ** Unit and annihilation *)
 
-Definition prod_empty_r X : X * Empty <~> Empty
-  := (Build_Equiv _ _ snd _).
+Definition prod_empty_r@{u} (X : Type@{u}) : X * Empty <~> Empty
+  := (Build_Equiv@{u u} _ _ snd _).
 
-Definition prod_empty_l X : Empty * X <~> Empty
-  := (Build_Equiv _ _ fst _).
+Definition prod_empty_l@{u} (X : Type@{u}) : Empty * X <~> Empty
+  := (Build_Equiv@{u u} _ _ fst _).
 
 Definition prod_unit_r X : X * Unit <~> X.
 Proof.
@@ -391,13 +393,13 @@ Global Instance contr_prod `{CA : Contr A} `{CB : Contr B} : Contr (A * B) | 100
 
 Global Instance decidable_prod {A B : Type}
        `{Decidable A} `{Decidable B}
-: Decidable (A * B).
+: Decidable@{k} (A * B).
 Proof.
   destruct (dec A) as [x1|y1]; destruct (dec B) as [x2|y2].
-  - exact (inl (x1,x2)).
-  - apply inr; intros [_ x2]; exact (y2 x2).
-  - apply inr; intros [x1 _]; exact (y1 x1).
-  - apply inr; intros [x1 _]; exact (y1 x1).
+  - exact (inl@{k k} (x1,x2)).
+  - apply inr@{k k}; intros [_ x2]; exact (y2 x2).
+  - apply inr@{k k}; intros [x1 _]; exact (y1 x1).
+  - apply inr@{k k}; intros [x1 _]; exact (y1 x1).
 Defined.
 
 (** Interaction of ap and uncurry *)
diff --git a/theories/Types/Sum.v b/theories/Types/Sum.v
index 3d169930b3f..bcb67b10880 100644
--- a/theories/Types/Sum.v
+++ b/theories/Types/Sum.v
@@ -9,6 +9,8 @@ Require Import Types.Bool.
 Local Open Scope trunc_scope.
 Local Open Scope path_scope.
 
+Local Set Universe Minimization ToSet.
+
 Generalizable Variables X A B f g n.
 
 Scheme sum_ind := Induction for sum Sort Type.
@@ -603,6 +605,10 @@ Definition equiv_functor_sum_r {A A' B : Type} (f : A <~> A')
 : A + B <~> A' + B
   := f +E 1.
 
+Definition iff_functor_sum {A A' B B' : Type} (f : A <-> A') (g : B <-> B')
+  : A + B <-> A' + B'
+  := (functor_sum (fst f) (fst g), functor_sum (snd f) (snd g)).
+
 (** ** Unfunctoriality on equivalences *)
 
 Global Instance isequiv_unfunctor_sum_l {A A' B B' : Type}
@@ -682,7 +688,8 @@ Definition equiv_unfunctor_sum {A A' B B' : Type}
 
 (* This is a special property of [sum], of course, not an instance of a general family of facts about types. *)
 
-Definition equiv_sum_symm (A B : Type) : A + B <~> B + A.
+Definition equiv_sum_symm@{u v k | u <= k, v <= k} (A : Type@{u}) (B : Type@{v})
+  : Equiv@{k k} (A + B) (B + A).
 Proof.
   apply (equiv_adjointify
            (fun ab => match ab with inl a => inr a | inr b => inl b end)
@@ -705,44 +712,31 @@ Defined.
 
 (** ** Identity *)
 
-Definition sum_empty_l (A : Type) : Empty + A <~> A.
+Definition sum_empty_l@{u|} (A : Type@{u}) : Equiv@{u u} (Empty + A) A.
 Proof.
-  refine (equiv_adjointify
-       (fun z => match z:Empty+A with
-                   | inl e => match e with end
-                   | inr a => a
-                 end)
-       inr (fun a => 1) _).
-  intros [e|z]; [ elim e | reflexivity ].
+  snrapply equiv_adjointify@{u u}.
+  - intros [e|a]; [ exact (Empty_rec@{u} e) | exact a ].
+  - intros a; exact (inr@{Set u} a).
+  - intro x; exact idpath@{u}.
+  - intros [e|z]; [ elim e | exact idpath@{u}].
 Defined.
 
-Definition sum_empty_r (A : Type) : A + Empty <~> A.
-Proof.
-  refine (equiv_adjointify
-       (fun z => match z : A + Empty with
-                   | inr e => match e with end
-                   | inl a => a
-                 end)
-       inl (fun a => 1) _).
-  intros [z|e]; [ reflexivity | elim e ].
-Defined.
+Definition sum_empty_r@{u} (A : Type@{u}) : Equiv@{u u} (A + Empty) A
+  := equiv_compose'@{u u u} (sum_empty_l A) (equiv_sum_symm@{u Set u} _ _).
 
 (** ** Distributivity *)
 
 Definition sum_distrib_l A B C
 : A * (B + C) <~> (A * B) + (A * C).
 Proof.
-  refine (Build_Equiv (A * (B + C)) ((A * B) + (A * C))
-            (fun abc => let (a,bc) := abc in
-                        match bc with
-                          | inl b => inl (a,b)
-                          | inr c => inr (a,c)
-                        end) _).
-  simple refine (Build_IsEquiv (A * (B + C)) ((A * B) + (A * C)) _
-            (fun ax => match ax with
-                         | inl (a,b) => (a,inl b)
-                         | inr (a,c) => (a,inr c)
-                       end) _ _ _).
+  snrapply Build_Equiv.
+  2: snrapply Build_IsEquiv.
+  - intros [a [b|c]].
+    + exact (inl@{u u} (a, b)).
+    + exact (inr@{u u} (a, c)).
+  - intros [[a b]|[a c]].
+    + exact (a, inl@{u u} b).
+    + exact (a, inr@{u u} c).
   - intros [[a b]|[a c]]; reflexivity.
   - intros [a [b|c]]; reflexivity.
   - intros [a [b|c]]; reflexivity.
@@ -965,15 +959,15 @@ Defined.
 (** ** Decidability *)
 
 (** Sums preserve decidability *)
-Global Instance decidable_sum {A B : Type}
-       `{Decidable A} `{Decidable B}
-: Decidable (A + B).
+Global Instance decidable_sum@{u v k | u <= k, v <= k} {A : Type@{u}} {B : Type@{v}}
+  `{Decidable A} `{Decidable B}
+  : Decidable@{k} (A + B).
 Proof.
   destruct (dec A) as [x1|y1].
-  - exact (inl (inl x1)).
-  - destruct (dec B) as [x2|y2].
-    + exact (inl (inr x2)).
-    + apply inr; intros z.
+  - exact (inl@{k k} (inl x1)).
+  - destruct (dec@{v} B) as [x2|y2].
+    + exact (inl@{k k} (inr x2)).
+    + apply inr@{k k}; intros z.
       destruct z as [x1|x2].
       * exact (y1 x1).
       * exact (y2 x2).
diff --git a/theories/Utf8Minimal.v b/theories/Utf8Minimal.v
index 06dc33d1f7b..f2538163009 100644
--- a/theories/Utf8Minimal.v
+++ b/theories/Utf8Minimal.v
@@ -1,5 +1,4 @@
-Require Export HoTT.Basics.Utf8.
-Require Import HoTT.Basics.Overture.
+Require Export Basics.Utf8 Basics.Overture Basics.Iff.
 
 (** * Just enough Utf8/unicode for the Classes library to build, without depending on everything that HoTT.Utf8 depends on. *)
 
diff --git a/theories/WildCat/EquivGpd.v b/theories/WildCat/EquivGpd.v
index 11dbc347be6..a9bda05d356 100644
--- a/theories/WildCat/EquivGpd.v
+++ b/theories/WildCat/EquivGpd.v
@@ -1,6 +1,6 @@
 (* -*- mode: coq; mode: visual-line -*-  *)
 
-Require Import Basics.Overture Basics.Tactics.
+Require Import Basics.Overture Basics.Tactics Basics.Iff.
 Require Import WildCat.Core.
 Require Import WildCat.NatTrans.
 Require Import WildCat.Sigma.