Add Rec LoadPath "Foundations/Generalities".
Add Rec LoadPath "Foundations/hlevel1".
Add Rec LoadPath "Foundations/hlevel2".

Require Export "Foundations/hlevel2/finitesets" .


Variable Delta : forall (i j : nat) , Type . (* This should be defined as the type of order
preserving injections from {0,...i} to {0,...,j}. I introduced these axiomatically to save the
time. *)

Variable gamma : forall ( i j k : nat ) ( s1 : Delta i j ) (s2 : Delta j k ) , Delta i k . (*
This should be defined as compositions of injections. *)

Variable rl : forall ( j k : nat )( s : Delta j k )( a : stn (j+1) ) , stn (k + 1) . (* This
should be defined as the obvious function from order preserving injections to all funcions. *)

Definition Intrec1 ( n : nat ) := total2 ( fun

SS : Type => total2 ( fun

mapsfromsks : forall ( X : SS ) ( i : nat ) ( c : natleh i n )  (j : nat ) , Type  =>

(* restr : *) forall ( X : SS )  ( i : nat ) ( c : natleh i n )  (j : nat ) ( k : nat ) ( f :
mapsfromsks X i c k ) ( s : Delta j k ) , mapsfromsks X i c j )) .

Definition SS ( n : nat ) ( XX : Intrec1 n ) := pr1 XX .

Definition mapsfromsks ( n : nat ) ( XX : Intrec1 n ) := pr1 (pr2 XX ) .

Definition restr ( n : nat ) ( XX : Intrec1 n ) := pr2 (pr2 XX ) .

Lemma mapsfromsksSn ( n : nat ) ( IHn : Intrec1 n ) : forall ( X : total2 ( fun X0 : SS n IHn =>
forall f : mapsfromsks n IHn X0 n (isreflnatleh n) ( S n ) , UU ) ) ( i : nat ) ( c : natleh i (
S n ) ) ( j : nat ) , Type .
Proof.  intros . set ( SSn := SS n IHn ) . set (mapsfromsksn := mapsfromsks n IHn ) . set
(restrn := restr n IHn ) . set ( SSSn := total2 ( fun Xn : SSn => forall f : mapsfromsksn Xn n
(isreflnatleh n) ( S n ) , UU ) ) .

set ( cc := natlehchoice2 _ _ c ) . destruct cc .
simpl in h . change (pr1 (natleh i n ) ) in h . exact ( mapsfromsksn ( pr1 X ) i h j ) .
exact ( total2 ( fun f : mapsfromsksn ( pr1 X ) n ( isreflnatleh n ) j => forall s : Delta ( S n
) j , (pr2 X) (restrn (pr1 X) n (isreflnatleh n) ( S n ) j f s ) ) ). Defined.

Definition SEMISIMPL ( n : nat ) : Intrec1 n .
Proof . induction n .

(* n=0 *)  unfold Intrec1. split with UU . split with (fun X => fun i => fun c => fun j => ( stn
(j+1) -> X )) .  exact ( fun X => fun i => fun c => fun j => fun k => fun f => fun phi => fun a
=> f (rl j k phi a ) ).

(* n => Sn *) set ( SSn := SS n IHn ) . set (mapsfromsksn := mapsfromsks n IHn ) . set (restrn
:= restr n IHn ) .

set ( SSSn := total2 ( fun Xn : SSn => forall f : mapsfromsksn Xn n (isreflnatleh n) ( S n ) ,
UU ) ) . split with SSSn .
split with (fun X => fun i => fun c => fun j => mapsfromsksSn n IHn X i c j ) .

intro. intro. intro. intro. intro.   unfold mapsfromsksSn . set ( cc := natlehchoice2 _ _ c ) .
destruct cc . apply restrn .

intros. destruct f as [fn ff]. simpl in restrn .  change (pr1 IHn) with SSn in restrn . change
(pr1 (pr2 IHn)) with mapsfromsksn in restrn.  split with (restrn (pr1 X) n (isreflnatleh n) j k
fn s ).

intros . set ( s1 := gamma ( S n ) j k s0 s ) . set ( ffint := ff s1 ) .

set ( fs1 := restrn (pr1 X) n (isreflnatleh n) (S n) k fn s1) . set (fs0s := restr n IHn (pr1 X)
n (isreflnatleh n) (S n) j (restrn (pr1 X) n (isreflnatleh n) j k fn s) s0).

simpl in fs1 . simpl in fs0s.

assert ( e : paths (restrn (pr1 X) n (isreflnatleh n) (S n) k fn s1) (restr n IHn (pr1 X) n
(isreflnatleh n) (S n) j (restrn (pr1 X) n (isreflnatleh n) j k fn s) s0) ).

(* At this point the remaining goal is to prove a certain equality. This equlity will hold
definitionally in TS (if I am not mistaken). *)

Check (restrn (pr1 X) n (isreflnatleh n) (S n) k fn s1).

Admitted.


Definition SEMISIMPL0 : Intrec1 0.
Proof . unfold Intrec1. split with UU . split with (fun X => fun i => fun c => fun j => ( stn
(j+1) -> X )) .  exact ( fun X => fun i => fun c => fun j => fun k => fun f => fun phi => fun a
=> f (rl j k phi a ) ). Defined.

Definition SEMISIMPL1 : Intrec1 1.
Proof.  set ( IHn := SEMISIMPL0 ) . set ( SSn := SS 0 IHn ) . set (mapsfromsksn := mapsfromsks 0
IHn ) . set (restrn := restr 0 IHn ) .

set ( SSSn := total2 ( fun Xn : SSn => forall f : mapsfromsksn Xn 0 (isreflnatleh 0) ( S 0 ) ,
UU ) ) . split with SSSn .
split with (fun X => fun i => fun c => fun j => mapsfromsksSn 0 IHn X i c j ) .

intro. intro. intro. intro. intro.   unfold mapsfromsksSn . set ( cc := natlehchoice2 _ _ c ) .
destruct cc . apply restrn .

intros. destruct f as [fn ff]. simpl in restrn .  change (pr1 IHn) with SSn in restrn . change
(pr1 (pr2 IHn)) with mapsfromsksn in restrn.  split with (restrn (pr1 X) 0 (isreflnatleh 0) j k
fn s ).

intros . set ( s1 := gamma ( S 0 ) j k s0 s ) . set ( ffint := ff s1 ) .

set ( fs1 := restrn (pr1 X) 0 (isreflnatleh 0) (S 0) k fn s1) . set (fs0s := restr 0 IHn (pr1 X)
0 (isreflnatleh 0) (S 0) j (restrn (pr1 X) 0 (isreflnatleh 0) j k fn s) s0).

simpl in fs1 . simpl in fs0s.

assert ( e : paths (restrn (pr1 X) 0 (isreflnatleh 0) (S 0) k fn s1) (restr 0 IHn (pr1 X) 0
(isreflnatleh 0) (S 0) j (restrn (pr1 X) 0 (isreflnatleh 0) j k fn s) s0) ).

simpl.  unfold IHn. unfold restrn. unfold restr. unfold IHn .   unfold SEMISIMPL0.  simpl .
apply funextfun . intro .  apply ( maponpaths fn ) .

Check (restrn (pr1 X) 0 (isreflnatleh 0) (S 0) k fn s1).








(* End of the file semisimplicial.v *)





(*
*** Local Variables: ***
*** coq-prog-name: "/opt/local/bin/coqtop" ***
*** coq-prog-args: ("-emacs-U") ***
*** End: ***
 *)