dkrustev

// So called van Laarhoven lenses, named after their discoverer, have a number
// of nice properties as explained by Russell O'Connor:
//
//   http://r6.ca/blog/20120623T104901Z.html
//
// Unfortunately their typing (in Haskell)
//
//   type Lens s t a b = forall f. Functor f => (a -> f b) -> (s -> f t)
//
// seems to be well outside of what can be achieved in F#.

dkrustev

module Unify where

-- Translated from http://strictlypositive.org/unify.ps.gz

open import Data.Empty
import Data.Maybe as Maybe
open Maybe hiding (map)
open import Data.Nat
open import Data.Fin
open import Data.Product hiding (map)

dkrustev

(* author: Dimitur Krustev *)
(* started: 20130616 *)
(* based on: http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html *)

Require Import Arith List Bool.

Set Implicit Arguments.

Section Lang.