[Agda] universe with extensional propositional equality?

[James Chapman]

Hi Dan,

On Apr 8, 2009, at 3:48 AM, Dan Licata wrote:

> 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

It isn't reflexive. Eq is a partial equivalence relation. It's also a  
logical relation (<_> is a logical predicate). Is it a PER model?

> 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.

I think it doesn't hold for all functions, it only holds for functions  
that are in the equality relation. This is as you would expect for a  
PER. In general reflexivity only holds for elements that are in the  
PER: Eq x y implies Eq x x.

>
> 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).

I'm not an OTT expert (I'm not sure if I'm even an amateur). However,  
I think that in OTT when reflexivity is added as an axiom it is  
something new (to turn equality into a proper equivalence relation),  
it is just something that is axiomatized as it hasn't been proven yet  
and will be removed later.

Regards,

James