foldr I combinator composition

id_fold.v

   Require Import Coq.Program.Basics Coq.Lists.List FunctionalExtensionality.
   
   Import Coq.Lists.List.ListNotations.

   Fixpoint replicate (T : Type) (e : T) n :=
     match n with
       | 0 => []
       | S n => e :: replicate T e n
     end.
     
   Eval simpl in replicate nat 0 0.
   Eval simpl in replicate nat 0 1.
   Eval simpl in replicate nat 0 2.
    
   Theorem compose_id : forall (f : Type -> Type),
                        compose id f = f.
   Proof.
      intros. unfold compose, id. now rewrite eta_expansion.
   Qed.

   Theorem id_fold : forall (f : Type -> Type)
                       (g : Type -> Type) 
                       (n : nat), 
                     fold_right (fun g f : Type -> Type => compose g f) 
                                id 
                                (replicate (Type -> Type) id n)
                     = id.
   Proof.
      intros. induction n.
      - now simpl.
      - simpl. now rewrite compose_id. 
   Qed.