module Chapter8.Container.Morphism.Examples.List 
         {A : Set}
       where

open import Function

open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Chapter5.Container.Examples.Nat
open import Chapter5.Container.Examples.List

open import Chapter8.Container.Morphism.Cartesian

τ : ListCont A ⇒c[ id ∣ id ] NatCont
τ = record { σ = λ { (inj₁ tt) → inj₁ tt 
                   ; (inj₂ a) → inj₂ tt }
           ; ρ = λ { {j} {inj₁ tt} → refl
                   ; {j} {inj₂ a} → refl }
           ; q = λ p → refl }