Coq-HoTT
Coq-HoTT copied to clipboard
HoTT
Can coq pointify types?
Can we turn Build_pType into a coercion, such that whenever coq expects a pType but is supplied a Type instead, it goes and searches for a IsPointed?
For example, I would like to be able to have an instance for pMap being pointed. So that if I give a pMap where Coq expects a pType, it knows how to pointify it.
I haven't been able to get this to work. I don't know how to make Build_pType a coercion.
For the pMap example, the type pMap A B is pointed by the constant pmap which sends everything in A to the basepoint of B.
I would be interested if anybody has a solution for this.
This sounds like maybe the use case of Canonical Structures?
However, when possible, I think it often works better to define things to be pointed types by default and coerce them in the other direction. For instance, it might be better to define pMap to be a pType that gets coerced to a Type rather than the other way around.
Coq does not permit Sortclass to be the source of a coercion, IIRC, and anyway coercions must be total and cannot use typeclass resolution to insert arguments. I think Mike's suggestion is a good one.
Once my torus PR #1066 is merged, I have a PR that will reorganise the Pointed file into a library. I will see, after that is merged, if making pMap a pType can be done. The main use that will come out of this change will be formalising the smash product / pointed map adjunction.
So it is not as easy as setting pMap to be a type. I have tried the following:
(** ** Pointed functions *)
(* A pointed map is a map with a proof that it preserves the point *)
Record pMap' (A B : pType) := {
pointed_fun' : A -> B ;
point_eq' : pointed_fun' (point A) = point B
}.
(* We use pMap' to arrive at a version of pMap which is itself a pType *)
Definition pMap (A B : pType) : pType
:= Build_pType (pMap' A B) (Build_pMap' _ _ (const (point B)) 1).
Definition Build_pMap (A B : pType) (f : A -> B)
: f (point A) = point B -> pMap A B := Build_pMap' A B f.
Coercion pointed_fun (A B : pType) : pMap A B -> A -> B := pointed_fun' A B.
Definition point_eq (A B : pType) (p : pMap A B)
: pointed_fun A B p (point A) = point B.
Proof.
apply point_eq'.
Defined.
(* TODO:
- write pMap_ind pMap_Rec
- set elimination principle for pMap
- hide pMap' from public view
*)
Arguments point_eq {A B} f : rename.
(* Coercion pointed_fun : pMap >-> Funclass. *)
Infix "->*" := pMap : pointed_scope.
Definition pmap_idmap {A : pType} : A ->* A
:= Build_pMap A A idmap 1.
Definition pmap_compose {A B C : pType} (g : B ->* C) (f : A ->* B) : A ->* C
:= Build_pMap A C (g o f)
(ap g (point_eq f) @ point_eq g).
Infix "o*" := pmap_compose : pointed_scope.
I am hoping to hide pMap' out of view but I am running into a few issues. In the definition of pmap_compose g and f are coerced to functions. pointed_fun is supposed to be a coercion but the original declaration didn't work so I defined pmap_compose as a coercion. However coq wasn't happy with this and said:
pointed_fun is defined
pointed_fun does not respect the uniform inheritance condition
[uniform-inheritance,typechecker]
pointed_fun is now a coercion
But I can't progress into pmap_compose, because g and f won't coerce:
In environment
A : pType
B : pType
C : pType
g : B ->* C
f : A ->* B
The term "g" has type "pointed_type (B ->* C)" while it is expected to have type
"forall x : ?T, ?T0".
Perhaps you want to coerce pMap instead into Funclass?
However, this sort of problem is one reason it generally seems better to work with unbundled things, with IsPointed typeclass hypotheses rather than arguments of type pType.
@mikeshulman If I understand coercions correctly, then pMap is being coerced into Funclass.
I am not so sure about IsPointed in general however. When I was defining homotopy groups, I couldn't define iterated loops using IsPointed because the typeclass resolution wasn't clever enough to see that the correct basepoint was being mentioned. These problems went away when I packaged everything together.
It is also sometimes useful to specify your own basepoint, not just the canonical one. Take for example the local-global looping principle, where loops in Type based at A are equivalent to forall a : A, loops in A centered at a. (This is proven in Kraus-Sattler)
I am not so sure about IsPointed in general however. When I was defining homotopy groups, I couldn't define iterated loops using IsPointed because the typeclass resolution wasn't clever enough to see that the correct basepoint was being mentioned.
Do you have a concrete example? I might be able to [help you] fix it.
Even the definition of iterated loops is problematic, is there some sort of where statement I can generate an instance with an fixpoint?
Require Import Basics.
Definition loops (A : Type) `{a : IsPointed A} := a = a.
Global Instance ispointed_loops (A : Type) `{a : IsPointed A}
: IsPointed (loops A) := 1%path.
Fixpoint iter_loops (n : nat) (A : Type) `{a : IsPointed A}
:= match n with
| O => A
| S m => loops (iter_loops m A)
end.
If you can get this to work we should be able to prove the following:
Lemma unfold_loops (n : nat) (A : Type) `{a : IsPointed A}
: iter_loops n.+1 A = iter_loops n (loops A).
I see
Coercion pointed_fun (A B : pType) : pMap A B -> A -> B
...
(* Coercion pointed_fun : pMap >-> Funclass. *)
which doesn't look to me as though you are actually coercing into Funclass. Unless Coq has some magic I'm not aware of where by a coercion whose target is a function type is automatically treated as a coercion into Funclass?
@mikeshulman If I haven't misunderstood, there is a variant here which says you can declare a coercion like a definition, and it magically puts it in the right class. Which I am guessing for functions is easy enough.
Hmm. Did you try explicitly putting it in Funclass and see whether that makes any difference? If I had problems with your definition I would suspect that that variant only applies to user-defined classes. Note that the class Funclass is different from a user-defined class that happens to be a function type. In particular, I believe that in order to type an application f x, Coq has to be able to coerce f into Funclass, which is different from coercing it into a user-defined class that happens to be a function type.
Do you mean like this?
(* A pointed map is a map with a proof that it preserves the point *)
Record pMap' (A B : pType) := {
pointed_fun' : A -> B ;
point_eq' : pointed_fun' (point A) = point B
}.
(* We use pMap' to arrive at a version of pMap which is itself a pType *)
Definition pMap (A B : pType) : pType
:= Build_pType (pMap' A B) (Build_pMap' _ _ (const (point B)) 1).
Definition Build_pMap (A B : pType) (f : A -> B)
: f (point A) = point B -> pMap A B := Build_pMap' A B f.
Definition pointed_fun (A B : pType) : pMap A B -> A -> B := pointed_fun' A B.
Coercion pointed_fun : pMap >-> Funclass.
because this gives me the following error:
Cannot recognize pMap as a source class of pointed_fun.
You should be able to do
Fixpoint is_pointed_iter_loops {n : nat} {A : Type} {a : IsPointed A} : IsPointed (iter_loops n A)
:= ...
and then do
Existing Instance is_pointed_iter_loops.
@JasonGross But the definition of iter_loops requires it to be already pointed. The definition of iter_loops I gave doesn't actually work.
You can define a helper fixpoint which builds the sigma type and then define the projections out of it?
@JasonGross Do you mean package everything together and then project out of it? This is exactly what we are doing at the moment. iterated_loops is exactly the kind of situation where have instances of IsPointed floating around doesn't cut it.
Ah, maybe the problem is that pMap is not itself a type, hence not a "class"? I'm getting out of my depth here. I do notice that your
Coercion pointed_fun (A B : pType) : pMap A B -> A -> B := pointed_fun' A B.
is warned as not respecting the "uniform inheritance condition", which IIRC may mean that it isn't actually doing anything.
@mikeshulman Yes, I agree that it probably isn't doing anything. I don't know much about coercions apart from what I have inferred. There isn't much documentation on them either (at least that I could find).
This awkwardness makes me more inclined to keep everything packaged up in pType. I do feel like there must be a better solution that we are not seeing however.
Ah, maybe the problem is that pMap is not itself a type, hence not a "class"? I'm getting out of my depth here. I do notice that your
Coercion pointed_fun (A B : pType) : pMap A B -> A -> B := pointed_fun' A B.is warned as not respecting the "uniform inheritance condition", which IIRC may mean that it isn't actually doing anything.
This is all correct. You can, however, make pointed_fun' a coercion via Coercion pointed_fun' : pMap' >-> Funclass. and everything will work just fine.
@JasonGross Do you mean package everything together and then project out of it? This is exactly what we are doing at the moment. iterated_loops is exactly the kind of situation where have instances of IsPointed floating around doesn't cut it.
Ah, yes, I see now. I agree that you want pType for this. Note, however, that this works fine:
Require Import Basics.
Definition loops (A : Type) `{a : IsPointed A} := a = a.
Global Instance ispointed_loops (A : Type) `{a : IsPointed A}
: IsPointed (loops A) := 1%path.
Fixpoint iter_loops (n : nat) (A : Type) `{a : IsPointed A}
:= match n with
| O => Build_pType A _
| S m => Build_pType (loops (iter_loops m A)) _
end.
@JasonGross That definition was the one we had before I wrote the homotopy group file. At the time I had much difficulty proving the inner unfold lemma
Lemma unfold_loops (n : nat) (A : Type) `{a : IsPointed A}
: iter_loops n.+1 A = iter_loops n (loops A).
using the definition you just gave. That is why I changed it fully to pTypes. Here is what I mean:
Require Import Basics.
Definition loops (A : Type) `{a : IsPointed A} := a = a.
Global Instance ispointed_loops (A : Type) `{a : IsPointed A}
: IsPointed (loops A) := 1%path.
Fixpoint iter_loops (n : nat) (A : Type) `{a : IsPointed A}
:= match n with
| O => Build_pType A _
| S m => Build_pType (loops (iter_loops m A)) _
end.
Lemma unfold_loops (n : nat) (A : Type) `{a : IsPointed A}
: iter_loops n.+1 A = iter_loops n (loops A).
Proof.
induction n.
1: reflexivity.
apply ap. (* This ought to work but doesn't *)
exact IHn.
Defined.
Ah, I see. Yes, if you do not change it fully to pType, then you pay the cost of crossing the abstraction barrier between the bundled and unbundled versions in many places, and it is quite painful if done wrong.
Note, however, that this works:
Lemma unfold_loops (n : nat) (A : Type) `{a : IsPointed A}
: iter_loops n.+1 A = iter_loops n (loops A).
Proof.
induction n.
1: reflexivity.
refine (ap (fun T : pType => Build_pType (loops T) _) IHn).
Defined.
You can, however, make
pointed_fun'a coercion viaCoercion pointed_fun' : pMap' >-> Funclass.and everything will work just fine.
Right, that's the solution, thanks. Does that solve the problem Ali?
@mikeshulman Yes this seems to solve the problem. I will see if I can get it to work with the rest of the library today.
As it seems like this is working I want to also see if we can push it further. My next proposal would be turning pMap into a class, say IsPointedMap so that we can do away with seperate compositions. i.e. there ought to be an instance ispointedmap_compose which detects the composition of pointed maps g o f as a pointed map.
I'm closing this issue as it doesn't seem to be entirely that useful in practice. These days we have nicer ways of pointifying a type by writing [X, pt] for X which is easy to write and quite readable. Also, choosing a basepoint is actually quite important even if in the majority of cases it is trivial. Therefore I don't see a good enough reason for Coq to be doing this for us.