Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Nat.Core.
Require Import Spaces.Int.
Require Import Spaces.Finite.Fin.
Require Import WildCat.Core.

Local Set Universe Minimization ToSet.

(** * Successor Structures. *)

(** A successor structure is just a type with a endofunctor on it, called 'successor'. Typical examples include either the integers or natural numbers with the successor (or predecessor) operation. *)

Record SuccStr : Type := {
   ss_carrier :> Type ;
   ss_succ : ss_carrier -> ss_carrier ;
}.

Declare Scope succ_scope.

Local Open Scope nat_scope.
Local Open Scope type_scope.
Local Open Scope succ_scope.

Delimit Scope succ_scope with succ.
Arguments ss_succ {_} _.

Notation "x .+1" := (ss_succ x) : succ_scope.

(** Successor structure of naturals *)
Definition NatSucc : SuccStr := Build_SuccStr nat nat_succ.

(** Successor structure of integers *)
Definition BinIntSucc : SuccStr := Build_SuccStr Int int_succ.

Notation "'+N'" := NatSucc : succ_scope.
Notation "'+Z'" := BinIntSucc : succ_scope.

(** Stratified successor structures *)

(** If [N] has a successor structure, then so does the product [N * Fin n].  The successor operation increases the second factor, and if it wraps around, it also increases the first factor. *)

Definition StratifiedType (N : SuccStr) (n : nat) := N * Fin n.

Definition stratified_succ (N : SuccStr) (n : nat) (x : StratifiedType N n)
  : StratifiedType N n.
N: SuccStr
n: nat
x: StratifiedType N n
StratifiedType N n
Proof.
N: SuccStr
n: nat
x: StratifiedType N n
StratifiedType N n
  constructor.
N: SuccStr
n: nat
x: StratifiedType N n
N
N: SuccStr
n: nat
x: StratifiedType N n
Fin n
  +
N: SuccStr
n: nat
x: StratifiedType N n
N destruct n.
N: SuccStr
x: StratifiedType N 0
N
N: SuccStr
n: nat
x: StratifiedType N n.+1
N
    -
N: SuccStr
x: StratifiedType N 0
N exact (Empty_rec _ (snd x)).
    -
N: SuccStr
n: nat
x: StratifiedType N n.+1
N destruct (dec (snd x = inr tt)).
N: SuccStr
n: nat
x: StratifiedType N n.+1
p: snd x = inr tt
N
N: SuccStr
n: nat
x: StratifiedType N n.+1
n0: snd x <> inr tt
N
      *
N: SuccStr
n: nat
x: StratifiedType N n.+1
p: snd x = inr tt
N exact (ss_succ (fst x)).
      *
N: SuccStr
n: nat
x: StratifiedType N n.+1
n0: snd x <> inr tt
N exact (fst x).
  +
N: SuccStr
n: nat
x: StratifiedType N n
Fin n exact (fsucc_mod (snd x)).
Defined.

Definition Stratified (N : SuccStr) (n : nat) : SuccStr
  := Build_SuccStr (StratifiedType N n) (stratified_succ N n).

(** Addition in successor structures *)
Definition ss_add {N : SuccStr} (n : N) (k : nat) : N := nat_iter k ss_succ n.

Infix "+" := ss_add : succ_scope.

Definition ss_add_succ {N : SuccStr} (n : N) (k : nat)
  : n + k.+1 = n.+1 + k
  := nat_iter_succ_r k ss_succ n.

Definition ss_add_sum {N : SuccStr} (n : N) (k l : nat)
  : n + (k + l) = (n + l) + k
  := nat_iter_add k l ss_succ n.

(** Nat and Int segmented by triples *)
Notation "'N3'" := (Stratified (+N) 3) : succ_scope.
Notation "'Z3'" := (Stratified (+Z) 3) : succ_scope.

(** ** Category of successor structures *)

