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 }