Stream: Coq users

Topic: Dict of typeclass record


view this post on Zulip 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?

view this post on Zulip Li-yao (Jan 31 2022 at 02:59):

Sure, you can use @myproj to make the arguments of the projection explicit.

view this post on Zulip Callan McGill (Jan 31 2022 at 03:00):

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

view this post on Zulip 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)).

view this post on Zulip Callan McGill (Jan 31 2022 at 03:04):

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.

view this post on Zulip Li-yao (Jan 31 2022 at 03:04):

I think you want @contr

view this post on Zulip Callan McGill (Jan 31 2022 at 03:05):

ah perfect, thank you!


Last updated: Feb 09 2023 at 00:03 UTC