(** * Truncatedness *)

Require Import
  Basics.Overture
  Basics.Contractible
  Basics.Equivalences
  Basics.Tactics
  Basics.Nat
  Basics.Iff.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Set Universe Minimization ToSet.

Local Open Scope trunc_scope.
Local Open Scope path_scope.
Generalizable Variables A B m n f.

(** ** Notation for truncation-levels *)
Open Scope trunc_scope.

(** Increase a truncation index by a natural number. *)
Fixpoint trunc_index_inc@{} (k : trunc_index) (n : nat)
  : trunc_index
  := match n with
      | O => k
      | S m => (trunc_index_inc k m).+1
    end.

(** This is a variation that inserts the successor operations in the other order.  This is sometimes convenient. *)
Fixpoint trunc_index_inc'@{} (k : trunc_index) (n : nat)
  : trunc_index
  := match n with
      | O => k
      | S m => (trunc_index_inc' k.+1 m)
    end.

Definition trunc_index_inc'_succ@{} (n : nat) (k : trunc_index)
  : trunc_index_inc' k.+1 n = (trunc_index_inc' k n).+1.
n: nat
k: trunc_index
trunc_index_inc' k.+1 n = (trunc_index_inc' k n).+1
Proof.
n: nat
k: trunc_index
trunc_index_inc' k.+1 n = (trunc_index_inc' k n).+1
  revert k; simple_induction n n IHn; intro k.
k: trunc_index
trunc_index_inc' k.+1 0 = (trunc_index_inc' k 0).+1
n: nat
IHn: forall k : trunc_index, trunc_index_inc' k.+1 n = (trunc_index_inc' k n).+1
k: trunc_index
trunc_index_inc' k.+1 n.+1 =
(trunc_index_inc' k n.+1).+1
  -
k: trunc_index
trunc_index_inc' k.+1 0 = (trunc_index_inc' k 0).+1 reflexivity.
  -