(** Inspired by the construction of the wildcat structure on [pType], we can give [SuccStr] a wildcat structure in a similar manner (all the way up). *)

Record ssFam (A : SuccStr) := {
  ss_fam :> A -> Type;
  dss_succ {x} : ss_fam x -> ss_fam (x.+1);
}.

Arguments ss_fam {_ _} _.
Arguments dss_succ {_ _ _}.

Record ssForall {A : SuccStr} (B : ssFam A) := {
  ss_fun :> forall x, B x;
  ss_fun_succ : forall x, ss_fun x.+1 = dss_succ (ss_fun x); 
}.

Arguments ss_fun {_ _} _ _.
Arguments ss_fun_succ {_ _} _ _.

Definition ssfam_const {A : SuccStr} (B : SuccStr) : ssFam A
  := Build_ssFam A (fun _ => B) (fun _ => ss_succ).

Definition ssfam_sshomotopy {A : SuccStr} {P : ssFam A} (f g : ssForall P)
  : ssFam A.
A: SuccStr
P: ssFam A
f, g: ssForall P
ssFam A
Proof.
A: SuccStr
P: ssFam A
f, g: ssForall P
ssFam A
  snapply Build_ssFam.
A: SuccStr
P: ssFam A
f, g: ssForall P
A -> Type
A: SuccStr
P: ssFam A
f, g: ssForall P
forall x : A, ?ss_fam x -> ?ss_fam x.+1
  1: exact (fun x => f x = g x).
A: SuccStr
P: ssFam A
f, g: ssForall P
forall x : A,
(fun x0 : A => f x0 = g x0) x ->
(fun x0 : A => f x0 = g x0) x.+1
  cbn; intros x p.
A: SuccStr
P: ssFam A
f, g: ssForall P
x: A
p: f x = g x
f x.+1 = g x.+1
  exact (ss_fun_succ f x @ ap dss_succ p @ (ss_fun_succ g x)^).
Defined.

Definition ssHomotopy {A : SuccStr} {P : ssFam A} (f g : ssForall P)
  := ssForall (ssfam_sshomotopy f g).

Instance isgraph_ss : IsGraph SuccStr.
IsGraph SuccStr
Proof.
IsGraph SuccStr
  snapply Build_IsGraph.
SuccStr -> SuccStr -> Type
  intros X Y.
X, Y: SuccStr
Type
  exact (@ssForall X (ssfam_const Y)).
Defined.

Instance isgraph_ssforall {A : SuccStr} (P : ssFam A)
  : IsGraph (ssForall P).
A: SuccStr
P: ssFam A
IsGraph (ssForall P)
Proof.
A: SuccStr
P: ssFam A
IsGraph (ssForall P)
  snapply Build_IsGraph.
A: SuccStr
P: ssFam A
ssForall P -> ssForall P -> Type
  exact ssHomotopy.
Defined.

Instance is2graph_ssforall {A : SuccStr} (P : ssFam A)
  : Is2Graph (ssForall P)
  := {}.

Instance is2graph_ss : Is2Graph SuccStr := {}.
Instance is3graph_ss : Is3Graph SuccStr := {}.

Ltac sselim_elim eq x :=
  match type of (eq x) with
  | ?lhs = _ =>
    generalize dependent (eq x);
    generalize dependent lhs
  | _ => fail "sselim: no lhs found"
  end.

Ltac sselim f :=
  let eq := fresh "eq" in
  destruct f as [f eq];
  cbn in *;
  match type of eq with
  | forall x : ?X, _ = _ =>
    multimatch goal with
    | x : X |- _ => sselim_elim eq x
    | f : ?Y -> X |- _ =>
      match goal with
      | y : Y |- _ => sselim_elim eq (f y)
      | g : ?Z -> Y |- _ =>
        match goal with
        | z : Z |- _ => sselim_elim eq (f (g z))
        end
      end
    | _ => fail "sselim: no hyp found"
    end
  | _ => fail "sselim: no eq found"
  end;  
  napply paths_ind_r;
  try clear eq;
  try clear f.

