Section fold_Nat.
Variable B:Set.
Variable f:B -> B.
Variable b0:B.
Fixpoint foldr_nat (n:nat){struct n}:B:=
match n with
0 => b0
| (S n0) => f (foldr_nat  n0)
end.


Fixpoint foldl_nat (b:B)(n:nat){struct n}:B:=
match n with
0 =>  b
 | (S n0) => foldl_nat  (f b) n0
end.

Implicit Arguments foldr_nat.
Implicit Arguments foldl_nat.

Lemma value_r: forall  f b n, foldr_nat  f  b (S n)= f (foldr_nat  f b n).
Proof.
intuition.
Qed.

Lemma value_l: forall  f b n, foldl_nat  f b (S n)=foldl_nat  f (f b) n.
Proof.
intuition.
Qed.

Lemma aux_value: forall n  f b, f (foldl_nat  f b n)=foldl_nat  f (f b) n.
Proof.
induction n.
auto.
intuition.
rewrite  (value_l). 
rewrite value_l.
rewrite <- (IHn B f (f b)).
auto.
Qed.

Lemma coinc: forall n  f b , foldr_nat  f b n = foldl_nat  f b n.
Proof.
induction n;intuition.
rewrite value_r.
rewrite IHn.
rewrite  value_l.
apply aux_value.
Qed.

Definition h1 :=fun (b:B) => fun (n:nat) => (pair  b (S n)).
Definition h2 :=fun (b:B) => fun (n:nat) => ((f b),n).

Lemma one: forall b:B, forall n:nat,
(foldl_nat f  (fst (h1  b n)) (snd (h1 b n)))=
         (foldl_nat f (fst (h2 b n)) (snd (h2 b n))).
Proof.
intros.
 auto.  
 Qed.   
 Variable C:Set.

 Lemma coequalizer_nat: forall h:B -> nat -> C, (forall n b,
 (h (fst (h1  b n)) (snd (h1 b n)))=(h (fst (h2 b n)) (snd (h2 b n))))
  -> { f':B->C | (forall n b, f'(foldl_nat f b n)=h b n ) 
        /\ (forall (g:B -> C),(forall  n b, g (foldl_nat f  b n)=h b n)
            -> forall b:B,g b=f' b) } .
 Proof.           
 intros.
 exists (fun b:B => h b 0).
 split.
 induction n.
 intuition.  
 simpl in H. 
 intros.
 simpl. 
 rewrite H.
 apply IHn.
 intros.
 replace (g b) with (g (foldl_nat b 0));intuition.
 Qed.
 
End fold_Nat.