(* -*- mode: coq; mode: visual-line -*-  *)
(** * Impredicative truncations. *)

Require Import HoTT.Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import PropResizing.PropResizing.
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. *)

Section AssumePropResizing.
  Context `{PropResizing}.

  Definition merely@{i j} (A : Type@{i}) : Type@{i}
    := forall P:Type@{j}, IsHProp P -> (A -> P) -> P.   (* requires j < i *)

  Definition trm {A} : A -> merely A
    := fun a P HP f => f a.

  Global Instance ishprop_merely `{Funext} (A : Type) : IsHProp (merely A).
H: PropResizing
H0: Funext
A: Type
IsHProp (merely A)
  Proof.
H: PropResizing
H0: Funext
A: Type
IsHProp (merely A)
    exact _.
  Defined.

  Definition merely_rec {A : Type@{i}} {P : Type@{j}} `{IsHProp P} (f : A -> P)
    : merely A -> P
    := fun ma => (equiv_resize_hprop P)^-1
                 (ma (resize_hprop P) _ (equiv_resize_hprop P o f)).

  Definition functor_merely `{Funext} {A B : Type} (f : A -> B)
    : merely A -> merely B.
H: PropResizing
H0: Funext
A, B: Type
f: A -> B
merely A -> merely B
  Proof.
H: PropResizing
H0: Funext
A, B: Type
f: A -> B
merely A -> merely B
    srefine (merely_rec (trm o f)).
  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. *)

(* 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.

(* 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 *)
H: Funext
A, B: Type
f: A -> B
merely A -> merely B
Proof.
H: Funext
A, B: Type
f: A -> B
merely A -> merely B
  srefine (merely_rec_naive (trm o f)).
Defined.

(* 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.
The command has indeed failed with message:
In environment
H : Funext
A : Type
f : typeofid A
The term "functor_merely_weak f" has type
 "merely A -> merely A"
while it is expected to have type
 "typeofid (merely A)"
(universe inconsistency: Cannot enforce
ImpredicativeTruncation.249 <=
ImpredicativeTruncation.251 because
ImpredicativeTruncation.251
< ImpredicativeTruncation.249).

(* 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.

(* 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 *)