Tactic Notation "sselim" constr(x0) := sselim x0.
Tactic Notation "sselim" constr(x0) constr(x1) := sselim x0; sselim x1.
Tactic Notation "sselim" constr(x0) constr(x1) constr(x2) := sselim x0; sselim x1 x2.
Tactic Notation "sselim" constr(x0) constr(x1) constr(x2) constr(x3) := sselim x0; sselim x1 x2 x3.
Tactic Notation "sselim" constr(x0) constr(x1) constr(x2) constr(x3) constr(x4) := sselim x0; sselim x1 x2 x3 x4.
Tactic Notation "sselim" constr(x0) constr(x1) constr(x2) constr(x3) constr(x4) constr(x5) := sselim x0; sselim x1 x2 x3 x4 x5.
Tactic Notation "sselim" constr(x0) constr(x1) constr(x2) constr(x3) constr(x4) constr(x5) constr(x6) := sselim x0; sselim x1 x2 x3 x4 x5 x6.

Instance is01cat_ss : Is01Cat SuccStr.
Is01Cat SuccStr
Proof.
Is01Cat SuccStr
  snapply Build_Is01Cat.
forall a : SuccStr, a $-> a
forall a b c : SuccStr,
(b $-> c) -> (a $-> b) -> a $-> c
  -
forall a : SuccStr, a $-> a intro X.
X: SuccStr
X $-> X
    snapply Build_ssForall.
X: SuccStr
forall x : X, ssfam_const X x
X: SuccStr
forall x : X, ?ss_fun x.+1 = dss_succ (?ss_fun x)
    +
X: SuccStr
forall x : X, ssfam_const X x exact (fun x => x).
    +
X: SuccStr
forall x : X, idmap x.+1 = dss_succ (idmap x) reflexivity.
  -
forall a b c : SuccStr,
(b $-> c) -> (a $-> b) -> a $-> c intros X Y Z f g.
X, Y, Z: SuccStr
f: Y $-> Z
g: X $-> Y
X $-> Z
    snapply Build_ssForall.
X, Y, Z: SuccStr
f: Y $-> Z
g: X $-> Y
forall x : X, ssfam_const Z x
X, Y, Z: SuccStr
f: Y $-> Z
g: X $-> Y
forall x : X, ?ss_fun x.+1 = dss_succ (?ss_fun x)
    +
X, Y, Z: SuccStr
f: Y $-> Z
g: X $-> Y
forall x : X, ssfam_const Z x intro x.
X, Y, Z: SuccStr
f: Y $-> Z
g: X $-> Y
x: X
ssfam_const Z x
      exact (f (g x)).
    +
X, Y, Z: SuccStr
f: Y $-> Z
g: X $-> Y
forall x : X,
(fun x0 : X => f (g x0)) x.+1 =
dss_succ ((fun x0 : X => f (g x0)) x) intro x.
X, Y, Z: SuccStr
f: Y $-> Z
g: X $-> Y
x: X
(fun x : X => f (g x)) x.+1 =
dss_succ ((fun x : X => f (g x)) x)
      exact (ap f (ss_fun_succ g x) @ ss_fun_succ f (g x)).
Defined.

Instance is01cat_ssforall {A : SuccStr} (P : ssFam A)
  : Is01Cat (ssForall P).
A: SuccStr
P: ssFam A
Is01Cat (ssForall P)
Proof.
A: SuccStr
P: ssFam A
Is01Cat (ssForall P)
  snapply Build_Is01Cat.
A: SuccStr
P: ssFam A
forall a : ssForall P, a $-> a
A: SuccStr
P: ssFam A
forall a b c : ssForall P,
(b $-> c) -> (a $-> b) -> a $-> c
  -
