Last active
December 14, 2015 00:38
-
-
Save peterlefanulumsdaine/4999790 to your computer and use it in GitHub Desktop.
Code attachment for [this issue](https://github.com/HoTT/coq/issues/19) on [HoTT/coq](https://github.com/HoTT/coq)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Inductive equals {A : Type} (a : A) : A -> Type := | |
refl : equals a a. | |
Arguments refl {A a} , [A] a. | |
Notation "x = y" := (equals x y). | |
Definition flip {A B : Type} {P : A -> B -> Type} | |
: (forall a b, P a b) -> (forall b a, P a b) | |
:= fun f b a => f a b. | |
Variables (A B : Type) (P : A -> B -> Type). | |
Let flip_P := @flip _ _ P. | |
Let flip_P_inv := @flip _ _ (flip P). | |
Set Printing All. | |
Set Printing Universes. | |
(* Succeeds: *) | |
Definition flip_P_is_retr1 : forall g, flip_P_inv (flip_P g) = g. | |
Proof. | |
intro g. unfold flip_P, flip_P_inv, flip. exact (refl g). | |
Defined. | |
(* Fails: *) | |
Definition flip_P_is_retr2 : forall g, flip_P_inv (flip_P g) = g. | |
Proof. | |
intro g. exact (refl g). | |
Defined. | |
(* Fails (even though the definiens is exactly the output of [Print flip_P_is_retr1.]): *) | |
Definition flip_P_is_retr3 : forall g, flip_P_inv (flip_P g) = g | |
:= | |
(fun g : forall (a : A) (b : B), P a b => | |
@refl (forall (a : A) (b : B), P a b) g | |
: forall g : forall (a : A) (b : B), P a b, | |
@equals | |
(forall (b : A) (a : B), | |
@flip A B (fun (_ : A) (_ : B) => Type) P a b) | |
(flip_P_inv (flip_P g)) g). | |
(* If we avoid using [flip P] (i.e. using flip at a higher universe level), then things work fine: *) | |
Let flip_P_inv' := @flip _ _ (fun b a => P a b). | |
Definition flip_P_is_retr4 : forall g, flip_P_inv' (flip_P g) = g. | |
Proof. | |
intro g. exact (refl g). | |
Defined. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment