more funext

HIT.fm

import Data.Empty
import Data.Unit

Interval : Type
  $self
  { ~P  : {i : Interval} -> Type
  , I0  : P(i0)
  , I1  : P(i1)
  , ~SG : I0 == I1
  } -> [x : P(self) ~ I0 == I1]

i0 : Interval
  new(~Interval){~P, i0, i1, ~sg} [i0 ~ sg]

i1 : Interval
  new(~Interval){~P, i0, i1, ~sg} [i1 ~ sg]

sg : i0 == i1
  snd~((%i0)(~{i} Interval, i0, i1, ~sg))


funext :
  { ~A : Type
  , ~B : {x : A} -> Type
  , f : !({x : A} -> B(x))
  , g : !({x : A} -> B(x))
  , H : !({x : A} -> <f>(x) == <g>(x))
  } -> f == g
  let c = cong(~funext_helper(~A,~B,f,g,H),~sg)
  let ff = refl(~funext_helper(~A,~B,f,g,H,i0))
  log(ff)
  log(c)
  ?h

funext_helper :
  { ~A : Type
  , ~B : Type
  , f  : !(A -> B)
  , g  : !(A -> B)
  , H  : !({x : A} -> <f>(x) == <g>(x))
  , interval : !Interval
  , a  : !A
  } -> ![:B ~ <f>(<a>) == <g>(<a>)]
  dup a = a
  dup f = f
  dup g = g
  dup H = H
  dup interval = interval
  # funext_helper.go(~B,interval,f(a),g(a), H(a))

funext_helper.go :
  { ~B : Type
  , interval : Interval
  , fa  : B
  , ga  : B
  , Ha  : fa == ga
  } -> [:B ~ fa == ga]
  (%interval)(~{self} B
  , fa
  , ga
  , ~Ha
  )