A: SuccStr
P: ssFam A
forall a : ssForall P, a $-> a intro f.
A: SuccStr
P: ssFam A
f: ssForall P
f $-> f
    snapply Build_ssForall.
A: SuccStr
P: ssFam A
f: ssForall P
forall x : A, ssfam_sshomotopy f f x
A: SuccStr
P: ssFam A
f: ssForall P
forall x : A, ?ss_fun x.+1 = dss_succ (?ss_fun x)
    +
A: SuccStr
P: ssFam A
f: ssForall P
forall x : A, ssfam_sshomotopy f f x reflexivity.
    +
A: SuccStr
P: ssFam A
f: ssForall P
forall x : A,
(fun x0 : A => 1) x.+1 =
dss_succ ((fun x0 : A => 1) x) intro x; simpl.
A: SuccStr
P: ssFam A
f: ssForall P
x: A
1 = (ss_fun_succ f x @ 1) @ (ss_fun_succ f x)^
      by destruct (ss_fun_succ f x).
  -
A: SuccStr
P: ssFam A
forall a b c : ssForall P,
(b $-> c) -> (a $-> b) -> a $-> c intros f g h p q.
A: SuccStr
P: ssFam A
f, g, h: ssForall P
p: g $-> h
q: f $-> g
f $-> h
    snapply Build_ssForall.
A: SuccStr
P: ssFam A
f, g, h: ssForall P
p: g $-> h
q: f $-> g
forall x : A, ssfam_sshomotopy f h x
A: SuccStr
P: ssFam A
f, g, h: ssForall P
p: g $-> h
q: f $-> g
forall x : A, ?ss_fun x.+1 = dss_succ (?ss_fun x)
    +
A: SuccStr
P: ssFam A
f, g, h: ssForall P
p: g $-> h
q: f $-> g
forall x : A, ssfam_sshomotopy f h x intro x.
A: SuccStr
P: ssFam A
f, g, h: ssForall P
p: g $-> h
q: f $-> g
x: A
ssfam_sshomotopy f h x
      exact (q x @ p x).
    +
A: SuccStr
P: ssFam A
f, g, h: ssForall P
p: g $-> h
q: f $-> g
forall x : A,
(fun x0 : A => q x0 @ p x0) x.+1 =
dss_succ ((fun x0 : A => q x0 @ p x0) x) intro x; cbn.
A: SuccStr
P: ssFam A
f, g, h: ssForall P
p: g $-> h
q: f $-> g
x: A
q x.+1 @ p x.+1 =
(ss_fun_succ f x @ ap dss_succ (q x @ p x)) @
(ss_fun_succ h x)^
      sselim p q f g h.
A: SuccStr
P: ssFam A
f, g, h: forall x : A, P x
p: forall x : A, g x = h x
q: forall x : A, f x = g x
x: A
((1 @ ap dss_succ (q x)) @ 1) @
((1 @ ap dss_succ (p x)) @ 1^) =
(1 @ ap dss_succ (q x @ p x)) @ 1^ simpl.
A: SuccStr
P: ssFam A
f, g, h: forall x : A, P x
p: forall x : A, g x = h x
q: forall x : A, f x = g x
x: A
((1 @ ap dss_succ (q x)) @ 1) @
((1 @ ap dss_succ (p x)) @ 1) =
(1 @ ap dss_succ (q x @ p x)) @ 1
      by destruct (p x), (q x).
Defined.

Instance is0gpd_ssforall {A : SuccStr} (P : ssFam A)
  : Is0Gpd (ssForall P).
A: SuccStr
P: ssFam A
Is0Gpd (ssForall P)
Proof.
A: SuccStr
P: ssFam A
Is0Gpd (ssForall P)
  snapply Build_Is0Gpd.
A: SuccStr
P: ssFam A
forall a b : ssForall P, (a $-> b) -> b $-> a
  intros f g p.
A: SuccStr
P: ssFam A
f, g: ssForall P
p: f $-> g
g $-> f
  snapply Build_ssForall.