n: nat
IHn: forall k : trunc_index, trunc_index_inc' k.+1 n = (trunc_index_inc' k n).+1
k: trunc_index
trunc_index_inc' k.+1 n.+1 =
(trunc_index_inc' k n.+1).+1 exact (IHn k.+1).
Defined.

Definition trunc_index_inc_agree@{} (k : trunc_index) (n : nat)
  : trunc_index_inc k n = trunc_index_inc' k n.
k: trunc_index
n: nat
trunc_index_inc k n = trunc_index_inc' k n
Proof.
k: trunc_index
n: nat
trunc_index_inc k n = trunc_index_inc' k n
  simple_induction n n IHn.
k: trunc_index
trunc_index_inc k 0 = trunc_index_inc' k 0
k: trunc_index
n: nat
IHn: trunc_index_inc k n = trunc_index_inc' k n
trunc_index_inc k n.+1 = trunc_index_inc' k n.+1
  -
k: trunc_index
trunc_index_inc k 0 = trunc_index_inc' k 0 reflexivity.
  -
k: trunc_index
n: nat
IHn: trunc_index_inc k n = trunc_index_inc' k n
trunc_index_inc k n.+1 = trunc_index_inc' k n.+1 simpl.
k: trunc_index
n: nat
IHn: trunc_index_inc k n = trunc_index_inc' k n
(trunc_index_inc k n).+1 = trunc_index_inc' k.+1 n
    refine (ap _ IHn @ _).
k: trunc_index
n: nat
IHn: trunc_index_inc k n = trunc_index_inc' k n
(trunc_index_inc' k n).+1 = trunc_index_inc' k.+1 n
    symmetry; apply trunc_index_inc'_succ.
Defined.

Definition nat_to_trunc_index@{} (n : nat) : trunc_index
  := (trunc_index_inc minus_two n).+2.

Coercion nat_to_trunc_index : nat >-> trunc_index.

Definition trunc_index_inc'_0n (n : nat)
  : trunc_index_inc' 0%nat n = n.
n: nat
trunc_index_inc' 0%nat n = n
Proof.
n: nat
trunc_index_inc' 0%nat n = n
  induction n as [|n p].
trunc_index_inc' 0%nat 0 = 0%nat
n: nat
p: trunc_index_inc' 0%nat n = n
trunc_index_inc' 0%nat n.+1 = n.+1%nat
  1: reflexivity.
n: nat
p: trunc_index_inc' 0%nat n = n
trunc_index_inc' 0%nat n.+1 = n.+1%nat
  refine (trunc_index_inc'_succ _ _ @ _).
n: nat
p: trunc_index_inc' 0%nat n = n
(trunc_index_inc' (trunc_index_inc minus_two 0).+1
   n.+1).+1 = n.+1%nat
  exact (ap _ p).
Defined.

Definition int_to_trunc_index@{} (v : Decimal.int) : option trunc_index
  := match v with
     | Decimal.Pos d => Some (nat_to_trunc_index (Nat.of_uint d))
     | Decimal.Neg d => match Nat.of_uint d with
                        | 2%nat => Some minus_two
                        | 1%nat => Some (minus_two.+1)
                        | 0%nat => Some (minus_two.+2)
                        | _ => None
                        end
     end.

Definition num_int_to_trunc_index@{} (v : Numeral.int) : option trunc_index :=
  match v with
  | Numeral.IntDec v => int_to_trunc_index v
  | Numeral.IntHex _ => None
  end.

Fixpoint trunc_index_to_little_uint@{} n acc :=
  match n with
  | minus_two => acc
  | minus_two.+1 => acc
  | minus_two.+2 => acc
  | trunc_S n => trunc_index_to_little_uint n (Decimal.Little.succ acc)
  end.

Definition trunc_index_to_int@{} n :=
  match n with
  | minus_two => Decimal.Neg (Nat.to_uint 2)
  | minus_two.+1 => Decimal.Neg (Nat.to_uint 1)
  | n => Decimal.Pos (Decimal.rev (trunc_index_to_little_uint n Decimal.zero))
  end.

Definition trunc_index_to_num_int@{} n :=
  Numeral.IntDec (trunc_index_to_int n).

(** This allows us to use notation like (-2) and 42 for a [trunc_index]. *)
Number Notation trunc_index num_int_to_trunc_index trunc_index_to_num_int
  : trunc_scope.

(** Sends a [trunc_index] [n] to the natural number [n+2]. *)
Fixpoint trunc_index_to_nat (n : trunc_index) : nat
  := match n with
    | minus_two => 0%nat
    | n'.+1 => (trunc_index_to_nat n').+1
    end.

(** ** Arithmetic on truncation-levels. *)
Fixpoint trunc_index_add@{} (m n : trunc_index) : trunc_index
  := match m with
       | -2 => n
       | m'.+1 => (trunc_index_add m' n).+1
     end.

Notation "m +2+ n" := (trunc_index_add m n) : trunc_scope.

Definition trunc_index_add_minus_two@{} m
  : m +2+ -2 = m.
m: trunc_index
m +2+ -2 = m
Proof.
m: trunc_index
m +2+ -2 = m
  simple_induction m m IHm.
-2 +2+ -2 = -2
m: trunc_index
IHm: m +2+ -2 = m
m.+1 +2+ -2 = m.+1
  1: reflexivity.
m: trunc_index
IHm: m +2+ -2 = m
m.+1 +2+ -2 = m.+1
  cbn; apply ap.
m: trunc_index
IHm: m +2+ -2 = m
m +2+ -2 = m
  assumption.
Defined.

Definition trunc_index_add_succ@{} m n
  : m +2+ n.+1 = (m +2+ n).+1.
m, n: trunc_index
m +2+ n.+1 = (m +2+ n).+1
Proof.
m, n: trunc_index
m +2+ n.+1 = (m +2+ n).+1
  simple_induction m m IHm.
n: trunc_index
-2 +2+ n.+1 = (-2 +2+ n).+1
n, m: trunc_index
IHm: m +2+ n.+1 = (m +2+ n).+1
m.+1 +2+ n.+1 = (m.+1 +2+ n).+1
  1: reflexivity.
n, m: trunc_index
IHm: m +2+ n.+1 = (m +2+ n).+1
m.+1 +2+ n.+1 = (m.+1 +2+ n).+1
  cbn; apply ap; assumption.
Defined.

Definition trunc_index_add_comm@{} m n
  : m +2+ n = n +2+ m.
m, n: trunc_index
m +2+ n = n +2+ m
Proof.
m, n: trunc_index
m +2+ n = n +2+ m
  simple_induction n n IHn.
m: trunc_index
m +2+ -2 = -2 +2+ m
m, n: trunc_index
IHn: m +2+ n = n +2+ m
m +2+ n.+1 = n.+1 +2+ m
  -
m: trunc_index
m +2+ -2 = -2 +2+ m apply trunc_index_add_minus_two.
  -
m, n: trunc_index
IHn: m +2+ n = n +2+ m
m +2+ n.+1 = n.+1 +2+ m exact (trunc_index_add_succ _ _ @ ap trunc_S IHn).
Defined.

Fixpoint trunc_index_leq@{} (m n : trunc_index) : Type0
  := match m, n with
       | -2, _ => Unit
       | m'.+1, -2 => Empty
       | m'.+1, n'.+1 => trunc_index_leq m' n'
     end.

Existing Class trunc_index_leq.

Notation "m <= n" := (trunc_index_leq m n) : trunc_scope.

Instance trunc_index_leq_minus_two_n@{} n : -2 <= n := tt.

Instance trunc_index_leq_succ@{} n : n <= n.+1.
n: trunc_index
n <= n.+1
Proof.
n: trunc_index
n <= n.+1
  by induction n as [|n IHn] using trunc_index_ind.
Defined.

Definition trunc_index_pred@{} : trunc_index -> trunc_index.
trunc_index -> trunc_index
Proof.
trunc_index -> trunc_index
  intros [|m].
trunc_index
m: trunc_index
trunc_index
  1: exact (-2).
m: trunc_index
trunc_index
  exact m.
Defined.

Notation "n '.-1'" := (trunc_index_pred n) : trunc_scope.
Notation "n '.-2'" := (n.-1.-1) : trunc_scope.

Definition trunc_index_succ_pred@{} (n : nat)
  : (n.-1).+1 = n
  := idpath.

Definition trunc_index_succ_pred'@{} (n : trunc_index)
  : -1 <= n -> (n.-1).+1 = n.
n: trunc_index
-1 <= n -> n.-1.+1 = n
Proof.
n: trunc_index
-1 <= n -> n.-1.+1 = n
  destruct n.
-1 <= -2 -> (-2).-1.+1 = -2
n: trunc_index
-1 <= n.+1 -> n.+1.-1.+1 = n.+1
  1: contradiction.
n: trunc_index
-1 <= n.+1 -> n.+1.-1.+1 = n.+1
  reflexivity.
Defined.

Definition trunc_index_add_pred@{} (m : trunc_index) (n : nat)
  : m +2+ n.-1 = (m +2+ n).-1.
m: trunc_index
n: nat
m +2+ n.-1 = (m +2+ n).-1
Proof.
m: trunc_index
n: nat
m +2+ n.-1 = (m +2+ n).-1
  destruct m.
n: nat
-2 +2+ n.-1 = (-2 +2+ n).-1
m: trunc_index
n: nat
m.+1 +2+ n.-1 = (m.+1 +2+ n).-1
  1: reflexivity.
m: trunc_index
n: nat
m.+1 +2+ n.-1 = (m.+1 +2+ n).-1
  (* The RHS is definitionally [m +2+ n], which is definitionally [m +2+ n.-1.+1], so this finishes it off: *)
  symmetry; napply trunc_index_add_succ.
Defined.

Definition trunc_index_add_pred'@{} (m n : trunc_index)
  : -1 <= n -> m +2+ n.-1 = (m +2+ n).-1.
m, n: trunc_index
-1 <= n -> m +2+ n.-1 = (m +2+ n).-1
Proof.
m, n: trunc_index
-1 <= n -> m +2+ n.-1 = (m +2+ n).-1
  destruct m.
n: trunc_index
-1 <= n -> -2 +2+ n.-1 = (-2 +2+ n).-1
m, n: trunc_index
-1 <= n -> m.+1 +2+ n.-1 = (m.+1 +2+ n).-1
  1: reflexivity.
m, n: trunc_index
-1 <= n -> m.+1 +2+ n.-1 = (m.+1 +2+ n).-1
  destruct n.
m: trunc_index
-1 <= -2 -> m.+1 +2+ (-2).-1 = (m.+1 +2+ -2).-1
m, n: trunc_index
-1 <= n.+1 -> m.+1 +2+ n.+1.-1 = (m.+1 +2+ n.+1).-1
  1: contradiction.
m, n: trunc_index
-1 <= n.+1 -> m.+1 +2+ n.+1.-1 = (m.+1 +2+ n.+1).-1
  intros _.
m, n: trunc_index
m.+1 +2+ n.+1.-1 = (m.+1 +2+ n.+1).-1
  (* The RHS is definitionally [m +2+ n], which is definitionally [m +2+ n.-1.+1], so this finishes it off: *)
  symmetry; napply trunc_index_add_succ.
Defined.

Definition trunc_index_leq_minus_two@{} {n}
  : n <= -2 -> n = -2.
n: trunc_index
n <= -2 -> n = -2
Proof.
n: trunc_index
n <= -2 -> n = -2
  destruct n.
-2 <= -2 -> -2 = -2
n: trunc_index
n.+1 <= -2 -> n.+1 = -2
  1: reflexivity.
n: trunc_index
n.+1 <= -2 -> n.+1 = -2
  contradiction.
Defined.

Definition trunc_index_leq_succ'@{} n m
  : n <= m -> n <= m.+1.
n, m: trunc_index
n <= m -> n <= m.+1
Proof.
n, m: trunc_index
n <= m -> n <= m.+1
  revert m.
n: trunc_index
forall m : trunc_index, n <= m -> n <= m.+1
  induction n as [|n IHn] using trunc_index_ind.
forall m : trunc_index, -2 <= m -> -2 <= m.+1
n: trunc_index
IHn: forall m : trunc_index, n <= m -> n <= m.+1
forall m : trunc_index, n.+1 <= m -> n.+1 <= m.+1
  1: exact _.
n: trunc_index
IHn: forall m : trunc_index, n <= m -> n <= m.+1
forall m : trunc_index, n.+1 <= m -> n.+1 <= m.+1
  intros m p; cbn.
n: trunc_index
IHn: forall m : trunc_index, n <= m -> n <= m.+1
m: trunc_index
p: n.+1 <= m
n <= m
  induction m as [|m IHm] using trunc_index_ind.
n: trunc_index
IHn: forall m : trunc_index, n <= m -> n <= m.+1
p: n.+1 <= -2
n <= -2
n: trunc_index
IHn: forall m : trunc_index, n <= m -> n <= m.+1
m: trunc_index
p: n.+1 <= m.+1
IHm: n.+1 <= m -> n <= m
n <= m.+1
  1: destruct p.
n: trunc_index
IHn: forall m : trunc_index, n <= m -> n <= m.+1
m: trunc_index
p: n.+1 <= m.+1
IHm: n.+1 <= m -> n <= m
n <= m.+1
  apply IHn, p.
Defined.

Instance trunc_index_leq_refl@{}
  : Reflexive trunc_index_leq.
Reflexive trunc_index_leq
Proof.
Reflexive trunc_index_leq
  intro n.
n: trunc_index
n <= n
  by induction n as [|n IHn] using trunc_index_ind.
Defined.

Instance trunc_index_leq_transitive@{}
  : Transitive trunc_index_leq.
Transitive trunc_index_leq
Proof.
Transitive trunc_index_leq
  intros a b c p q.
a, b, c: trunc_index
p: a <= b
q: b <= c
a <= c
  revert b a c p q.
forall b a c : trunc_index, a <= b -> b <= c -> a <= c
  induction b as [|b IHb] using trunc_index_ind.
forall a c : trunc_index, a <= -2 -> -2 <= c -> a <= c
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
forall a c : trunc_index,
a <= b.+1 -> b.+1 <= c -> a <= c
  {
forall a c : trunc_index, a <= -2 -> -2 <= c -> a <= c intros a c p.
a, c: trunc_index
p: a <= -2
-2 <= c -> a <= c
    by destruct (trunc_index_leq_minus_two p). }
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
forall a c : trunc_index,
a <= b.+1 -> b.+1 <= c -> a <= c
  induction a as [|a IHa] using trunc_index_ind;
  induction c as [|c IHc] using trunc_index_ind.
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
-2 <= b.+1 -> b.+1 <= -2 -> -2 <= -2
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
c: trunc_index
IHc: -2 <= b.+1 -> b.+1 <= c -> -2 <= c
-2 <= b.+1 -> b.+1 <= c.+1 -> -2 <= c.+1
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
a: trunc_index
IHa: forall c : trunc_index, a <= b.+1 -> b.+1 <= c -> a <= c
a.+1 <= b.+1 -> b.+1 <= -2 -> a.+1 <= -2
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
a: trunc_index
IHa: forall c : trunc_index, a <= b.+1 -> b.+1 <= c -> a <= c
c: trunc_index
IHc: a.+1 <= b.+1 -> b.+1 <= c -> a.+1 <= c
a.+1 <= b.+1 -> b.+1 <= c.+1 -> a.+1 <= c.+1
  all: intros.
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
p: -2 <= b.+1
q: b.+1 <= -2
-2 <= -2
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
c: trunc_index
IHc: -2 <= b.+1 -> b.+1 <= c -> -2 <= c
p: -2 <= b.+1
q: b.+1 <= c.+1
-2 <= c.+1
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
a: trunc_index
IHa: forall c : trunc_index, a <= b.+1 -> b.+1 <= c -> a <= c
p: a.+1 <= b.+1
q: b.+1 <= -2
a.+1 <= -2
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
a: trunc_index
IHa: forall c : trunc_index, a <= b.+1 -> b.+1 <= c -> a <= c
c: trunc_index
IHc: a.+1 <= b.+1 -> b.+1 <= c -> a.+1 <= c
p: a.+1 <= b.+1
q: b.+1 <= c.+1
a.+1 <= c.+1
  1,2: exact tt.
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
a: trunc_index
IHa: forall c : trunc_index, a <= b.+1 -> b.+1 <= c -> a <= c
p: a.+1 <= b.+1
q: b.+1 <= -2
a.+1 <= -2
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
a: trunc_index
IHa: forall c : trunc_index, a <= b.+1 -> b.+1 <= c -> a <= c
c: trunc_index
IHc: a.+1 <= b.+1 -> b.+1 <= c -> a.+1 <= c
p: a.+1 <= b.+1
q: b.+1 <= c.+1
a.+1 <= c.+1
  1: contradiction.
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
a: trunc_index
IHa: forall c : trunc_index, a <= b.+1 -> b.+1 <= c -> a <= c
c: trunc_index
IHc: a.+1 <= b.+1 -> b.+1 <= c -> a.+1 <= c
p: a.+1 <= b.+1
q: b.+1 <= c.+1
a.+1 <= c.+1
  cbn in p, q; cbn.
b: trunc_index
IHb: forall a c : trunc_index, a <= b -> b <= c -> a <= c
a: trunc_index
IHa: forall c : trunc_index, a <= b.+1 -> b.+1 <= c -> a <= c
c: trunc_index
IHc: a.+1 <= b.+1 -> b.+1 <= c -> a.+1 <= c
p: a <= b
q: b <= c
a <= c
  by apply IHb.
Defined.

Definition trunc_index_leq_add@{} n m
  : n <= m +2+ n.
n, m: trunc_index
n <= m +2+ n
Proof.
n, m: trunc_index
n <= m +2+ n
  simple_induction m m IHm.
n: trunc_index
n <= -2 +2+ n
n, m: trunc_index
IHm: n <= m +2+ n
n <= m.+1 +2+ n
  -
n: trunc_index
n <= -2 +2+ n reflexivity.
  -
n, m: trunc_index
IHm: n <= m +2+ n
n <= m.+1 +2+ n rapply trunc_index_leq_transitive.
Defined.

Definition trunc_index_leq_add'@{} n m
  : n <= n +2+ m.
n, m: trunc_index
n <= n +2+ m
Proof.
n, m: trunc_index
n <= n +2+ m
  rewrite trunc_index_add_comm.
n, m: trunc_index
n <= m +2+ n
  apply trunc_index_leq_add.
Defined.

Fixpoint trunc_index_min@{} (n m : trunc_index)
  : trunc_index.
trunc_index_min: trunc_index ->
trunc_index -> trunc_index
n, m: trunc_index
trunc_index
Proof.
trunc_index_min: trunc_index ->
trunc_index -> trunc_index
n, m: trunc_index
trunc_index
  destruct n.
trunc_index_min: trunc_index ->
trunc_index -> trunc_index
m: trunc_index
trunc_index
trunc_index_min: trunc_index ->
trunc_index -> trunc_index
n, m: trunc_index
trunc_index
  1: exact (-2).
trunc_index_min: trunc_index ->
trunc_index -> trunc_index
n, m: trunc_index
trunc_index
  destruct m.
trunc_index_min: trunc_index ->
trunc_index -> trunc_index
n: trunc_index
trunc_index
trunc_index_min: trunc_index ->
trunc_index -> trunc_index
n, m: trunc_index
trunc_index
  1: exact (-2).
trunc_index_min: trunc_index ->
trunc_index -> trunc_index
n, m: trunc_index
trunc_index
  exact (trunc_index_min n m).+1.
Defined.

Definition trunc_index_min_minus_two@{} n
  : trunc_index_min n (-2) = -2.
n: trunc_index
trunc_index_min n (-2) = -2
Proof.
n: trunc_index
trunc_index_min n (-2) = -2
  by destruct n.
Defined.

Definition trunc_index_min_swap@{} n m
  : trunc_index_min n m = trunc_index_min m n.
n, m: trunc_index
trunc_index_min n m = trunc_index_min m n
Proof.
n, m: trunc_index
trunc_index_min n m = trunc_index_min m n
  revert m.
n: trunc_index
forall m : trunc_index,
trunc_index_min n m = trunc_index_min m n
  simple_induction n n IHn; intro m.
m: trunc_index
trunc_index_min (-2) m = trunc_index_min m (-2)
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m = trunc_index_min m n
m: trunc_index
trunc_index_min n.+1 m = trunc_index_min m n.+1
  {
m: trunc_index
trunc_index_min (-2) m = trunc_index_min m (-2) symmetry.
m: trunc_index
trunc_index_min m (-2) = trunc_index_min (-2) m
    apply trunc_index_min_minus_two. }
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m = trunc_index_min m n
m: trunc_index
trunc_index_min n.+1 m = trunc_index_min m n.+1
  simple_induction m m IHm.
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m = trunc_index_min m n
trunc_index_min n.+1 (-2) = trunc_index_min (-2) n.+1
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m = trunc_index_min m n
m: trunc_index
IHm: trunc_index_min n.+1 m = trunc_index_min m n.+1
trunc_index_min n.+1 m.+1 = trunc_index_min m.+1 n.+1
  1: reflexivity.
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m = trunc_index_min m n
m: trunc_index
IHm: trunc_index_min n.+1 m = trunc_index_min m n.+1
trunc_index_min n.+1 m.+1 = trunc_index_min m.+1 n.+1
  cbn; apply ap, IHn.
Defined.

Definition trunc_index_min_path@{} n m
  : (trunc_index_min n m = n) + (trunc_index_min n m = m).
n, m: trunc_index
(trunc_index_min n m = n) + (trunc_index_min n m = m)
Proof.
n, m: trunc_index
(trunc_index_min n m = n) + (trunc_index_min n m = m)
  revert m; simple_induction n n IHn; intro m.
m: trunc_index
(trunc_index_min (-2) m = -2) +
(trunc_index_min (-2) m = m)
n: trunc_index
IHn: forall m : trunc_index, (trunc_index_min n m = n) + (trunc_index_min n m = m)
m: trunc_index
(trunc_index_min n.+1 m = n.+1) +
(trunc_index_min n.+1 m = m)
  1: by apply inl.
n: trunc_index
IHn: forall m : trunc_index, (trunc_index_min n m = n) + (trunc_index_min n m = m)
m: trunc_index
(trunc_index_min n.+1 m = n.+1) +
(trunc_index_min n.+1 m = m)
  simple_induction m m IHm.
n: trunc_index
IHn: forall m : trunc_index, (trunc_index_min n m = n) + (trunc_index_min n m = m)
(trunc_index_min n.+1 (-2) = n.+1) +
(trunc_index_min n.+1 (-2) = -2)
n: trunc_index
IHn: forall m : trunc_index, (trunc_index_min n m = n) + (trunc_index_min n m = m)
m: trunc_index
IHm: (trunc_index_min n.+1 m = n.+1) + (trunc_index_min n.+1 m = m)
(trunc_index_min n.+1 m.+1 = n.+1) +
(trunc_index_min n.+1 m.+1 = m.+1)
  1: by apply inr.
n: trunc_index
IHn: forall m : trunc_index, (trunc_index_min n m = n) + (trunc_index_min n m = m)
m: trunc_index
IHm: (trunc_index_min n.+1 m = n.+1) + (trunc_index_min n.+1 m = m)
(trunc_index_min n.+1 m.+1 = n.+1) +
(trunc_index_min n.+1 m.+1 = m.+1)
  destruct (IHn m).
n: trunc_index
IHn: forall m : trunc_index, (trunc_index_min n m = n) + (trunc_index_min n m = m)
m: trunc_index
IHm: (trunc_index_min n.+1 m = n.+1) + (trunc_index_min n.+1 m = m)
p: trunc_index_min n m = n
(trunc_index_min n.+1 m.+1 = n.+1) +
(trunc_index_min n.+1 m.+1 = m.+1)
n: trunc_index
IHn: forall m : trunc_index, (trunc_index_min n m = n) + (trunc_index_min n m = m)
m: trunc_index
IHm: (trunc_index_min n.+1 m = n.+1) + (trunc_index_min n.+1 m = m)
p: trunc_index_min n m = m
(trunc_index_min n.+1 m.+1 = n.+1) +
(trunc_index_min n.+1 m.+1 = m.+1)
  1: apply inl.
n: trunc_index
IHn: forall m : trunc_index, (trunc_index_min n m = n) + (trunc_index_min n m = m)
m: trunc_index
IHm: (trunc_index_min n.+1 m = n.+1) + (trunc_index_min n.+1 m = m)
p: trunc_index_min n m = n
trunc_index_min n.+1 m.+1 = n.+1
n: trunc_index
IHn: forall m : trunc_index, (trunc_index_min n m = n) + (trunc_index_min n m = m)
m: trunc_index
IHm: (trunc_index_min n.+1 m = n.+1) + (trunc_index_min n.+1 m = m)
p: trunc_index_min n m = m
(trunc_index_min n.+1 m.+1 = n.+1) +
(trunc_index_min n.+1 m.+1 = m.+1)
  2: apply inr.
n: trunc_index
IHn: forall m : trunc_index, (trunc_index_min n m = n) + (trunc_index_min n m = m)
m: trunc_index
IHm: (trunc_index_min n.+1 m = n.+1) + (trunc_index_min n.+1 m = m)
p: trunc_index_min n m = n
trunc_index_min n.+1 m.+1 = n.+1
n: trunc_index
IHn: forall m : trunc_index, (trunc_index_min n m = n) + (trunc_index_min n m = m)
m: trunc_index
IHm: (trunc_index_min n.+1 m = n.+1) + (trunc_index_min n.+1 m = m)
p: trunc_index_min n m = m
trunc_index_min n.+1 m.+1 = m.+1
  1,2: cbn; by apply ap.
Defined.

Definition trunc_index_min_leq_left@{} (n m : trunc_index)
  : trunc_index_min n m <= n.
n, m: trunc_index
trunc_index_min n m <= n
Proof.
n, m: trunc_index
trunc_index_min n m <= n
  revert n m.
forall n m : trunc_index, trunc_index_min n m <= n
  refine (trunc_index_ind _ _ _); [ | intros n IHn ].
forall m : trunc_index, trunc_index_min (-2) m <= -2
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m <= n
forall m : trunc_index, trunc_index_min n.+1 m <= n.+1
  all: refine (trunc_index_ind _ _ _); [ | intros m IHm ].
trunc_index_min (-2) (-2) <= -2
m: trunc_index
IHm: trunc_index_min (-2) m <= -2
trunc_index_min (-2) m.+1 <= -2
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m <= n
trunc_index_min n.+1 (-2) <= n.+1
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m <= n
m: trunc_index
IHm: trunc_index_min n.+1 m <= n.+1
trunc_index_min n.+1 m.+1 <= n.+1
  all: try exact tt.
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m <= n
m: trunc_index
IHm: trunc_index_min n.+1 m <= n.+1
trunc_index_min n.+1 m.+1 <= n.+1
  exact (IHn m).
Defined.

Definition trunc_index_min_leq_right@{} (n m : trunc_index)
  : trunc_index_min n m <= m.
n, m: trunc_index
trunc_index_min n m <= m
Proof.
n, m: trunc_index
trunc_index_min n m <= m
  revert n m.
forall n m : trunc_index, trunc_index_min n m <= m
  refine (trunc_index_ind _ _ _); [ | intros n IHn ].
forall m : trunc_index, trunc_index_min (-2) m <= m
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m <= m
forall m : trunc_index, trunc_index_min n.+1 m <= m
  all: refine (trunc_index_ind _ _ _); [ | intros m IHm ].
trunc_index_min (-2) (-2) <= -2
m: trunc_index
IHm: trunc_index_min (-2) m <= m
trunc_index_min (-2) m.+1 <= m.+1
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m <= m
trunc_index_min n.+1 (-2) <= -2
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m <= m
m: trunc_index
IHm: trunc_index_min n.+1 m <= m
trunc_index_min n.+1 m.+1 <= m.+1
  all: try exact tt.
n: trunc_index
IHn: forall m : trunc_index, trunc_index_min n m <= m
m: trunc_index
IHm: trunc_index_min n.+1 m <= m
trunc_index_min n.+1 m.+1 <= m.+1
  exact (IHn m).
Defined.

(** ** Truncatedness proper. *)

(** A contractible space is (-2)-truncated, by definition. This function is the identity, so there is never any need to actually use it, but it exists to be found in searches. *)
Definition contr_istrunc_minus_two `{H : IsTrunc (-2) A} : Contr A
  := H.

(** Truncation levels are cumulative. *)
Instance istrunc_paths' {n : trunc_index} {A : Type} `{IsTrunc n A}
  : forall x y : A, IsTrunc n (x = y) | 1000.
n: trunc_index
A: Type
IsTrunc0: IsTrunc n A
forall x y : A, IsTrunc n (x = y)
Proof.
n: trunc_index
A: Type
IsTrunc0: IsTrunc n A
forall x y : A, IsTrunc n (x = y)
  generalize dependent A.
n: trunc_index
forall A : Type,
IsTrunc n A -> forall x y : A, IsTrunc n (x = y)
  simple_induction n n IH; simpl; intros A H x y.
A: Type
H: Contr A
x, y: A
Contr (x = y)
n: trunc_index
IH: forall A : Type,
IsTrunc n A -> forall x y : A, IsTrunc n (x = y)
A: Type
H: IsTrunc n.+1 A
x, y: A
IsTrunc n.+1 (x = y)
  -
A: Type
H: Contr A
x, y: A
Contr (x = y) apply contr_paths_contr.
  -
n: trunc_index
IH: forall A : Type,
IsTrunc n A -> forall x y : A, IsTrunc n (x = y)
A: Type
H: IsTrunc n.+1 A
x, y: A
IsTrunc n.+1 (x = y) apply istrunc_S.
n: trunc_index
IH: forall A : Type,
IsTrunc n A -> forall x y : A, IsTrunc n (x = y)
A: Type
H: IsTrunc n.+1 A
x, y: A
forall x0 y0 : x = y, IsTrunc n (x0 = y0)  rapply IH.
Defined.

Instance istrunc_succ {n : trunc_index} {A : Type} `{IsTrunc n A}
  : IsTrunc n.+1 A | 1000.
n: trunc_index
A: Type
IsTrunc0: IsTrunc n A
IsTrunc n.+1 A
Proof.
n: trunc_index
A: Type
IsTrunc0: IsTrunc n A
IsTrunc n.+1 A
  apply istrunc_S.
n: trunc_index
A: Type
IsTrunc0: IsTrunc n A
forall x y : A, IsTrunc n (x = y)
  exact istrunc_paths'.
Defined.

(** This could be an [Instance] (with very high priority, so it doesn't get applied trivially).  However, we haven't given typeclass search any hints allowing it to solve goals like [m <= n], so it would only ever be used trivially.  *)
Definition istrunc_leq {m n} (Hmn : m <= n) `{IsTrunc m A}
  : IsTrunc n A.
m, n: trunc_index
Hmn: m <= n
A: Type
IsTrunc0: IsTrunc m A
IsTrunc n A
Proof.
m, n: trunc_index
Hmn: m <= n
A: Type
IsTrunc0: IsTrunc m A
IsTrunc n A
  generalize dependent A; generalize dependent m.
n: trunc_index
forall m : trunc_index,
m <= n -> forall A : Type, IsTrunc m A -> IsTrunc n A
  simple_induction n n' IH;
    intros [ | m'] Hmn A ? .
Hmn: -2 <= -2
A: Type
IsTrunc0: Contr A
Contr A
m': trunc_index
Hmn: m'.+1 <= -2
A: Type
IsTrunc0: IsTrunc m'.+1 A
Contr A
n': trunc_index
IH: forall m : trunc_index,
m <= n' ->
forall A : Type, IsTrunc m A -> IsTrunc n' A
Hmn: -2 <= n'.+1
A: Type
IsTrunc0: Contr A
IsTrunc n'.+1 A
n': trunc_index
IH: forall m : trunc_index,
m <= n' ->
forall A : Type, IsTrunc m A -> IsTrunc n' A
m': trunc_index
Hmn: m'.+1 <= n'.+1
A: Type
IsTrunc0: IsTrunc m'.+1 A
IsTrunc n'.+1 A
  - (* -2, -2 *)
Hmn: -2 <= -2
A: Type
IsTrunc0: Contr A
Contr A assumption.
  - (* S m', -2 *)
m': trunc_index
Hmn: m'.+1 <= -2
A: Type
IsTrunc0: IsTrunc m'.+1 A
Contr A destruct Hmn.
  - (* -2, S n' *)
n': trunc_index
IH: forall m : trunc_index,
m <= n' ->
forall A : Type, IsTrunc m A -> IsTrunc n' A
Hmn: -2 <= n'.+1
A: Type
IsTrunc0: Contr A
IsTrunc n'.+1 A apply @istrunc_succ, (IH (-2)); auto.
  - (* S m', S n' *)
n': trunc_index
IH: forall m : trunc_index,
m <= n' ->
forall A : Type, IsTrunc m A -> IsTrunc n' A
m': trunc_index
Hmn: m'.+1 <= n'.+1
A: Type
IsTrunc0: IsTrunc m'.+1 A
IsTrunc n'.+1 A
    apply istrunc_S.
n': trunc_index
IH: forall m : trunc_index,
m <= n' ->
forall A : Type, IsTrunc m A -> IsTrunc n' A
m': trunc_index
Hmn: m'.+1 <= n'.+1
A: Type
IsTrunc0: IsTrunc m'.+1 A
forall x y : A, IsTrunc n' (x = y)
    intros x y; apply (IH m'); auto with typeclass_instances.
Defined.

(** In particular, a contractible type, hprop, or hset is truncated at all higher levels.  We don't allow these to be used as idmaps, since there would be no point to it. *)

Definition istrunc_contr {n} {A} `{Contr A} : IsTrunc n.+1 A
  := (@istrunc_leq (-2) n.+1 tt _ _).

Definition istrunc_hprop {n} {A} `{IsHProp A} : IsTrunc n.+2 A
  := (@istrunc_leq (-1) n.+2 tt _ _).

Definition istrunc_hset {n} {A} `{IsHSet A}
  : IsTrunc n.+3 A
  := (@istrunc_leq 0 n.+3 tt _ _).

(** Consider the preceding definitions as instances for typeclass search, but only if the requisite hypothesis is already a known assumption; otherwise they result in long or interminable searches. *)
#[export] Hint Immediate istrunc_contr : typeclass_instances.
#[export] Hint Immediate istrunc_hprop : typeclass_instances.
#[export] Hint Immediate istrunc_hset : typeclass_instances.

(** Equivalence preserves truncation (this is, of course, trivial with univalence).  This is not an [Instance] because it causes infinite loops. *)
Definition istrunc_isequiv_istrunc A {B} (f : A -> B)
  `{IsTrunc n A} `{IsEquiv A B f}
  : IsTrunc n B.
A, B: Type
f: A -> B
n: trunc_index
IsTrunc0: IsTrunc n A
H: IsEquiv f
IsTrunc n B
Proof.
A, B: Type
f: A -> B
n: trunc_index
IsTrunc0: IsTrunc n A
H: IsEquiv f
IsTrunc n B
  generalize dependent B; generalize dependent A.
n: trunc_index
forall A : Type,
IsTrunc n A ->
forall (B : Type) (f : A -> B),
IsEquiv f -> IsTrunc n B
  simple_induction n n IH; simpl; intros A ? B f ?.
A: Type
IsTrunc0: Contr A
B: Type
f: A -> B
H: IsEquiv f
Contr B
n: trunc_index
IH: forall A : Type,
IsTrunc n A ->
forall (B : Type) (f : A -> B),
IsEquiv f -> IsTrunc n B
A: Type
IsTrunc0: IsTrunc n.+1 A
B: Type
f: A -> B
H: IsEquiv f
IsTrunc n.+1 B
  -
A: Type
IsTrunc0: Contr A
B: Type
f: A -> B
H: IsEquiv f
Contr B exact (contr_equiv _ f).
  -
n: trunc_index
IH: forall A : Type,
IsTrunc n A ->
forall (B : Type) (f : A -> B),
IsEquiv f -> IsTrunc n B
A: Type
IsTrunc0: IsTrunc n.+1 A
B: Type
f: A -> B
H: IsEquiv f
IsTrunc n.+1 B apply istrunc_S.
n: trunc_index
IH: forall A : Type,
IsTrunc n A ->
forall (B : Type) (f : A -> B),
IsEquiv f -> IsTrunc n B
A: Type
IsTrunc0: IsTrunc n.+1 A
B: Type
f: A -> B
H: IsEquiv f
forall x y : B, IsTrunc n (x = y)
    intros x y.
n: trunc_index
IH: forall A : Type,
IsTrunc n A ->
forall (B : Type) (f : A -> B),
IsEquiv f -> IsTrunc n B
A: Type
IsTrunc0: IsTrunc n.+1 A
B: Type
f: A -> B
H: IsEquiv f
x, y: B
IsTrunc n (x = y)
    exact (IH _ _ _ (ap (f^-1))^-1 _).
Defined.

Definition istrunc_equiv_istrunc A {B} (f : A <~> B) `{IsTrunc n A}
  : IsTrunc n B
  := istrunc_isequiv_istrunc A f.

(** ** Truncated morphisms *)

Class IsTruncMap (n : trunc_index) {X Y : Type} (f : X -> Y)
  := istruncmap_fiber :: forall y:Y, IsTrunc n (hfiber f y).

Notation IsEmbedding := (IsTruncMap (-1)).

(** ** Universes of truncated types *)

(** It is convenient for some purposes to consider the universe of all n-truncated types (within a given universe of types).  In particular, this allows us to state the important fact that each such universe is itself (n+1)-truncated. *)

Record TruncType (n : trunc_index) := {
  trunctype_type : Type ;
  trunctype_istrunc :: IsTrunc n trunctype_type
}.

Arguments Build_TruncType _ _ {_}.
Arguments trunctype_type {_} _.
Arguments trunctype_istrunc [_] _.

Coercion trunctype_type : TruncType >-> Sortclass.

Notation "n -Type" := (TruncType n) : type_scope.
Notation HProp := (-1)-Type.
Notation HSet := 0-Type.

Notation Build_HProp := (Build_TruncType (-1)).
Notation Build_HSet := (Build_TruncType 0).

(** This is (as of October 2014) the only [Canonical Structure] in the library.  It would be nice to do without it, in the interests of minimizing the number of fancy Coq features that the reader needs to know about. *)
Canonical Structure default_TruncType := fun n T P => (@Build_TruncType n T P).

(** Version of [smalltype] for n-Types. *)
Definition smallntype@{i j} (n : trunc_index) (P : TruncType@{j} n) {smallP : IsSmall@{i j} P}
  : TruncType@{i} n.
n: trunc_index
P: n -Type
smallP: IsSmall P
n -Type
Proof.
n: trunc_index
P: n -Type
smallP: IsSmall P
n -Type
  napply (Build_TruncType n (smalltype P)).
n: trunc_index
P: n -Type
smallP: IsSmall P
IsTrunc n (smalltype P)
  apply (@istrunc_equiv_istrunc _ _ (equiv_smalltype P)^-1 n _).
Defined.

Notation smallhprop := (smallntype (-1)).

(** ** Facts about hprops *)

(** An inhabited proposition is contractible.  This is not an [Instance] because it causes infinite loops. *)
Lemma contr_inhabited_hprop (A : Type) `{H : IsHProp A} (x : A)
  : Contr A.
A: Type
H: IsHProp A
x: A
Contr A
Proof.
A: Type
H: IsHProp A
x: A
Contr A
  apply (Build_Contr _ x).
A: Type
H: IsHProp A
x: A
forall y : A, x = y
  intro y.
A: Type
H: IsHProp A
x, y: A
x = y
  rapply center.
Defined.

(** If inhabitation implies contractibility, then we have an h-proposition.  We probably won't often have a hypothesis of the form [A -> Contr A], so we make sure we give priority to other instances. *)
Instance hprop_inhabited_contr (A : Type)
  : (A -> Contr A) -> IsHProp A | 10000.
A: Type
(A -> Contr A) -> IsHProp A
Proof.
A: Type
(A -> Contr A) -> IsHProp A
  intros H; apply istrunc_S; intros x y.
A: Type
H: A -> Contr A
x, y: A
Contr (x = y)
  pose (C := H x).
A: Type
H: A -> Contr A
x, y: A
C:= H x: Contr A
Contr (x = y)
  apply contr_paths_contr.
Defined.

(** Any two points in an hprop are connected by a path. *)
Theorem path_ishprop `{H : IsHProp A}
  : forall x y : A, x = y.
A: Type
H: IsHProp A
forall x y : A, x = y
Proof.
A: Type
H: IsHProp A
forall x y : A, x = y
  intros x y.
A: Type
H: IsHProp A
x, y: A
x = y
  rapply center.
Defined.

(** Conversely, this property characterizes hprops. *)
Theorem hprop_allpath (A : Type)
  : (forall (x y : A), x = y) -> IsHProp A.
A: Type
(forall x y : A, x = y) -> IsHProp A
Proof.
A: Type
(forall x y : A, x = y) -> IsHProp A
  intros H; apply istrunc_S; intros x y.
A: Type
H: forall x y : A, x = y
x, y: A
Contr (x = y)
  napply contr_paths_contr.
A: Type
H: forall x y : A, x = y
x, y: A
Contr A
  exact (Build_Contr _ x (H x)).
Defined.

(** Two propositions are equivalent as soon as there are maps in both directions. *)
Definition isequiv_iff_hprop `{IsHProp A} `{IsHProp B}
  (f : A -> B) (g : B -> A)
  : IsEquiv f.
A: Type
IsHProp0: IsHProp A
B: Type
IsHProp1: IsHProp B
f: A -> B
g: B -> A
IsEquiv f
Proof.
A: Type
IsHProp0: IsHProp A
B: Type
IsHProp1: IsHProp B
f: A -> B
g: B -> A
IsEquiv f
  apply (isequiv_adjointify f g);
    intros ?; apply path_ishprop.
Defined.

Definition equiv_iff_hprop_uncurried `{IsHProp A} `{IsHProp B}
  : (A <-> B) -> (A <~> B).
A: Type
IsHProp0: IsHProp A
B: Type
IsHProp1: IsHProp B
A <-> B -> A <~> B
Proof.
A: Type
IsHProp0: IsHProp A
B: Type
IsHProp1: IsHProp B
A <-> B -> A <~> B
  intro fg.
A: Type
IsHProp0: IsHProp A
B: Type
IsHProp1: IsHProp B
fg: A <-> B
A <~> B
  apply (equiv_adjointify (fst fg) (snd fg));
    intros ?; apply path_ishprop.
Defined.

Definition equiv_iff_hprop `{IsHProp A} `{IsHProp B}
  : (A -> B) -> (B -> A) -> (A <~> B)
  := fun f g => equiv_iff_hprop_uncurried (f, g).

Corollary iff_contr_hprop (A : Type) `{IsHProp A}
  : Contr A <-> A.
A: Type
IsHProp0: IsHProp A
Contr A <-> A
Proof.
A: Type
IsHProp0: IsHProp A
Contr A <-> A
  split.
A: Type
IsHProp0: IsHProp A
Contr A -> A
A: Type
IsHProp0: IsHProp A
A -> Contr A
  -
A: Type
IsHProp0: IsHProp A
Contr A -> A apply center.
  -
A: Type
IsHProp0: IsHProp A
A -> Contr A rapply contr_inhabited_hprop.
Defined.

(** ** Truncatedness: any dependent product of n-types is an n-type *)

Definition contr_forall `{Funext} `{P : A -> Type} `{forall a, Contr (P a)}
  : Contr (forall a, P a).
H: Funext
A: Type
P: A -> Type
H0: forall a : A, Contr (P a)
Contr (forall a : A, P a)
Proof.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, Contr (P a)
Contr (forall a : A, P a)
  apply (Build_Contr _ (fun a => center (P a))).
H: Funext
A: Type
P: A -> Type
H0: forall a : A, Contr (P a)
forall y : forall a : A, P a,
(fun a : A => center (P a)) = y
  intro f.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, Contr (P a)
f: forall a : A, P a
(fun a : A => center (P a)) = f  apply path_forall.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, Contr (P a)
f: forall a : A, P a
(fun a : A => center (P a)) == f  intro a.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, Contr (P a)
f: forall a : A, P a
a: A
center (P a) = f a  apply contr.
Defined.

Instance istrunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)}
  : IsTrunc n (forall a, P a) | 100.
H: Funext
A: Type
P: A -> Type
n: trunc_index
H0: forall a : A, IsTrunc n (P a)
IsTrunc n (forall a : A, P a)
Proof.
H: Funext
A: Type
P: A -> Type
n: trunc_index
H0: forall a : A, IsTrunc n (P a)
IsTrunc n (forall a : A, P a)
  generalize dependent P.
H: Funext
A: Type
n: trunc_index
forall P : A -> Type,
(forall a : A, IsTrunc n (P a)) ->
IsTrunc n (forall a : A, P a)
  simple_induction n n IH; simpl; intros P ?.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, Contr (P a)
Contr (forall a : A, P a)
H: Funext
A: Type
n: trunc_index
IH: forall P : A -> Type,
(forall a : A, IsTrunc n (P a)) ->
IsTrunc n (forall a : A, P a)
P: A -> Type
H0: forall a : A, IsTrunc n.+1 (P a)
IsTrunc n.+1 (forall a : A, P a)
  (* case [n = -2], i.e. contractibility *)
  -
H: Funext
A: Type
P: A -> Type
H0: forall a : A, Contr (P a)
Contr (forall a : A, P a) exact contr_forall.
  (* case n = n'.+1 *)
  -
H: Funext
A: Type
n: trunc_index
IH: forall P : A -> Type,
(forall a : A, IsTrunc n (P a)) ->
IsTrunc n (forall a : A, P a)
P: A -> Type
H0: forall a : A, IsTrunc n.+1 (P a)
IsTrunc n.+1 (forall a : A, P a) apply istrunc_S.
H: Funext
A: Type
n: trunc_index
IH: forall P : A -> Type,
(forall a : A, IsTrunc n (P a)) ->
IsTrunc n (forall a : A, P a)
P: A -> Type
H0: forall a : A, IsTrunc n.+1 (P a)
forall x y : forall a : A, P a, IsTrunc n (x = y)
    intros f g; exact (istrunc_isequiv_istrunc@{u1 u1} _ (apD10@{_ _ u1} ^-1)).
Defined.

(** Truncatedness is an hprop. *)
Instance ishprop_istrunc `{Funext} (n : trunc_index) (A : Type)
  : IsHProp (IsTrunc n A) | 0.
H: Funext
n: trunc_index
A: Type
IsHProp (IsTrunc n A)
Proof.
H: Funext
n: trunc_index
A: Type
IsHProp (IsTrunc n A)
  revert A; simple_induction n n IH; cbn; intro A.
H: Funext
A: Type
IsHProp (Contr A)
H: Funext
n: trunc_index
IH: forall A : Type, IsHProp (IsTrunc n A)
A: Type
IsHProp (IsTrunc n.+1 A)
  -
H: Funext
A: Type
IsHProp (Contr A) napply (istrunc_equiv_istrunc _ (equiv_istrunc_unfold (-2) A)^-1%equiv).
H: Funext
A: Type
IsHProp (IsTrunc_unfolded (-2) A)
    apply hprop_allpath.
H: Funext
A: Type
forall x y : IsTrunc_unfolded (-2) A, x = y
    intros [a1 c1] [a2 c2].
H: Funext
A: Type
a1: A
c1: forall y : A, a1 = y
a2: A
c2: forall y : A, a2 = y
(a1; c1) = (a2; c2)
    destruct (c1 a2).
H: Funext
A: Type
a1: A
c1, c2: forall y : A, a1 = y
(a1; c1) = (a1; c2)
    apply (ap (exist _ a1)).
H: Funext
A: Type
a1: A
c1, c2: forall y : A, a1 = y
c1 = c2
    funext x.
H: Funext
A: Type
a1: A
c1, c2: forall y : A, a1 = y
x: A
c1 x = c2 x
    pose (Build_Contr _ a1 c1); apply path2_contr.
  -
H: Funext
n: trunc_index
IH: forall A : Type, IsHProp (IsTrunc n A)
A: Type
IsHProp (IsTrunc n.+1 A) exact (istrunc_equiv_istrunc _ (equiv_istrunc_unfold n.+1 A)^-1%equiv).
    (* This case follows from [istrunc_forall]. *)
Defined.

(** By [trunc_hprop], it follows that [IsTrunc n A] is also [m]-truncated for any [m >= -1]. *)

(** Similarly, a map being truncated is also a proposition. *)
Instance ishprop_istruncmap `{Funext} (n : trunc_index) {X Y : Type} (f : X -> Y)
: IsHProp (IsTruncMap n f).
H: Funext
n: trunc_index
X, Y: Type
f: X -> Y
IsHProp (IsTruncMap n f)
Proof.
H: Funext
n: trunc_index
X, Y: Type
f: X -> Y
IsHProp (IsTruncMap n f)
  apply hprop_allpath; intros s t.
H: Funext
n: trunc_index
X, Y: Type
f: X -> Y
s, t: IsTruncMap n f
s = t
  apply path_forall; intros x.
H: Funext
n: trunc_index
X, Y: Type
f: X -> Y
s, t: IsTruncMap n f
x: Y
s x = t x
  apply path_ishprop.
Defined.

(** If a type [A] is [n]-truncated, then [IsTrunc n A] is contractible. *)
Instance contr_istrunc `{Funext} (n : trunc_index) (A : Type) `{istruncA : IsTrunc n A}
  : Contr (IsTrunc n A) | 100
  := contr_inhabited_hprop _ _.

Corollary equiv_contr_hprop (A : Type) `{Funext} `{IsHProp A}
  : Contr A <~> A.
A: Type
H: Funext
IsHProp0: IsHProp A
Contr A <~> A
Proof.
A: Type
H: Funext
IsHProp0: IsHProp A
Contr A <~> A
  exact (equiv_iff_hprop_uncurried (iff_contr_hprop A)).
Defined.

(** If a type [A] implies that it is [n.+1]-truncated, then it is [n.+1]-truncated. **)
Definition istrunc_inhabited_istrunc {n : trunc_index}
  {A : Type} (H : A -> IsTrunc n.+1 A)
  : IsTrunc n.+1 A
  := istrunc_S _ (fun a b => H a a b).

(** If you are looking for a theorem about truncation, you may want to read the note "Finding Theorems" in "STYLE.md". *)