Merge pull request #2103 from jdchristensen/impredicative-truncation

ImpredicativeTruncation: redo using universe annotations

theories/Metatheory/ImpredicativeTruncation.v

@@ -1,74 +1,124 @@
-(** * Impredicative truncations. *)
+(** * Impredicative truncations *)
+
+(** In this file, under the assumptions of propositional resizing [PropResizing] and function extensionality [Funext], we define the proposition truncation in any universe. In the main library, these are constructed using HITs. The definitions here are meant to be for illustration. *)
 
 Require Import HoTT.Basics.
 Require Import Universes.Smallness.
 Local Open Scope path_scope.
 
-(* Be careful about [Import]ing this file!  It defines truncations
-with the same name as those constructed with HITs.  Probably you want
-to use those instead, if you are using HITs. *)
+(** Using only function extensionality, we can define a "propositional truncation" [Trm A] of a type [A] in universe [i] which eliminates into propositions in universe [j].  It lands in [max(i,j+1)].  So if we want it to land in universe [i], then we can only eliminate into propositions in a strictly smaller universe [j].  Or, if we want it to eliminate into propositions in universe [i], then it must land in a strictly larger universe. *)
+Definition Trm@{i j | } (A : Type@{i})
+  := forall P:Type@{j}, IsHProp P -> (A -> P) -> P.
 
-Section AssumePropResizing.
-  Context `{PropResizing}.
+Definition trm@{i j | } {A : Type@{i}} : A -> Trm@{i j} A
+  := fun a P HP f => f a.
+
+(** Here [k] plays the role of [max(i,j+1)]. *)
+Global Instance ishprop_Trm@{i j k | i <= k, j < k} `{Funext} (A : Type@{i})
+  : IsHProp (Trm@{i j} A).
+Proof.
+  nrapply istrunc_forall@{k k k}; intro B.
+  nrapply istrunc_forall@{j k k}; intro ishp.
+  apply istrunc_forall@{k j k}.
+Defined.
 
-  Definition merely@{i j} (A : Type@{i}) : Type@{i}
-    := forall P:Type@{j}, IsHProp P -> (A -> P) -> P.   (* requires j < i *)
+(** As mentioned above, it eliminates into propositions in universe [j]. *)
+Definition Trm_rec@{i j | } {A : Type@{i}}
+  {P : Type@{j}} {p : IsHProp@{j} P} (f : A -> P)
+  : Trm@{i j} A -> P
+  := fun ma => ma P p f.
 
