Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Simplex Category
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;
|}.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.