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?

Sure, you can use `@myproj`

to make the arguments of the projection explicit.

could you possibly give an example, I was trying this but failing badly

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.

I think you want `@contr`

ah perfect, thank you!

Last updated: Oct 05 2023 at 02:01 UTC