get rid of isgraph_arrow #1884
get rid of isgraph_arrow #1884
Conversation
| @@ -124,7 +124,7 @@ Defined. | |||
|
|
|||
| (* A group homomorphism consists of a map between groups and a proof that the map preserves the group operation. *) | |||
| Record GroupHomomorphism (G H : Group) := Build_GroupHomomorphism' { | |||
| grp_homo_map : G -> H; | |||
| grp_homo_map : group_type G -> group_type H; | |||
There was a problem hiding this comment.
I originally tried making this $-> but it messes with the coercions. I quickly tweaked it to be the underlying type instead, but it can be undone. I think it is better this way.
| @@ -238,7 +238,7 @@ Global Instance is01cat_cring : Is01Cat CRing | |||
| := Build_Is01Cat _ _ rng_homo_id (@rng_homo_compose). | |||
|
|
|||
| Global Instance is2graph_cring : Is2Graph CRing | |||
| := fun A B => isgraph_induced (@rng_homo_map A B). | |||
| := fun A B => isgraph_induced (@rng_homo_map A B : _ -> (cring_type A $-> _)). | |||
There was a problem hiding this comment.
I don't know why this worked but in Group.v I needed to introduce it everywhere for the induced parts.
| - nrapply isequiv_compose. | ||
| 1: apply isequiv_ap_equiv_fun. | ||
| exact (isequiv_Htpy_path (uncore A) (uncore B) f g). |
There was a problem hiding this comment.
| - nrapply isequiv_compose. | |
| 1: apply isequiv_ap_equiv_fun. | |
| exact (isequiv_Htpy_path (uncore A) (uncore B) f g). | |
| - rapply isequiv_compose. | |
| rapply isequiv_Htpy_path. |
There was a problem hiding this comment.
BTW, this whole result could be generalized and put into WildCat/Equiv.v, with the assumption that ap cate_fun is an equivalence. Then it could be used both here and for hasmorext_core_ptype.
There was a problem hiding this comment.
Doesn't look like this is even used anywhere, but I'll put a more general version next to the core stuff for completeness.
There was a problem hiding this comment.
I'm gonna leave this for another PR as I think I can make a few more improvements.
This instance is far too general and should be restricted to Universe.v where it is actually used. A few places in the library were picking this up. This can be fixed by changeing a -> to a $-> so that the correct instance is inferred. Signed-off-by: Ali Caglayan <[email protected]> <!-- ps-id: feda50b3-daa5-4e3b-8205-59704ea2b1db -->
Signed-off-by: Ali Caglayan <[email protected]> <!-- ps-id: a5fdb34c-094f-4e8d-bd37-85e1d9657cd1 -->
Alizter
force-pushed
the
ps/rr/get_rid_of_isgraph_arrow
branch
from
17675b6 to
47b62b7
Compare
|
I'll merge this when it is green. |
This instance is far too general and should be restricted to Universe.v where it is actually used. A few places in the library were picking this up. This can be fixed by changeing a -> to a $-> so that the correct instance is inferred.