[Agda] Typed Jigger in vanilla Agda.

[Roman]

Hi guys. A while ago Conor McBride presented "A little hack to make de
Bruijn syntax more readable": [1]

To save a click, it allows to use host language binders like in HOAS,
but get first-order terms:

    data Tm (n : Nat) : Set where
      V : Fin n -> Tm n
      _$_ : Tm n -> Tm n -> Tm n
      L : Tm (suc n) -> Tm n

    l : {m : Nat} -> (({n : Nat} -> Tm (suc (m + n))) -> Tm (suc m)) -> Tm m
    l {m} f = L (f \{n} -> V (var m {n}))

    myTest : Tm zero
    myTest = l \ f -> l \ x -> f $ (f $ x)

But those terms are well-scoped and not well-typed. Conor found a way
to do the same in a well-typed setting and described it in his
DataData lecture notes [2]. But this new trick relies on the instance
resolution algorithm and became broken at some point if I recall
correctly. Then it was fixed, but instance resolution is still a
rather heavy tool to use. And using instance arguments one can write a
simpler thing: [3] (was broken previously as well)

However since Agda is so amazing, we can write a typed Jigger
machinery without relying on instance arguments: [4]

[1] https://personal.cis.strath.ac.uk/conor.mcbride/fooling/Jigger.agda
[2] https://github.com/pigworker/SSGEP-DataData
[3] https://github.com/effectfully/random-stuff/blob/master/TypedJigger.agda
[4] https://github.com/effectfully/random-stuff/blob/master/VanillaTypedJigger.agda