(** * The category ω of (ℕ, ≤), and the chain categories [[n]] *)
Require Import Category.Subcategory.Full.
Require Import Category.Sigma.Univalent.
Require Import Category.Morphisms Category.Univalent Category.Strict.
Require Import HoTT.Basics HoTT.Types HoTT.Spaces.Nat.Core.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope nat_scope.

(** ** Definitions *)
(** Quoting Wikipedia (http://en.wikipedia.org/wiki/Total_order##Chains):

    While chain is sometimes merely a synonym for totally ordered set,
    it can also refer to a totally ordered subset of some partially
    ordered set. The latter definition has a crucial role in Zorn's
    lemma. *)
(** We take the convention that a "chain" is a totally ordered or
    linearly ordered set; the corresponding category on that set has,
    as morphisms, the order relation. *)
(* N.B. The notation here (including that [[n]] have as objects the
   set [{0, 1, ..., n}]) was originally suggested by David Spivak.
   It's possible that we should pick a different or more common
   terminology. *)

Module Export Core.
  (** *** [[ω]], the linear order on ℕ *)
  Definition omega : PreCategory
    := @Build_PreCategory
         nat
         leq
         leq_refl
         (fun x y z p q => leq_trans q p)
         (fun _ _ _ _ _ _ _ => path_ishprop _ _)
         (fun _ _ _ => path_ishprop _ _)
         (fun _ _ _ => path_ishprop _ _)
         _.

  (** *** [[n]], a linear order on a finite set with [n + 1] elements *)
  (** Using [n + 1] elements allows us to agree with the common
      definition of an [n]-simplex, where a 0-simplex is a point, and
      a 1-simplex has two end-points, etc. *)
  Definition chain (n : nat) : PreCategory
    := { m : omega | m <= n }%category.

  (** TODO: Possibly generalize this to arbitrary sets with arbitrary
      (total?) orders on them? *)

  Module Export ChainCategoryCoreNotations.
    Notation "[ n ]" := (chain n) : category_scope.
  End ChainCategoryCoreNotations.
End Core.

Module Export Notations.
  Include ChainCategoryCoreNotations.
End Notations.

Module Utf8.
  Export Notations.

  Notation "[ ∞ ]" := omega : category_scope.
  Notation "[ 'ω' ]" := omega : category_scope.
End Utf8.
Module Export Strict.
  Definition isstrict_omega : IsStrictCategory omega.
IsStrictCategory omega
  Proof.
IsStrictCategory omega
    exact _.
  Defined.

  Definition isstrict_chain {n} : IsStrictCategory [n].
n: nat
IsStrictCategory [n]
  Proof.
n: nat
IsStrictCategory [n]
    exact _.
  Defined.
End Strict.

Module Export Univalent.
  Instance iscategory_omega : IsCategory omega.
IsCategory omega
  Proof.
IsCategory omega
    intros s d.
s, d: omega
IsEquiv (idtoiso omega (y:=d))
    refine (isequiv_iff_hprop _ _).
s, d: omega
IsHProp (s <~=~> d)%category
s, d: omega
(s <~=~> d)%category -> s = d
    {
s, d: omega
IsHProp (s <~=~> d)%category exact (istrunc_equiv_istrunc _ (issig_isomorphic _ _ _)). }
s, d: omega
(s <~=~> d)%category -> s = d
    {
s, d: omega
(s <~=~> d)%category -> s = d intro m; apply leq_antisym; apply m. }
  Defined.

  Definition iscategory_chain {n} : IsCategory [n].
n: nat
IsCategory [n]
  Proof.
n: nat
IsCategory [n]
    exact _.
  Defined.
End Univalent.