A: SuccStr
P: ssFam A
f, g: ssForall P
p: f $-> g
forall x : A, ssfam_sshomotopy g f x
A: SuccStr
P: ssFam A
f, g: ssForall P
p: f $-> g
forall x : A, ?ss_fun x.+1 = dss_succ (?ss_fun x)
  -
A: SuccStr
P: ssFam A
f, g: ssForall P
p: f $-> g
forall x : A, ssfam_sshomotopy g f x intro x.
A: SuccStr
P: ssFam A
f, g: ssForall P
p: f $-> g
x: A
ssfam_sshomotopy g f x
    exact (p x)^.
  -
A: SuccStr
P: ssFam A
f, g: ssForall P
p: f $-> g
forall x : A,
(fun x0 : A => (p x0)^) x.+1 =
dss_succ ((fun x0 : A => (p x0)^) x) intro x; cbn.
A: SuccStr
P: ssFam A
f, g: ssForall P
p: f $-> g
x: A
(p x.+1)^ =
(ss_fun_succ g x @ ap dss_succ (p x)^) @
(ss_fun_succ f x)^
    sselim p f g.
A: SuccStr
P: ssFam A
f, g: forall x : A, P x
p: forall x : A, f x = g x
x: A
((1 @ ap dss_succ (p x)) @ 1^)^ =
(1 @ ap dss_succ (p x)^) @ 1
    by destruct (p x).
Defined.

Instance is1cat_ss : Is1Cat SuccStr.
Is1Cat SuccStr
Proof.
Is1Cat SuccStr
  snapply Build_Is1Cat'.
forall a b : SuccStr, Is01Cat (a $-> b)
forall a b : SuccStr, Is0Gpd (a $-> b)
forall (a b c : SuccStr) (g : b $-> c),
Is0Functor (cat_postcomp a g)
forall (a b c : SuccStr) (f : a $-> b),
Is0Functor (cat_precomp c f)
forall (a b c d : SuccStr) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f)
forall (a b : SuccStr) (f : a $-> b), Id b $o f $== f
forall (a b : SuccStr) (f : a $-> b), f $o Id a $== f
  1,2: exact _.
forall (a b c : SuccStr) (g : b $-> c),
Is0Functor (cat_postcomp a g)
forall (a b c : SuccStr) (f : a $-> b),
Is0Functor (cat_precomp c f)
forall (a b c d : SuccStr) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f)
forall (a b : SuccStr) (f : a $-> b), Id b $o f $== f
forall (a b : SuccStr) (f : a $-> b), f $o Id a $== f
  -
forall (a b c : SuccStr) (g : b $-> c),
Is0Functor (cat_postcomp a g) intros X Y Z g.
X, Y, Z: SuccStr
g: Y $-> Z
Is0Functor (cat_postcomp X g)
    snapply Build_Is0Functor.
X, Y, Z: SuccStr
g: Y $-> Z
forall a b : X $-> Y,
(a $-> b) -> cat_postcomp X g a $-> cat_postcomp X g b
    intros f h p.
X, Y, Z: SuccStr
g: Y $-> Z
f, h: X $-> Y
p: f $-> h
cat_postcomp X g f $-> cat_postcomp X g h
    snapply Build_ssForall.
X, Y, Z: SuccStr
g: Y $-> Z
f, h: X $-> Y
p: f $-> h
forall x : X,
ssfam_sshomotopy (cat_postcomp X g f)
  (cat_postcomp X g h) x
X, Y, Z: SuccStr
g: Y $-> Z
f, h: X $-> Y
p: f $-> h
forall x : X, ?ss_fun x.+1 = dss_succ (?ss_fun x)
    +
X, Y, Z: SuccStr
g: Y $-> Z
f, h: X $-> Y
p: f $-> h
forall x : X,
ssfam_sshomotopy (cat_postcomp X g f)
  (cat_postcomp X g h) x intro x.
