I am trying to prove something about monoids an categories. This results in the following (partial) proof:

Require Import UniMath.Algebra.Monoids.
Require Import UniMath.CategoryTheory.Core.Categories.

Unset Universe Checking.

Theorem exercise18 (M: monoid) : category.
    destruct M as [[[M misaset] mul] [assoc [e [lunit runit]]]].

    use makecategory.
        exact M.
        exact (λ x z, (hfiber (λ y: M, (mul x y)) z)).
            apply (isaset_hfiber _ _ misaset misaset).
            intros x.
            refine (e ,, (runit x)).
            intros x y z [f hf] [g hg].
            refine ((mul f g) ,, _).
            rewrite <- assoc, <- hg, <- hf.
            intros x y [f hf].
            assert (heq: mul e f = f).
                {exact (lunit f). }
            rewrite heq.

At the end, the goal is

mul e f,,
internal_paths_rew M (mul (mul x e) f) (λ p : M, p = y)
  (internal_paths_rew M (mul x f) (λ z : M, mul (mul x e) f = z)
     (internal_paths_rew M (mul x e)
        (λ y0 : M, mul (mul x e) f = mul y0 f)
        (idpath (mul (mul x e) f)) x (runit x)) y hf)
  (mul x (mul e f)) (assoc x e f) = f,, hf

Which leads me to ask a couple of questions (tell me if I should ask them separately):

  • Is there a tactic which turns a goal about equality of a record type (such as tpair, with notation _ ,, _) into a set of goals, one for each property of the record? Or is there another nice way to show equality?
  • What is the internal_paths_rew here?
  • The last line, rewrite heq gives an elaborate error:
Abstracting over the term "mul e f" leads to a term
λ p : M,, misaset,
internal_paths_rew M (mul (mul x e) f) (λ p0 : M, p0 = y)
  (internal_paths_rew M (mul x f) (λ z : M, mul (mul x e) f = z)
     (internal_paths_rew M (mul x e)
        (λ y0 : M, mul (mul x e) f = mul y0 f)
        (idpath (mul (mul x e) f)) x (runit x)) y hf) 
  (mul x p) (assoc x e f) = f,, hf
which is ill-typed.
Reason is: Illegal application: 
The term "internal_paths_rew" of type
 "∏ (A : UU) (a : A) (P : A → Type), P a → ∏ y : A, a = y → P y"
cannot be applied to the terms
 "M" : "UU"
 "mul (mul x e) f" : "pr1hSet (M,, misaset)"
 "λ p : M, p = y" : "M → UU"
 "internal_paths_rew M (mul x f) (λ z : M, mul (mul x e) f = z)
    (internal_paths_rew M (mul x e)
       (λ y : M, mul (mul x e) f = mul y f)
       (idpath (mul (mul x e) f)) x (runit x)) y hf"
   : "mul (mul x e) f = y"
 "mul x p" : "pr1hSet (M,, misaset)"
 "assoc x e f"
   : "(x * e * f)%multmonoid = (x * (e * f))%multmonoid"
The 6th term has type
 "(x * e * f)%multmonoid = (x * (e * f))%multmonoid"
which should be coercible to "mul (mul x e) f = mul x p".

What is happening here? I would expect I'd be able to perform arbitrary rewrites based on equality.

  • $\begingroup$ First internal_paths_rew appeared because you used rewrite, and notice how you have not yet used misasset. Where would you use that if you did the proof on paper? $\endgroup$ Apr 25, 2022 at 17:44
  • $\begingroup$ I used misaset as an argument for isaset_hfiber, to prove that my hom-sets are sets, right? $\endgroup$ Apr 25, 2022 at 20:56
  • $\begingroup$ And what does internal_paths_rew mean? $\endgroup$ Apr 25, 2022 at 20:57
  • $\begingroup$ I don't know what it means, someone like Pierre-Marie would. It's the proof term that is constructed by the rewrite tactic. $\endgroup$ Apr 26, 2022 at 6:28


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.