Email Gateway (Nov 04 2023 at 17:19): Email Gateway (Nov 04 2023 at 17:19):From: Roland Lutz <rlutz@hedmen.org>
Hi,
I ran into a problem when trying to define monomorphisms and epimorphisms:
definition monomorphism :: "('a ⇒ 'b) ⇒ bool" where
"monomorphism f ⟷ (∀ g g' :: ('c ⇒ 'a). f ∘ g = f ∘ g' ⟶ g = g')"
definition epimorphism :: "('a ⇒ 'b) ⇒ bool" where
"epimorphism f ⟷ (∀ h h' :: ('b ⇒ 'd). h ∘ f = h' ∘ f ⟶ h = h')"
(* Additional type variable(s) in specification of "monomorphism": 'c *)
(* Additional type variable(s) in specification of "epimorphism": 'd *)
A bit of googling led me to [0], which seems to suggest adding a dummy
parameter. I don't think this is what I want here, though, since the
extra type variable is supposed to be part of the all-quantifier as
opposed to being specified for each use of the definition.
How would I have to put these definitions to express the notion of a
monomorphism and an epimorphism, respectively?
Roland
[0] https://mailman46.in.tum.de/pipermail/isabelle-dev/2010-December/009676.html
Email Gateway (Nov 05 2023 at 21:56):From: Andrei Popescu <andrei.h.popescu@gmail.com>
Dear Roland,
I am afraid you bumped into a limitation of HOL. The best you can do
in HOL is express a weaker, "local" notion, and prove that it implies
the correct notion (which also means it is equivalent to the correct
notion). For monomorphisms, one option would be:
definition monomorphism :: "('a ⇒ 'b) ⇒ bool" where
"monomorphism f ⟷ (∀ g g' :: ('a ⇒ 'a). f o g = f o g' ⟶ g = g')"
lemma monomorphism_correct:
fixes g g' :: "'c ⇒ 'a"
assumes "monomorphism f" and "f o g = f o g'"
shows "g = g'"
proof(rule ext)
fix c
have "f o (g o (λ_::'a. c)) = f o (g' o (λ_::'a. c))"
using assms(2) unfolding fun_eq_iff by auto
from assms(1)[unfolded monomorphism_def, rule_format, OF this]
show "g c = g' c" unfolding fun_eq_iff by auto
qed
And similarly for epimorphisms. Of course, in this particular case you
can alternatively explore the connection between these notions and
injectivity / surjectivity, but the above is a more general recipe
that works for many other concepts: You start with a more local
version of the definition in HOL, and from it you prove the global
version which is not directly expressible as a definition.
An orthogonal caveat: Unlike sets in the usual category of sets, HOL
types are nonempty -- and this affects such category-theoretic
notions.
Best wishes,
Andrei
Email Gateway (Nov 06 2023 at 11:51):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Roland, I took a look at these.
As given, they require explicit quantification over type variables, which we don't have.
Note that the first one is actually provable using the already existing predicate “inj”.
lemma "inj f ⟷ (∀ g g' :: ('c ⇒ 'a). f ∘ g = f ∘ g' ⟶ g = g')"
by (force simp: inj_on_def fun_eq_iff)
On the other hand, the dual result is not provable because the implicit quantification over type variables is in the wrong place (as it also is for the first example):
lemma "surj f ⟷ (∀ h h' :: ('b ⇒ 'd). h ∘ f = h' ∘ f ⟶ h = h')"
That is to say, implicitly the type variable ‘d has global scope when you want its scope to be confined to the right hand side. This lemma fails if ‘d denotes a type having a single element.
In short, this sort of thing cannot work. What you should try instead depends on your overall aims.
Larry
Email Gateway (Nov 08 2023 at 21:47):From: Roland Lutz <rlutz@hedmen.org>
Thank you for your kind answers!
Do I understand it correctly that “if for any type 'a and term x :: <type
depending on 'a>, P x holds, then …” is a concept that can't be expressed
in HOL, similar to how FOL can't express some concepts HOL can and as
opposed to a technical limitation in Isabelle? What would be a good place
to read up on this kind of thing?
Roland
Email Gateway (Nov 09 2023 at 08:19):From: Tjark Weber <tjark.weber@it.uu.se>
Roland,
Others may suggest more appropriate references, but probably
https://en.wikipedia.org/wiki/Parametric_polymorphism#Rank-1_(predicative)_polymorphism
would not be a bad place to start.
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Last updated: Apr 29 2024 at 01:08 UTC