funiso.red

funiso.red

import prelude
import basics.isotoequiv

def curry (A B C : type) : ((A × B) → C) → (A → B → C) = 
  λ f a b → f (a, b)

def uncurry (A B C : type) : (A → B → C) → ((A × B) → C) = 
  λ f (a, b) → f a b

def iso/curry (A B C : type) : iso (A → B → C) ((A × B) → C) = 
  ( uncurry _ _ _
  , curry _ _ _
  , λ _ → refl
  , λ _ → refl
  )

def iso/lhs (A B C : type) (I : iso A B) : iso (A → C) (B → C) = 
  let (f,g,α,β) = I in
  ( λ ac b → ac (g b)
  , λ bc a → bc (f a)
  , λ bc i b → bc (α b i)
  , λ ac i a → ac (β a i)
  )

def iso/rhs (A B C : type) (I : iso A B) : iso (C → A) (C → B) = 
  let (f,g,α,β) = I in
  ( λ ca c → f (ca c)
  , λ cb c → g (cb c)
  , λ cb i c → α (cb c) i
  , λ ca i c → β (ca c) i
  )

def iso/flip (A B C : type) : iso (A → B → C) (B → A → C) = 
  ( λ f b a → f a b
  , λ f a b → f b a
  , λ _ → refl
  , λ _ → refl
  )