How do you declare a specific instance of uip for Equations ?
Because in the refman it is written
Module KAxiom.
(*By default we disallow the user of UIP, but it can be set.*)
Set Equations With UIP .
Module WithAx.
(* The user must declare this axiom itself, as an instance of the UIP class. *)
Axiom uipa : ∀ A, UIP A.
Local Existing Instance uipa.
(* In this case the following definition uses the UIP axiom just declared. *)
Equations K {A} (x : A) (P : x = x → Type) (p : P eq refl)
(H : x = x ) : P H :=
K x P p eq refl := p.
End WithAx.
but it is to declare a global instance, right ?
You can also just add "Instance : UIP mytype" to the context
Last updated: Oct 13 2024 at 01:02 UTC