X, Y, Z: SuccStr
g: Y $-> Z
f, h: X $-> Y
p: f $-> h
x: X
ssfam_sshomotopy (cat_postcomp X g f)
  (cat_postcomp X g h) x
      exact (ap g (p x)).
    +
X, Y, Z: SuccStr
g: Y $-> Z
f, h: X $-> Y
p: f $-> h
forall x : X,
(fun x0 : X => ap g (p x0)) x.+1 =
dss_succ ((fun x0 : X => ap g (p x0)) x) intro x; cbn.
X, Y, Z: SuccStr
g: Y $-> Z
f, h: X $-> Y
p: f $-> h
x: X
ap g (p x.+1) =
((ap g (ss_fun_succ f x) @ ss_fun_succ g (f x)) @
 ap ss_succ (ap g (p x))) @
(ap g (ss_fun_succ h x) @ ss_fun_succ g (h x))^
      sselim p f h.
X, Y, Z: SuccStr
g: ssForall (ssfam_const Z)
f, h: X -> Y
p: forall x : X, f x = h x
x: X
ap g ((1 @ ap ss_succ (p x)) @ 1^) =
((1 @ ss_fun_succ g (f x)) @ ap ss_succ (ap g (p x))) @
(ap g 1 @ ss_fun_succ g (h x))^
      destruct (p x); clear p; simpl.
X, Y, Z: SuccStr
g: ssForall (ssfam_const Z)
f, h: X -> Y
x: X
1 =
((1 @ ss_fun_succ g (f x)) @ 1) @
(1 @ ss_fun_succ g (f x))^
      sselim g.
X, Y, Z: SuccStr
g: Y -> Z
eq: forall x : Y, g x.+1 = (g x).+1
f, h: X -> Y
x: X
1 = ((1 @ eq (f x)) @ 1) @ (1 @ eq (f x))^
      by destruct (eq (f x)).
  -
forall (a b c : SuccStr) (f : a $-> b),
Is0Functor (cat_precomp c f) intros X Y Z g.
X, Y, Z: SuccStr
g: X $-> Y
Is0Functor (cat_precomp Z g)
    snapply Build_Is0Functor.
X, Y, Z: SuccStr
g: X $-> Y
forall a b : Y $-> Z,
(a $-> b) -> cat_precomp Z g a $-> cat_precomp Z g b
    intros f h q.
X, Y, Z: SuccStr
g: X $-> Y
f, h: Y $-> Z
q: f $-> h
cat_precomp Z g f $-> cat_precomp Z g h
    snapply Build_ssForall.
X, Y, Z: SuccStr
g: X $-> Y
f, h: Y $-> Z
q: f $-> h
forall x : X,
ssfam_sshomotopy (cat_precomp Z g f)
  (cat_precomp Z g h) x
X, Y, Z: SuccStr
g: X $-> Y
f, h: Y $-> Z
q: f $-> h
forall x : X, ?ss_fun x.+1 = dss_succ (?ss_fun x)
    +
X, Y, Z: SuccStr
g: X $-> Y
f, h: Y $-> Z
q: f $-> h
forall x : X,
ssfam_sshomotopy (cat_precomp Z g f)
  (cat_precomp Z g h) x intros x.
X, Y, Z: SuccStr
g: X $-> Y
f, h: Y $-> Z
q: f $-> h
x: X
ssfam_sshomotopy (cat_precomp Z g f)
  (cat_precomp Z g h) x
      apply q.
    +
X, Y, Z: SuccStr
g: X $-> Y
f, h: Y $-> Z
q: f $-> h
forall x : X,
(fun x0 : X => let X0 := ss_fun q in X0 (g x0)) x.+1 =
dss_succ
  ((fun x0 : X => let X0 := ss_fun q in X0 (g x0)) x) intros x; cbn.
