Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Diagrams.Sequence.
Require Import Homotopy.Join.Core.
Require Import Colimits.Colimit Colimits.Sequential.

Local Open Scope nat_scope.

(** * Propositonal truncation as a colimit. *)

(** In this file we give an alternative construction of the propositional truncation using colimits. This can serve as a metatheoretic justification that propositional truncations exist. *)

(** The sequence of increasing joins. *)
Definition Join_seq (A : Type) : Sequence.
A: Type
Sequence
Proof.
A: Type
Sequence
  srapply Build_Sequence.
A: Type
nat -> Type
A: Type
forall n : nat, ?X n -> ?X n.+1
  1: exact (iterated_join A).
A: Type
forall n : nat,
iterated_join A n -> iterated_join A n.+1
  intros n.
A: Type
n: nat
iterated_join A n -> iterated_join A n.+1
  exact joinr.
Defined.

(** Propositional truncation can be defined as the colimit of this sequence. *)
Definition PropTrunc A : Type := Colimit (Join_seq A).

(** The constructor is given by the colimit constructor. *)
Definition ptr_in {A} : A -> PropTrunc A := colim (D:=Join_seq A) 0.

(** The sequential colimit of this sequence is the propositional truncation. *)

(** Universal property of propositional truncation. *)
Lemma equiv_PropTrunc_rec `{Funext} (A P : Type) `{IsHProp P}
  : (PropTrunc A -> P) <~> (A -> P).
H: Funext
A, P: Type
IsHProp0: IsHProp P
(PropTrunc A -> P) <~> (A -> P)
Proof.
H: Funext
A, P: Type
IsHProp0: IsHProp P
(PropTrunc A -> P) <~> (A -> P)
  refine (_ oE equiv_colim_seq_rec _ P).
H: Funext
A, P: Type
IsHProp0: IsHProp P
(forall n : Graph.graph0 sequence_graph,
 Diagram.obj (Join_seq A) n -> P) <~> 
(A -> P)
  srapply equiv_iff_hprop.
H: Funext
A, P: Type
IsHProp0: IsHProp P
(forall n : Graph.graph0 sequence_graph,
 Diagram.obj (Join_seq A) n -> P) -> 
A -> P
H: Funext
A, P: Type
IsHProp0: IsHProp P
(A -> P) ->
forall n : Graph.graph0 sequence_graph,
Diagram.obj (Join_seq A) n -> P
  {
H: Funext
A, P: Type
IsHProp0: IsHProp P
(forall n : Graph.graph0 sequence_graph,
 Diagram.obj (Join_seq A) n -> P) -> 
A -> P intros h.
H: Funext
A, P: Type
IsHProp0: IsHProp P
h: forall n : Graph.graph0 sequence_graph,
Diagram.obj (Join_seq A) n -> P
A -> P
    exact (h 0). }
H: Funext
A, P: Type
IsHProp0: IsHProp P
(A -> P) ->
forall n : Graph.graph0 sequence_graph,
Diagram.obj (Join_seq A) n -> P
  intros f.
H: Funext
A, P: Type
IsHProp0: IsHProp P
f: A -> P
forall n : Graph.graph0 sequence_graph,
Diagram.obj (Join_seq A) n -> P
  induction n.
H: Funext
A, P: Type
IsHProp0: IsHProp P
f: A -> P
Diagram.obj (Join_seq A) 0 -> P
H: Funext
A, P: Type
IsHProp0: IsHProp P
f: A -> P
n: nat
IHn: Diagram.obj (Join_seq A) n -> P
Diagram.obj (Join_seq A) n.+1 -> P
  -
H: Funext
A, P: Type
IsHProp0: IsHProp P
f: A -> P
Diagram.obj (Join_seq A) 0 -> P exact f.
  -
H: Funext
A, P: Type
IsHProp0: IsHProp P
f: A -> P
n: nat
IHn: Diagram.obj (Join_seq A) n -> P
Diagram.obj (Join_seq A) n.+1 -> P cbn.
H: Funext
A, P: Type
IsHProp0: IsHProp P
f: A -> P
n: nat
IHn: Diagram.obj (Join_seq A) n -> P
Join A
  ((fix F (m : nat) : Type :=
      match m with
      | 0 => A
      | m'.+1 => Join A (F m')
      end) n) -> P
    srapply Join_rec.
