Simplex Category

simplex_category.v

Require Import Relation_Definitions.
Require Import SetoidClass.
Require Import VectorDef.
Require Import Morphisms.
Require Import COC.Base.Main.


Set Implicit Arguments.

Section Type_Aligned_Sequence.
  Variable (A : Type)
           (D : A -> A -> Type).

  Inductive taseq : A -> A -> Type :=
  | taseq_tail :
      forall {a : A}, taseq a a
  | taseq_cons :
      forall {a b c : A}, D a b -> taseq b c -> taseq a c.
  
  Notation "x ^*: xs" := (taseq_cons x xs) (at level 60, right associativity).
  
  Fixpoint taseq_concat {a b c : A}
           (f : taseq a b) (g : taseq b c) : taseq a c.
  Proof.
    induction f.
    exact g.
    exact (d ^*: (IHf g)).
  Defined.

  Fixpoint taseq_fold {a b : A} (T : A -> Type)
           (f : forall {a b : A}, D a b -> T a -> T b) 
           (init : T a) (seq : taseq a b) : T b.
  Proof.
    induction seq.
    exact init.
    exact (IHseq (f a b d init)).
  Defined.
End Type_Aligned_Sequence.

Definition s_index (n : nat) : Set := Fin.t (S n).

Inductive s_morph_prim : nat -> nat -> Set :=
| sm_face : forall (n : nat), s_index (S n) -> s_morph_prim n (S n)
| sm_degen : forall (n : nat), s_index n -> s_morph_prim (S n) n.

  
Fixpoint sm_face_component {m} (l : s_index (S m)) : s_index m -> s_index (S m) :=
  match l in Fin.t (S x) return Fin.t x -> Fin.t (S x) with
    | Fin.F1 =>
      fun k => Fin.FS k
    | Fin.FS l0 =>
      fun k =>
        match k in Fin.t y return Fin.t y -> Fin.t (S y) with
          | Fin.F1 => fun _ => Fin.F1
          | @Fin.FS (S n0) k0 => fun l00 => Fin.FS (@sm_face_component n0 l00 k0)
          | @Fin.FS 0 k0 => fun l00 => Fin.case0 (fun _ => Fin.t 2) k0
        end l0
  end.


Fixpoint sm_degen_component {m} (l : s_index m) (k : s_index (S m)) : s_index m :=
  match k in Fin.t (S x) return Fin.t x -> Fin.t x with
    | @Fin.F1 (S n) =>
      fun _ => Fin.F1
    | @Fin.F1 0 =>
      fun l0 => Fin.case0 (fun _ => Fin.t 0) l0
    | Fin.FS k0 =>
      fun l =>
        match l in Fin.t y return Fin.t y -> Fin.t y with
          | Fin.F1 => id (* k0 *)
          | @Fin.FS (S n0) l0 =>
            fun k00 => Fin.FS (@sm_degen_component n0 l0 k00)
          | @Fin.FS 0 l0 => fun _ => Fin.case0 (fun _ => Fin.t 1) l0                              
        end k0
  end l.

Definition s_morph_prim_component 
           {m n} (prim : s_morph_prim m n) (k : s_index m) : s_index n :=
  match prim in s_morph_prim m' n' return s_index m' -> s_index n' with
    | sm_face l => sm_face_component l
    | sm_degen l => sm_degen_component l
  end k.
  

Definition s_morph_carrier m n := taseq s_morph_prim m n.

Definition s_morph_component
           {m n} (morph : s_morph_carrier m n) (k : s_index m) : s_index n :=
  taseq_fold s_index (fun a b => @s_morph_prim_component a b) k morph.


Definition s_morph_equal {m n} (f g : s_morph_carrier m n) : Prop :=
  forall k : s_index m, s_morph_component f k = s_morph_component g k.

Theorem s_morph_equal_equiv : forall {m n}, Equivalence (@s_morph_equal m n).
Proof.
  intros.
  split.
  split.
  unfold Symmetric.
  unfold s_morph_equal.
  intros.
  rewrite (H k).
  reflexivity.
  unfold Transitive.
  unfold s_morph_equal.
  intros.
  rewrite (H k).
  rewrite (H0 k).
  reflexivity.
Qed.  

Definition simplex_morph (m n : nat) : Setoid :=
  {|
    setoid_carrier := s_morph_carrier m n;
    setoid_equal := s_morph_equal;
    setoid_prf := s_morph_equal_equiv;
  |}.

Definition s_morph_comp :
  forall (l m n : nat) (x : @simplex_morph l m) (y : @simplex_morph m n), @simplex_morph l n :=
  fun _ _ _ x y => taseq_concat x y.

Definition s_morph_id : forall (m : nat), @simplex_morph m m :=
  fun _ => taseq_tail s_morph_prim.


Theorem s_morph_comp_functor :
  forall (l m n : nat) (x : simplex_morph l m) (y : simplex_morph m n) (k : s_index l),
    s_morph_component (s_morph_comp x y) k =
    s_morph_component y (s_morph_component x k).
Proof.
  induction x.
  auto.
  intros.
  replace (s_morph_comp (taseq_cons d x) y) with (taseq_cons d (s_morph_comp x y)).
  assert (forall {l m n} (d : s_morph_prim l m) (f : s_morph_carrier m n) k, s_morph_component (taseq_cons d f) k = s_morph_component f (s_morph_prim_component d k)).
  intros.
  unfold s_morph_component.
  induction f.
  auto.
  simpl.
  reflexivity.
  rewrite H.
  rewrite H.
  rewrite IHx.
  reflexivity.
  induction x.
  auto.
  auto.
Qed.  
  
Theorem s_morph_comp_assoc :
  forall (k l m n : nat) (x : simplex_morph k l) (y : simplex_morph l m) (z : simplex_morph m n),
    s_morph_equal (s_morph_comp (s_morph_comp x y) z)
                        (s_morph_comp x (s_morph_comp y z)).
Proof.
  intros.
  unfold s_morph_equal.
  intros.
  rewrite s_morph_comp_functor.
  rewrite s_morph_comp_functor.
  rewrite s_morph_comp_functor.
  rewrite s_morph_comp_functor.
  reflexivity.
Qed.
  
Theorem s_morph_is_category : IsCategory s_morph_comp s_morph_id.
Proof.
  split.
  intros.
  
  simpl.
  unfold Proper, respectful.
  unfold s_morph_equal.
  intros.
  rewrite s_morph_comp_functor.
  rewrite s_morph_comp_functor.
  rewrite H.
  rewrite H0.
  reflexivity.

  intros.
  simpl.
  unfold s_morph_equal.
  intros.
  rewrite s_morph_comp_functor.
  rewrite s_morph_comp_functor.
  rewrite s_morph_comp_functor.
  rewrite s_morph_comp_functor.
  reflexivity.

  intros.
  simpl.
  unfold s_morph_equal.
  intros.
  reflexivity.

  intros.
  simpl.
  unfold s_morph_equal.
  intros.
  rewrite s_morph_comp_functor.
  unfold s_morph_component.
  simpl.
  reflexivity.
Qed.

Definition simplex_category : Category :=
  {|
    cat_obj := nat;
    cat_hom := simplex_morph;
    cat_comp := s_morph_comp;
    cat_id := s_morph_id;
    cat_prf := s_morph_is_category;
  |}.