This file finds the morphisms mappable over the list of lists [[1,2],[3]] when considered with respect to the specification List[β₁]. Note that the data in the list happen to be lists themselves, but this is incidental.
module ex4-4 where open import map open import nat using (1Nat ; 2Nat ; 3Nat) open import list using (List[_] ; ⊢List ; nil[] ; cons[_,_] ) open import Data.List using ([] ; _∷_ ; [_]) open import Data.Vec renaming ([] to [||] ; _∷_ to _¦_ ; [_] to [|_|] )
We start with the declaration of variables that will be used in the call to adm.
β₁ : mix-var
β₁ = tvar 0
Γβ₁ : type-context {mix-var}
Γβ₁ = ⟦ [| β₁ |] ⟧
f : mix-var
f = fvar 0
We then define the term of Example 2.4, and the specification with respect to which we are considering it.
t = cons[ cons[ 1Nat , cons[ 2Nat , nil[] ] ] , cons[ cons[ 3Nat , nil[] ] , nil[] ] ]
⊢List[β₁] : Γβ₁ ∥ ∅ ⊢ List[ varᵀ β₁ ]
⊢List[β₁] = ⊢List (var-intro ∋-last)
C,s = adm t ⊢List[β₁] [| varᵀ f |] (record { curr = 1 }) []