-  Definition trm {A} : A -> merely A
-    := fun a P HP f => f a.
+(** This computes definitionally. *)
+Definition Trm_rec_beta@{i j | } {A : Type@{i}}
+  {P : Type@{j}} `{IsHProp P} (f : A -> P)
+  : Trm_rec@{i j} f o trm == f
+  := fun _ => idpath.
+
+(** Because of the universe constraints, we can't make this into a functor on [Type@{i}].  We have a universe constraint [i' <= j] and [Trm@{i j} A] lands in [max(i,j+1)], which is strictly larger. *)
+Definition functor_Trm@{i j i' j' | i' <= j, j' < j} `{Funext}
+  {A : Type@{i}} {A' : Type@{i'}} (f : A -> A')
+  : Trm@{i j} A -> Trm@{i' j'} A'
+  := Trm_rec (trm o f).
+
+(** We also record the dependent induction principle.  But it only computes propositionally. *)
+Definition Trm_ind@{i j k | i <= k, j < k} {A : Type@{i}} `{Funext}
+  {P : Trm@{i j} A -> Type@{j}} {p : forall x, IsHProp@{j} (P x)} (f : forall a, P (trm a))
+  : forall x, P x.
+Proof.
+  unfold Trm.
+  intro x.
+  rapply x.
+  intro a.
+  refine (transport P _ (f a)).
+  rapply path_ishprop@{k}.
+Defined.
 
-  Global Instance ishprop_merely `{Funext} (A : Type) : IsHProp (merely A).
-  Proof.
-    exact _.
-  Defined.
+(** The universe constraints go away if we assume propositional resizing. *)
 
-  Definition merely_rec {A : Type@{i}} {P : Type@{j}} `{IsHProp P} (f : A -> P)
-    : merely A -> P
-    := fun ma => (equiv_smalltype P)
-                 (ma (smalltype P) _ ((equiv_smalltype P)^-1 o f)).
+Section AssumePropResizing.
+  Context `{PropResizing}.
 
-  Definition functor_merely `{Funext} {A B : Type} (f : A -> B)
-    : merely A -> merely B.
+  (** If we assume propositions resizing, then we may as well quantify over propositions in the lowest universe [Set] when defining the truncation.  This reduces the number of universe variables.  We also assume that [Set < i], so that the construction lands in universe [i]. *)
+  Definition imp_Trm@{i | Set < i} (A : Type@{i}) : Type@{i}
+    := Trm@{i Set} A.
+
+  (** Here we use propositional resizing to resize a arbitrary proposition [P] from an arbitrary universe [j] to universe [Set], so there is no constraint on the universe [j].  In particular, we can take [j = i], which shows that [imp_Trm] is a reflective subuniverse of [Type@{i}], since any two maps into a proposition agree. *)
+  Definition imp_Trm_rec@{i j | Set < i} {A : Type@{i}}
+    {P : Type@{j}} `{IsHProp P} (f : A -> P)
+    : imp_Trm@{i} A -> P
+    := fun ma => (equiv_smalltype@{Set j} P)
+                 (ma (smalltype@{Set j} P) _ ((equiv_smalltype@{Set j} P)^-1 o f)).
+
+  (** Similarly, there are no constraints between [i] and [i'] in the next definition, so they could be taken to be equal. *)
+  Definition functor_imp_Trm@{i i' | Set < i, Set < i'} `{Funext}
+    {A : Type@{i}} {A' : Type@{i'}} (f : A -> A')
+    : imp_Trm@{i} A -> imp_Trm@{i'} A'
+    := imp_Trm_rec (trm o f).
+
+  (** Note that [imp_Trm_rec] only computes propositionally. *)
+  Definition imp_Trm_rec_beta@{i j | Set < i} {A : Type@{i}}
+    {P : Type@{j}} `{IsHProp P} (f : A -> P)
+    : imp_Trm_rec@{i j} f o trm == f.
   Proof.
-    srefine (merely_rec (trm o f)).
+    intro a.
+    unfold imp_Trm_rec, trm; cbn beta.
+    apply eisretr@{Set j}.
   Defined.
 
-(* show what is gained by propositional resizing, without mentioning universe levels *)
-  Local Definition typeofid (A : Type) := A -> A.
-
-  Local Definition functor_merely_sameargs `{Funext} {A : Type} (f : typeofid A)
-    : typeofid (merely A) := functor_merely f.
-
-(* a more informative version using universe levels *)
-  Local Definition functor_merely_sameuniv `{Funext} {A B: Type@{i}} (f : A -> B)
-    : merely@{j k} A -> merely@{j k} B:= functor_merely f.    (* requires i <= j & k < j *)
-
-
 End AssumePropResizing.
 
-(* Here, we show what goes wrong without propositional resizing. *)
+(** Above, we needed the constraint [Set < i].  But one can use propositional resizing again to make [imp_Trm] land in the lowest universe, if that is needed.  (We'll in fact let it land in any universe [u].)  To do this, we need to assume [Funext] in the definition of the truncation itself. *)
 
-(* the naive definition *)
-Local Definition merely_rec_naive {A : Type@{i}} {P : Type@{j}} {p:IsHProp@{j} P} (f : A -> P)
-  : merely@{i j} A -> P
-  := fun ma => ma P p f.
+Section TruncationWithFunext.
+  Context `{PropResizing} `{Funext}.
 
-(* the too weak definition *)
-Local Definition functor_merely_weak `{Funext} {A B : Type@{k}} (f : A -> B)
-  : merely@{j k} A -> merely@{k l} B. (* evidently, this requires k<j and l<k *)
-Proof.
-  srefine (merely_rec_naive (trm o f)).
-Defined.
+  (** [Funext] implies that [Trm A] is a proposition, so [PropResizing] can be used to put it in any universe. The construction passes through universe [k], which represents [max(i,Set+1)]. *)
+  Definition resized_Trm@{i k u | i <= k, Set < k} (A : Type@{i})
+    : Type@{u}
+    := smalltype@{u k} (Trm@{i Set} A).
+
+  Definition resized_trm@{i k u | i <= k, Set < k} {A : Type@{i}}
+    : A -> resized_Trm@{i k u} A
+    := (equiv_smalltype _)^-1 o trm.
 
-(* impossible due to universe inconsistency: *)
-Fail Local Definition functor_merely_weak_sameargs `{Funext} {A : Type} (f : typeofid A)
-  : typeofid(merely A) := functor_merely_weak f.
+  Definition resized_Trm_rec@{i j k u | i <= k, Set < k} {A : Type@{i}}
+    {P : Type@{j}} `{IsHProp P} (f : A -> P)
+    : resized_Trm@{i k u} A -> P.
+  Proof.
+    refine (_ o (equiv_smalltype@{u k} _)).
+    exact (fun ma => (equiv_smalltype@{Set j} P)
+                 (ma (smalltype@{Set j} P) _ ((equiv_smalltype@{Set j} P)^-1 o f))).
+  Defined.
 
-(* The following much weaker definition is possible: *)
-Local Definition functor_merely_weak_sameargs_weak `{Funext} {A : Type} (f : typeofid A)
-  : merely A -> merely A := functor_merely_weak f.
+  (** The beta rule is again propositional. *)
+  Definition resized_Trm_rec_beta@{i j k u | i <= k, Set < k} {A : Type@{i}}
+    {P : Type@{j}} `{IsHProp P} (f : A -> P)
+    : resized_Trm_rec@{i j k u} f o resized_trm == f.
+  Proof.
+    intro a.
+    unfold resized_Trm_rec, resized_trm, Trm, trm; cbn beta.
+    rewrite eisretr@{u k}.
+    apply eisretr@{Set j}.
+  Defined.
 
-(* a more general (but still weak) and more informative version using universe levels *)
-Local Definition functor_merely_weak_sameuniv_weak `{Funext} {A B: Type@{i}} (f : A -> B)
-  : merely@{j k} A -> merely@{k l} B:= functor_merely_weak f.
-(* requires i <= j & l < k < j *)
+End TruncationWithFunext.

theories/Metatheory/IntervalImpliesFunext.v

@@ -1,14 +1,16 @@
-(** * Theorems about the homotopical interval. *)
+(** * An interval type implies function extensionality *)
 
 Require Import HoTT.Basics.
 Require Import HIT.Interval.
 Require Import Metatheory.Core Metatheory.FunextVarieties.
 
-(** ** From an interval type, we can prove function extensionality. *)
+(** From an interval type with definitional computation rules on the end points, we can prove function extensionality. *)
 
 Definition funext_type_from_interval : Funext_type
   := WeakFunext_implies_Funext (NaiveFunext_implies_WeakFunext
     (fun A P f g p =>
       let h := fun (x:interval) (a:A) =>
         interval_rec _ (f a) (g a) (p a) x
         in ap h seg)).
+
+(** Note that the converse is also true:  function extensionality implies that an interval type exists, with definitional computation rules.  This is illustrated in TruncImpliesFunext.v. *)

theories/Metatheory/TruncImpliesFunext.v

@@ -1,31 +1,68 @@
-(** * Theorems about trunctions *)
+(** * Propositional truncation implies function extensionality *)
 
 Require Import HoTT.Basics HoTT.Truncations HoTT.Types.Bool.
-Require Import Metatheory.Core Metatheory.FunextVarieties.
+Require Import Metatheory.Core Metatheory.FunextVarieties Metatheory.ImpredicativeTruncation.
 
-(** ** We can construct an interval type as [Trunc -1 Bool] *)
+(** ** An approach using the truncations defined as HITs *)
 
+(** We can construct an interval type as [Trunc -1 Bool]. *)
 Local Definition interval := Trunc (-1) Bool.
 
 Local Definition interval_rec (P : Type) (a b : P) (p : a = b)
-: interval -> P.
+  : interval -> P.
 Proof.
-  unfold interval; intro x.
-  cut { pt : P | pt = b }.
-  { apply pr1. }
-  { strip_truncations.
-    refine (if x then a else b; _).
-    destruct x; (reflexivity || assumption). }
+  (** We define this map by factoring it through the type [{ x : P & x = b}], which is a proposition since it is contractible. *)
+  refine ((pr1 : { x : P & x = b } -> P) o _).
+  apply Trunc_rec.
+  intros [].
+  - exact (a; p).
+  - exact (b; idpath).
 Defined.
 
 Local Definition seg : tr true = tr false :> interval
   := path_ishprop _ _.
 
-(** ** From an interval type, and thus from truncations, we can prove function extensionality. *)
-
+(** From an interval type, and thus from truncations, we can prove function extensionality. *)
 Definition funext_type_from_trunc : Funext_type
   := WeakFunext_implies_Funext (NaiveFunext_implies_WeakFunext
     (fun A P f g p =>
       let h := fun (x:interval) (a:A) =>
         interval_rec _ (f a) (g a) (p a) x
         in ap h seg)).
+
+(** ** An approach without using HITs *)
+
+(** Assuming [Funext] (and not propositional resizing), the construction [Trm] in ImpredicativeTruncation.v applied to [Bool] gives an interval type with definitional computation on the end points.  So we see that function extensionality is equivalent to the existence of an interval type. *)
+
+Section AssumeFunext.
+  Context `{Funext}.
+
+  Definition finterval := Trm Bool.
+
+  Definition finterval_rec (P : Type) (a b : P) (p : a = b)
+    : finterval -> P.
+  Proof.
+    refine ((pr1 : { x : P & x = b } -> P) o _).
+    apply Trm_rec.
+    intros [].
+    - exact (a; p).
+    - exact (b; idpath).
+  Defined.
+
+  (** As an example, we check that it computes on [true]. *)
+  Definition finterval_rec_beta (P : Type) (a b : P) (p : a = b)
+    : finterval_rec P a b p (trm true) = a
+    := idpath.
+
+  Definition fseg : trm true = trm false :> finterval
+    := path_ishprop _ _.
+
+  (** To verify that our interval type is good enough, we use it to prove function extensionality. *)
+  Definition funext_type_from_finterval : Funext_type
+    := WeakFunext_implies_Funext (NaiveFunext_implies_WeakFunext
+      (fun A P f g p =>
+        let h := fun (x:finterval) (a:A) =>
+          finterval_rec _ (f a) (g a) (p a) x
+          in ap h fseg)).
+
+End AssumeFunext.