Wordsmith the exposition in the W-types development

proofs/type_theory/homotopy_type_theory.v

@@ -16,6 +16,36 @@ Require Import Coq.Program.Basics.
 
 Definition U := Type.
 
+Definition Singleton X := { c : X & forall x, c = x }.
+
+Definition Fiber [X Y] (f : X -> Y) y := { x & f x = y }.
+
+Definition Equivalence [X Y] (f : X -> Y) := forall y, Singleton (Fiber f y).
+
+Definition Equivalent X Y := { f : X -> Y & Equivalence f }.
+
+Definition SingletonType [X] (x : X) := { y & y = x }.
+
+Definition singleton [X] (x : X) : SingletonType x := existT _ x eq_refl.
+
+Definition singletonIsSingleton [X] (x : X) : Singleton (SingletonType x) :=
+  existT _ (existT _ x eq_refl) _.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 (* Transport *)
 
 Definition transport [A] [x y : A] [P : A -> Type] (p : x = y) (px : P x) :=

proofs/type_theory/w_types.v

@@ -10,11 +10,11 @@ Require Import Coq.Logic.FunctionalExtensionality.
 
 (*
   W-types are the types of well-founded trees and generalize inductive types
-  like `bool`, `nat`, `list`, etc. The parameter `A` encodes both the choice of
+  like `bool`, `nat`, `list`, etc. The type `A` encodes both the choice of
   constructor and its non-recursive arguments. The family `B` encodes the
-  number of recursive arguments for a given choice of `A`. The name `sup` is
-  short for "supremum", since each node in the tree is the least upper bound of
-  its subtrees in the "subtree of" relation.
+  number of recursive arguments for each value of `A`. The name `sup` is short
+  for "supremum", since each node in the tree is the least upper bound of its
+  subtrees in the "subtree of" relation.
 *)
 
 Inductive W [A] (B : A -> Type) :=
@@ -84,7 +84,7 @@ Definition pre_eliminator
       with
       | true => fun f _ =>
         match
-          functional_extensionality
+          functional_extensionality (* Here *)
             (fun x : Empty_set => match x with end)
             f
             (fun x => match x with end)
@@ -95,7 +95,7 @@ Definition pre_eliminator
         end
       | false => fun f h =>
         match
-          functional_extensionality
+          functional_extensionality (* And here *)
             (fun _ => f tt)
             f
             (
@@ -148,10 +148,9 @@ Qed.
      would go through if we had η-conversion for the unit type (along with
      η-conversion on Π types, which we already have in Coq).
 
-  This encoding of natural numbers suffers from the general issue that the `f`
-  argument of the `sup` constructor isn't sufficiently constrained. For
-  example, here's another definition of zero that is extensionally but not
-  judgmentally equal to `zero`:
+  The issue is that the `f` argument of the `sup` constructor isn't
+  sufficiently constrained. For example, here's another definition of zero that
+  is extensionally but not judgmentally equal to `zero`:
 *)
 
 Definition other_zero : PreNat := sup true (fun _ : Empty_set => pre_zero).
@@ -178,10 +177,15 @@ Qed.
     Leibniz-Zentrum für Informatik (2021)
     https://doi.org/10.4230/LIPIcs.TYPES.2020.8
 
-  The Σ type in Coq's standard library doesn't have definitional
-  η-conversion:
+  Coq has η-conversion for Π types but not for the Σ type defined in the
+  standard library:
 *)
 
+Goal forall T (P : T -> Type) (f : forall x : T, P x), f = fun x => f x.
+Proof.
+  reflexivity.
+Qed.
+
 Goal
   forall T (P : T -> Type) (s : { x : T & P x }),
   s = existT _ (projT1 s) (projT2 s).
@@ -193,7 +197,7 @@ Proof.
 Qed.
 
 (*
-  However, we can define a Σ with η-conversion as a primitive record type:
+  Fortunately, we can define a Σ with η-conversion as a primitive record type:
 *)
 
 Record Sigma [T] (P : T -> Type) := sigma { x : T; y : P x }.