interiorFoldLemma

interiorFoldLemma.agda

    interiorFoldLemma :
      (pq : [ P -:> Q ])(qalg : Algebra (CUTTING C) Q)
      (f : [ Interior C P -:> Q ]) ->
      ((i : I)(p : P i) -> pq i p == f i (tile p)) ->
      ((i : I)(c : Cuts i)(ps : All (Interior C P) (inners c)) ->
        qalg i (c 8>< all f (inners c) ps) == f i < c 8>< ps >) ->
      (i : I)(pi : Interior C P i) -> interiorFold pq qalg i pi == f i pi

    interiorFoldLemma pq qalg f base step i (tile x) = base i x
    interiorFoldLemma pq qalg f base step i < c 8>< pi >
       rewrite allInteriorFoldLaw pq qalg
          | sym (step i c pi)
      = refl (\ x -> qalg i (c 8>< all x (inners c) pi)) =$=
          extensionality \ i1 -> extensionality \ pi1 ->
            -- XXX: termination checker complains :(
            -- interiorFoldLemma pq qalg {!f!} {!base!} {!step!} i1 pi1
            {!!}