Why we want functional Extentionality in formality

funext.fm

// Let's start our lawful Functor abstraction

T Functor {F : Type -> Type}
| functor
  { map : {~A : Type , ~B : Type , f : A -> B, x : F(A)} -> F(B)
  , identity : {~A : Type , fa : F(A)} -> map(~A, ~A, id(~A),fa) == fa
  , composition :
    { ~A : Type
    , ~B : Type
    , ~C : Type
    , g  : B -> C
    , f  : A -> B
    , fa : F(A)
    } -> map(~A, ~C, {x} g(f(x)), fa) == map(~B, ~C, g, map(~A, ~B, f, fa))
  }
  
// This works great for type constructors like Maybe
maybe.functor : Functor(Maybe)
  let map = {~A, ~B, f, x}
    case/Maybe x
    | just => just(~B, f(x.value))
    | none => none(~B)
    : Maybe(B)
  let identity = {~A, ma}
    case/Maybe ma
    | just => refl(~just(~A,ma.value))
    | none => refl(~none)
    : map(~A,~A,id(~A),ma) == ma
  let composition = {~A, ~B, ~C, g, f, ma}
    case/Maybe ma
    | just => refl(~just(~C,(g(f(ma.value)))))
    | none => refl(~none)
    : map(~A,~C,{x:A} g(f(x)),ma) == map(~B,~C,g,map(~A,~B,f,ma))
  functor(~Maybe,map,identity,composition)

// But if we try to define it for Fun(A) we have a problem
Fun : {A : Type, B : Type} -> Type
  A -> B

fun.functor : {A : Type} -> Functor(Fun(A))
functor(~Fun(A),compose(~A),?id,?comp)

// Hole found: 'id'
// - With goal... {~A : Type, fa : Fun(A^, A)} -> compose(~A^, ~A, ~A, id(~A), fa) == fa
// Hole found: 'comp'
// - With goal... {~A : Type, ~B : Type, ~C : Type, g : {:B} -> C, f : {:A} -> B, fa : Fun(A^, A)} -> 
//    compose(~A^, ~A, ~C, {x} => g(f(x)), fa) == compose(~A^, ~B, ~C, g, compose(~A^, ~A, ~B, f, fa))

// Since `==` is intensional, we can't actually construct a term of type `compose(~A^, ~A, ~A, id(~A), fa) == fa`

// So we're left with two options

// Option 1: Make unlawful functors like Haskell:

T UnlawfulFunctor {F : Type -> Type}
| unlawful_functor
  { map : {~A : Type , ~B : Type , f : A -> B, x : F(A)} -> F(B)
  }

// Option 2: Setoid hell:

T Setoid {A : Type}
| setoid
  { R           : Relation(A)
  , equivalence : Equivalence(A, R)
  }

T SetoidFunctor {F : Type -> Type, s : {A : Type} -> Setoid(F(A))}
| setoid_functor
  { map : {~A : Type , ~B : Type , f : A -> B, x : F(A)} -> F(B)
  , identity : {~A : Type , fa : F(A)} ->
      case/Setoid s(A) as s | setoid =>
        s.R(map(~A, ~A, id(~A),fa),fa)
      : Type
  , composition :
    { ~A : Type
    , ~B : Type
    , ~C : Type
    , g  : B -> C
    , f  : A -> B
    , fa : F(A)
    } -> case/Setoid s(C) as s | setoid =>
           s.R(map(~A, ~C, {x} g(f(x)), fa), map(~B, ~C, g, map(~A, ~B, f, fa)))
         : Type
  }


// Setoid Hell really is awful because when we want to make an equivalence relation for functions 
// we can't use `==` like we want to:

// Extentional equality for functions
Funext : {A : Type, B : Type, f : A -> B, g : A -> B} -> Type
  {x : A} -> f(x) == g(x)

// We have add another Setoid in case e.g. the function codomain is higher order, like another function

// Extentional equality for functions w/ codomain setoid
Funext_Hell : 
  { A : Type
  , B : Type
  , s : Setoid(B)
  , f : A -> B
  , g : A -> B
  } -> Type
    {x : A} -> case/Setoid s | setoid => s.R(f(x),g(x))

// This causes endless proliferation of Setoids and is basically so noisy as to be impractical.