X, Y, Z: SuccStr
g: X $-> Y
f, h: Y $-> Z
q: f $-> h
x: X
q (g x.+1) =
((ap f (ss_fun_succ g x) @ ss_fun_succ f (g x)) @
 ap ss_succ (q (g x))) @
(ap h (ss_fun_succ g x) @ ss_fun_succ h (g x))^
      by sselim g q f h.
  -
forall (a b c d : SuccStr) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f) intros X Y Z W f g h.
X, Y, Z, W: SuccStr
f: X $-> Y
g: Y $-> Z
h: Z $-> W
h $o g $o f $== h $o (g $o f)
    srapply Build_ssForall.
X, Y, Z, W: SuccStr
f: X $-> Y
g: Y $-> Z
h: Z $-> W
forall x : X,
ssfam_sshomotopy (h $o g $o f) (h $o (g $o f)) x
X, Y, Z, W: SuccStr
f: X $-> Y
g: Y $-> Z
h: Z $-> W
forall x : X, ?ss_fun x.+1 = dss_succ (?ss_fun x)
    +
X, Y, Z, W: SuccStr
f: X $-> Y
g: Y $-> Z
h: Z $-> W
forall x : X,
ssfam_sshomotopy (h $o g $o f) (h $o (g $o f)) x intro x.
X, Y, Z, W: SuccStr
f: X $-> Y
g: Y $-> Z
h: Z $-> W
x: X
ssfam_sshomotopy (h $o g $o f) (h $o (g $o f)) x
      reflexivity.
    +
X, Y, Z, W: SuccStr
f: X $-> Y
g: Y $-> Z
h: Z $-> W
forall x : X,
(fun x0 : X => 1) x.+1 =
dss_succ ((fun x0 : X => 1) x) intro x; cbn.
X, Y, Z, W: SuccStr
f: X $-> Y
g: Y $-> Z
h: Z $-> W
x: X
1 =
((ap (fun x : Y => h (g x)) (ss_fun_succ f x) @
  (ap h (ss_fun_succ g (f x)) @
   ss_fun_succ h (g (f x)))) @ 1) @
(ap h (ap g (ss_fun_succ f x) @ ss_fun_succ g (f x)) @
 ss_fun_succ h (g (f x)))^
      by sselim f g h.
  -
forall (a b : SuccStr) (f : a $-> b), Id b $o f $== f intros X Y f.
X, Y: SuccStr
f: X $-> Y
Id Y $o f $== f
    srapply Build_ssForall.
X, Y: SuccStr
f: X $-> Y
forall x : X, ssfam_sshomotopy (Id Y $o f) f x
X, Y: SuccStr
f: X $-> Y
forall x : X, ?ss_fun x.+1 = dss_succ (?ss_fun x)
    1: reflexivity.
X, Y: SuccStr
f: X $-> Y
forall x : X,
(fun x0 : X => 1) x.+1 =
dss_succ ((fun x0 : X => 1) x)
    intros x.
X, Y: SuccStr
f: X $-> Y
x: X
(fun x : X => 1) x.+1 = dss_succ ((fun x : X => 1) x)
    by sselim f.
  -
forall (a b : SuccStr) (f : a $-> b), f $o Id a $== f intros X Y f.
X, Y: SuccStr
f: X $-> Y
f $o Id X $== f
    srapply Build_ssForall.
X, Y: SuccStr
f: X $-> Y
forall x : X, ssfam_sshomotopy (f $o Id X) f x
X, Y: SuccStr
f: X $-> Y
forall x : X, ?ss_fun x.+1 = dss_succ (?ss_fun x)
    1: reflexivity.
X, Y: SuccStr
f: X $-> Y
forall x : X,
(fun x0 : X => 1) x.+1 =
dss_succ ((fun x0 : X => 1) x)
    intros x.
X, Y: SuccStr
f: X $-> Y
x: X
(fun x : X => 1) x.+1 = dss_succ ((fun x : X => 1) x)
    by sselim f.
Defined.