test3.sott

define Bool : Set as {| `True, `False |}

define sum :
  Set -> Set -> Set
as \A B -> (x : Bool) * (x for x. Set { `True -> A; `False -> B })

define inl :
  (A:Set)(B:Set) -> A -> sum A B
as \A B a -> (`True, a)

define symm :
  (A : Set)(x : A)(y : A)(p : [x : A = y : A]) -> [y : A = x : A]
as
  \A x y p ->
     coerce(refl,[x : A = x : A],[y : A = x : A],subst(A,z.[z : A = x : A],x,y,p))

(* Failure of canonicity -- if coerce doesn't compute past the pair,
   then we get a coercion expression where there ought to be a boolean
   in the first component of the pair. *)

define and :
  Bool -> Bool -> Bool
as \x y -> x for y. Bool { `True -> y; `False -> `False }

(* An easier to use functional extensionality principle *)
define funext2 :
  (S : Set)(T : S -> Set)(f : (x : S) -> T x)(g : (x : S) -> T x) ->
  ((x : S) -> [f x : T x = g x : T x]) ->
  [f : (x : S) -> T x = g : (x : S) -> T x]
as \S T f g e ->
   funext (x1 x2 xe. coerce(e x1,
                            [f x1 : T x1 = g x1 : T x1],
                            [f x1 : T x1 = g x2 : T x2],
                            subst(S,y.[f x1 : T x1 = g y : T y],x1,x2,xe)))

define eq_funcs :
  [ \b -> `False : Bool -> Bool = \b -> and b `False : Bool -> Bool]
as
  funext2 Bool (\x -> Bool) (\b -> `False) (\b -> and b `False) 
    (\b -> b for b. [`False : Bool = and b `False : Bool ]
                { `True -> refl; `False -> refl })

define F : (Bool -> Bool) -> Set
as \f -> sum [f : Bool -> Bool = \x -> `False : Bool -> Bool]
             [f : Bool -> Bool = \x -> `True : Bool -> Bool]

define v : F (\x -> `False)
as (`True, refl)

define hofmann2 : F (\x -> and x `False)
as coerce(v, F (\x -> `False), F (\x -> and x `False),
          subst(Bool -> Bool,x. F x, (\x -> `False), (\x -> and x `False), eq_funcs))

define test :
  [hofmann2 : F (\x -> and x `False) =
   (`True, symm (Bool -> Bool) (\x -> `False) (\x -> and x `False) eq_funcs)
      : F (\x -> and x `False)
      ]
as
  refl