(** * Homotopy PreCategory of Types *)
Require Import Category.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HoTT.Basics HoTT.Truncations.Core.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Local Open Scope path_scope.

Local Open Scope category_scope.

(** Quoting the HoTT Book:

    Example. There is a precategory whose type of objects is [U] and
    with [hom(X,Y) : ∥X → Y∥₀], and composition defined by induction
    on truncation from ordinary composition [(Y → Z) → (X → Y) → (X →
    Z)]. We call this the homotopy precategory of types. *)

(** We don't want access to all of the internals of this category at top level. *)
Module HomotopyPreCategoryInternals.
  Section homotopy_precategory.
    Local Notation object := Type (only parsing).
    Local Notation morphism s d := (Trunc 0 (s -> d)) (only parsing).

    Definition compose s d d' (m : morphism d d') (m' : morphism s d)
    : morphism s d'.
s, d, d': Type
m: Trunc 0 (d -> d')
m': Trunc 0 (s -> d)
Trunc 0 (s -> d')
    Proof.
s, d, d': Type
m: Trunc 0 (d -> d')
m': Trunc 0 (s -> d)
Trunc 0 (s -> d')
      revert m'; apply Trunc_rec; intro m'.
s, d, d': Type
m: Trunc 0 (d -> d')
m': s -> d
Trunc 0 (s -> d')
      revert m; apply Trunc_rec; intro m.
s, d, d': Type
m': s -> d
m: d -> d'
Trunc 0 (s -> d')
      apply tr.
s, d, d': Type
m': s -> d
m: d -> d'
s -> d'
      exact (m o m')%core.
    Defined.

    Definition identity x : morphism x x
      := tr idmap.

    Global Arguments compose [s d d'] m m' / .
    Global Arguments identity x / .
  End homotopy_precategory.
End HomotopyPreCategoryInternals.

(** ** The Homotopy PreCategory of Types *)
Definition homotopy_precategory : PreCategory.
PreCategory
Proof.
PreCategory
  refine (@Build_PreCategory
            Type
            _
            (@HomotopyPreCategoryInternals.identity)
            (@HomotopyPreCategoryInternals.compose)
            _
            _
            _
            _);
  simpl; intros;
  repeat match goal with
           | [ m : Trunc _ _ |- _ ]
             => revert m;
               apply Trunc_ind;
               [ intro;
                 match goal with
                   | [ |- IsHSet (?a = ?b :> ?T) ]
                     => generalize a b; intros;
                        let H := fresh in
                        assert (H : forall x y : T, IsHProp (x = y))
                 end;
                 typeclasses eauto
               | intro ]
         end;
  simpl;
  apply ap;
  exact idpath.
Defined.