[Agda] universe with extensional propositional equality?

[Dan Licata]

Hi everyone,

Suppose I define a little universe as follows:

  data Tp : Set where 
    bool : Tp
    _⊃_  : Tp -> Tp -> Tp

  <_> : Tp -> Set
  < bool >  = Bool
  < A ⊃ B > = < A > -> < B >

I'd like to define a notion of propositional equality that treats
functions extensionally, like this:

  Eq : {A : Tp} -> < A > -> < A > -> Set
  Eq {bool} True  True  = Unit
  Eq {bool} False False = Unit
  Eq {bool} True  False = Void
  Eq {bool} False True  = Void
  Eq {A ⊃ B} f g = (x y : < A >) -> Eq x y -> Eq (f x) (g y)
	  
However, I can't seem to prove that this notion of equality is
reflexive:

  refl : {A : Tp} -> (e : < A >) -> Eq e e

For functions, you need to show 

  refl {A ⊃ B} f = 
   (? : (x : < A >) (y : < A >) -> Eq x y -> Eq (f x) (f y))

i.e. that functions take equals to equals.  

My hunch is that all Agda functions in this little universe do take
equals to equals (e.g., OTT has reflexivity and substitutivity as
axioms---they're at least consistent).  

But can you prove them inside the system?  Or, if not, why not?

-Dan