Callan McGill (Jan 31 2022 at 02:52): Callan McGill (Jan 31 2022 at 02:52):I have a typeclass instance but it seems like resolution is not finding it. Is there any way for me to directly use projections on the instance definition?
Li-yao (Jan 31 2022 at 02:59):Sure, you can use @myproj to make the arguments of the projection explicit.
Callan McGill (Jan 31 2022 at 03:00):could you possibly give an example, I was trying this but failing badly
Callan McGill (Jan 31 2022 at 03:03):Here is what I am trying and failing to do:
Section based_path_induction.
Variable A : Type.
Variable a : A.
Definition based_path_space : Type :=
sig (fun x => a = x).
Definition
free_path_ind : forall (P : forall (x y : A) (p : x = y), Type)
(x y : A) (p : x = y) (p0 : P x x idpath), P x y p.
Proof.
intros P x y p p0. apply paths_ind. assumption.
Defined.
Instance pathspace_contr : Contr based_path_space.
Proof.
- refine (Build_Contr _ (a ; idpath) _).
* intros [x p].
exact (free_path_ind (fun a x p => (a; idpath) = (x; p)) a x p idpath).
Defined.
Definition based_path_ind (C : forall (x : A) (p : a = x), Type)
(c_refl : C a idpath) : forall (x : A) (p : a = x), C x p.
Proof.
apply equiv_sig_ind'. intros sg.
assert (H : (a ; idpath) = sg).
{ exact (contr @pathspace_contr (sg .1)).
This use of @pathspace_contr does not seem correct as it doesn't turn up in the error messages and the type is still printed as not unified.
Li-yao (Jan 31 2022 at 03:04):I think you want @contr
Callan McGill (Jan 31 2022 at 03:05):ah perfect, thank you!
Last updated: Oct 05 2023 at 02:01 UTC