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: *** *)