H: Funext
A, P: Type
IsHProp0: IsHProp P
f: A -> P
n: nat
IHn: Diagram.obj (Join_seq A) n -> P
A -> P
H: Funext
A, P: Type
IsHProp0: IsHProp P
f: A -> P
n: nat
IHn: Diagram.obj (Join_seq A) n -> P
(fix F (m : nat) : Type :=
   match m with
   | 0 => A
   | m'.+1 => Join A (F m')
   end) n -> P
H: Funext
A, P: Type
IsHProp0: IsHProp P
f: A -> P
n: nat
IHn: Diagram.obj (Join_seq A) n -> P
forall (a : A)
(b : (fix F (m : nat) : Type :=
        match m with
        | 0 => A
        | m'.+1 => Join A (F m')
        end) n), ?P_A a = ?P_B b
    1,2: assumption.
H: Funext
A, P: Type
IsHProp0: IsHProp P
f: A -> P
n: nat
IHn: Diagram.obj (Join_seq A) n -> P
forall (a : A)
(b : (fix F (m : nat) : Type :=
        match m with
        | 0 => A
        | m'.+1 => Join A (F m')
        end) n), f a = IHn b
    intros a b.
H: Funext
A, P: Type
IsHProp0: IsHProp P
f: A -> P
n: nat
IHn: Diagram.obj (Join_seq A) n -> P
a: A
b: (fix F (m : nat) : Type :=
   match m with
   | 0 => A
   | m'.+1 => Join A (F m')
   end) n
f a = IHn b
    rapply path_ishprop.
Defined.

(** The propositional truncation is a hprop. *)
Global Instance ishprop_proptrunc `{Funext} (A : Type)
  : IsHProp (PropTrunc A).
H: Funext
A: Type
IsHProp (PropTrunc A)
Proof.
H: Funext
A: Type
IsHProp (PropTrunc A)
  rapply hprop_inhabited_contr.
H: Funext
A: Type
PropTrunc A -> Contr (PropTrunc A)
  rapply (equiv_PropTrunc_rec _ _)^-1.
H: Funext
A: Type
A -> Contr (PropTrunc A)
  intros x.
H: Funext
A: Type
x: A
Contr (PropTrunc A)
  srapply contr_colim_seq_into_prop.
H: Funext
A: Type
x: A
forall n : Graph.graph0 sequence_graph,
Diagram.obj (Join_seq A) n
H: Funext
A: Type
x: A
forall n : nat,
const (?a n.+1) == Diagram.arr (Join_seq A) 1
  -
H: Funext
A: Type
x: A
forall n : Graph.graph0 sequence_graph,
Diagram.obj (Join_seq A) n intros n.
H: Funext
A: Type
x: A
n: Graph.graph0 sequence_graph
Diagram.obj (Join_seq A) n
    destruct n.
H: Funext
A: Type
x: A
Diagram.obj (Join_seq A) 0
H: Funext
A: Type
x: A
n: nat
Diagram.obj (Join_seq A) n.+1
    1: exact x.
H: Funext
A: Type
x: A
n: nat
Diagram.obj (Join_seq A) n.+1
    exact (joinl x).
  -
H: Funext
A: Type
x: A
forall n : nat,
const
  ((fun n0 : Graph.graph0 sequence_graph =>
    match
      n0 as n1 return (Diagram.obj (Join_seq A) n1)
    with
    | 0 => x
    | n1.+1 => (fun n2 : nat => joinl x) n1
    end) n.+1) == Diagram.arr (Join_seq A) 1 intros n.
H: Funext
A: Type
x: A
n: nat
const
  ((fun n : Graph.graph0 sequence_graph =>
    match
      n as n0 return (Diagram.obj (Join_seq A) n0)
    with
    | 0 => x
    | n0.+1 => (fun n1 : nat => joinl x) n0
    end) n.+1) == Diagram.arr (Join_seq A) 1
    rapply jglue.
Defined.