search

UniMath / UniMath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
http://unimath.org/
Other
954 stars 174 forks source link

ambiguous coercions #1044

Open DanGrayson opened 5 years ago

DanGrayson commented 5 years ago

I'm beginning to suspect that having multiple coercion paths between two classes is a bad idea, for making proofs easily. Does anyone else think so?

Here is what's bugging me today:

         (precategory_data_from_precategory
-            (category_to_precategory
-               (categoryWithAbgrops_category
                  (PreAdditive_categoryWithAbgrops M))))

         (precategory_data_from_precategory
-            (precategoryWithBinOps_precategory
-               (categoryWithAbgrops_precategoryWithBinOps
                  (PreAdditive_categoryWithAbgrops M))))

The notion of "precategory with binary operations on each Hom(A,B)" should be removed so we can avoid this.

DanGrayson commented 5 years ago

If we got rid of precategoryWithBinOps, we could probably also get rid of this silly rewriting rule:

Lemma rewrite_op {A:PreAdditive} (x y:A) :
  @to_binop (categoryWithAbgrops_precategoryWithBinOps (PreAdditive_categoryWithAbgrops A)) x y
  =
  @op (pr1monoid (grtomonoid (abgrtogr (@to_abgr (PreAdditive_categoryWithAbgrops A) x y)))).
Proof.
  reflexivity.
Defined.
benediktahrens commented 5 years ago

On 12/11/2018 14:04, Daniel R. Grayson wrote:

If we got rid of |precategoryWithBinOps|, we could probably also get rid of this silly rewriting rule:

|Lemma rewrite_op {A:PreAdditive} (x y:A) : @to_binop (categoryWithAbgrops_precategoryWithBinOps (PreAdditive_categoryWithAbgrops A)) x y = @op (pr1monoid (grtomonoid (abgrtogr (@to_abgr (PreAdditive_categoryWithAbgrops A) x y)))). Proof. reflexivity. Defined. |

Sounds good!

langston-barrett commented 5 years ago

I agree that it is generally a bad idea to have multiple coercion paths. Perhaps there is a way that we can get Coq to throw an error (or at least a warning) when this occurs?

DanGrayson commented 5 years ago

Loading the global All.v file does produce plenty of warning messages:

[Loading ML file ltac_plugin.cmxs ...
Ambiguous paths:
[hProp_to_hSet; pr1hSet] : hProp >-> Preamble.UU
[@negProp_to_hProp; hProp_to_hSet; pr1hSet] : PartB.negProp >-> Preamble.UU
Ambiguous paths: [@setquottouu0] : setquot >-> Sortclass
Ambiguous paths:
[weqtoincl; pr1incl] : weq >-> Funclass
[@posetUnderlyingEquivalence; weqtoincl; pr1incl] : PosetEquivalence >-> Funclass
Ambiguous paths: [@negProp_to_type] : negProp >-> UU
Ambiguous paths:
[underlyingFiniteSet; FiniteSet_to_hSet; pr1hSet] : FiniteOrderedSet >-> UU
[underlyingFiniteSet; FiniteSet_to_hSet; pr1hSet; fromUUtoType] : FiniteOrderedSet >-> Sortclass
[underlyingFiniteSet; FiniteSet_to_hSet] : FiniteOrderedSet >-> hSet
Ambiguous paths:
[@sequenceToUnorderedSequence; @unorderedSequenceToFunction] : Sequence >-> Funclass
Ambiguous paths:
[@NonemptySequenceToSequence; @sequenceToFunction] : NonemptySequence >-> Funclass
Ambiguous paths: [isabgroptoisabmonoidop; pr1isabmonoidop] : isabgrop >-> ismonoidop
Ambiguous paths: [iscommringopstoiscommrigops; pr1iscommrigops] : iscommringops >-> isrigops
Ambiguous paths: [binopincltobinopfun; pr1binopfun] : binopmono >-> Funclass
Ambiguous paths:
[binopisotobinopmono; pr1binopmono] : binopiso >-> incl
[binopisotobinopmono; pr1binopmono; pr1incl] : binopiso >-> Funclass
Ambiguous paths:
[@carrierofasubsetwithbinop; pr1setwithbinop; pr1hSet; fromUUtoType] : subsetswithbinop >-> Sortclass
Ambiguous paths: [twobinopincltotwobinopfun; pr1twobinopfun] : twobinopmono >-> Funclass
Ambiguous paths:
[twobinopisototwobinopmono; pr1twobinopmono] : twobinopiso >-> incl
[twobinopisototwobinopmono; pr1twobinopmono; pr1incl] : twobinopiso >-> Funclass
Ambiguous paths:
[@carrierofsubsetwith2binop; pr1setwith2binop; pr1hSet; fromUUtoType] : subsetswith2binop >-> Sortclass
Ambiguous paths:
[monoidincltomonoidfun; monoidfuntobinopfun; pr1binopfun] : monoidmono >-> Funclass
Ambiguous paths:
[monoidmonotobinopmono; binopincltobinopfun] : monoidmono >-> binopfun
[monoidmonotobinopmono; pr1binopmono] : monoidmono >-> incl
[monoidmonotobinopmono; pr1binopmono; pr1incl] : monoidmono >-> Funclass
Ambiguous paths:
[monoidisotomonoidmono; pr1monoidmono] : monoidiso >-> incl
[monoidisotomonoidmono; pr1monoidmono; pr1incl] : monoidiso >-> Funclass
Ambiguous paths:
[monoidisotobinopiso; binopisotobinopmono] : monoidiso >-> binopmono
[monoidisotobinopiso; binopisotobinopmono; binopincltobinopfun] : monoidiso >-> binopfun
[monoidisotobinopiso; pr1binopiso; weqtoincl] : monoidiso >-> incl
[monoidisotobinopiso; pr1binopiso] : monoidiso >-> weq
[monoidisotobinopiso; pr1binopiso; @pr1weq] : monoidiso >-> Funclass
Ambiguous paths:
[@carrierofsubmonoid; pr1monoid] : submonoid >-> setwithbinop
[@carrierofsubmonoid; pr1monoid; pr1setwithbinop] : submonoid >-> hSet
[@carrierofsubmonoid; pr1monoid; pr1setwithbinop; pr1hSet] : submonoid >-> UU
[@carrierofsubmonoid; pr1monoid; pr1setwithbinop; pr1hSet; fromUUtoType] : submonoid >-> Sortclass
Ambiguous paths:
[@carrierofsubabmonoid; abmonoidtomonoid] : subabmonoid >-> monoid
[@carrierofsubabmonoid; abmonoidtomonoid; pr1monoid] : subabmonoid >-> setwithbinop
[@carrierofsubabmonoid; abmonoidtomonoid; pr1monoid; pr1setwithbinop] : subabmonoid >-> hSet
[@carrierofsubabmonoid; abmonoidtomonoid; pr1monoid; pr1setwithbinop; pr1hSet] : subabmonoid >-> UU
[@carrierofsubabmonoid; abmonoidtomonoid; pr1monoid; pr1setwithbinop; pr1hSet; fromUUtoType] : subabmonoid >-> Sortclass
Ambiguous paths:
[@carrierofasubgr; grtomonoid] : subgr >-> monoid
[@carrierofasubgr; grtomonoid; pr1monoid] : subgr >-> setwithbinop
[@carrierofasubgr; grtomonoid; pr1monoid; pr1setwithbinop] : subgr >-> hSet
[@carrierofasubgr; grtomonoid; pr1monoid; pr1setwithbinop; pr1hSet] : subgr >-> UU
[@carrierofasubgr; grtomonoid; pr1monoid; pr1setwithbinop; pr1hSet; fromUUtoType] : subgr >-> Sortclass
Ambiguous paths:
[abgrtoabmonoid; abmonoidtomonoid] : abgr >-> monoid
[abgrtoabmonoid; abmonoidtomonoid; pr1monoid] : abgr >-> setwithbinop
[abgrtoabmonoid; abmonoidtomonoid; pr1monoid; pr1setwithbinop] : abgr >-> hSet
[abgrtoabmonoid; abmonoidtomonoid; pr1monoid; pr1setwithbinop; pr1hSet] : abgr >-> UU
[abgrtoabmonoid; abmonoidtomonoid; pr1monoid; pr1setwithbinop; pr1hSet; fromUUtoType] : abgr >-> Sortclass
Ambiguous paths:
[@carrierofasubabgr; abgrtogr] : subabgr >-> gr
[@carrierofasubabgr; abgrtogr; grtomonoid] : subabgr >-> monoid
[@carrierofasubabgr; abgrtogr; grtomonoid; pr1monoid] : subabgr >-> setwithbinop
[@carrierofasubabgr; abgrtogr; grtomonoid; pr1monoid; pr1setwithbinop] : subabgr >-> hSet
[@carrierofasubabgr; abgrtogr; grtomonoid; pr1monoid; pr1setwithbinop; pr1hSet] : subabgr >-> UU
[@carrierofasubabgr; abgrtogr; grtomonoid; pr1monoid; pr1setwithbinop; pr1hSet; fromUUtoType] : subabgr >-> Sortclass
Ambiguous paths:
[carrierofasubrig; pr1rig] : subrig >-> setwith2binop
[carrierofasubrig; pr1rig; pr1setwith2binop] : subrig >-> hSet
[carrierofasubrig; pr1rig; pr1setwith2binop; pr1hSet] : subrig >-> UU
[carrierofasubrig; pr1rig; pr1setwith2binop; pr1hSet; fromUUtoType] : subrig >-> Sortclass
Ambiguous paths:
[ConstructiveField_ConstructiveCommutativeDivisionRig;
 ConstructiveCommutativeDivisionRig_commrig; commrigtorig; pr1rig] : ConstructiveField >-> setwith2binop
[ConstructiveField_ConstructiveCommutativeDivisionRig;
 ConstructiveCommutativeDivisionRig_commrig; commrigtorig; pr1rig; pr1setwith2binop] : ConstructiveField >-> hSet
[ConstructiveField_ConstructiveCommutativeDivisionRig;
 ConstructiveCommutativeDivisionRig_commrig; commrigtorig; pr1rig; pr1setwith2binop; pr1hSet] : ConstructiveField >-> UU
[ConstructiveField_ConstructiveCommutativeDivisionRig;
 ConstructiveCommutativeDivisionRig_commrig; commrigtorig; pr1rig; pr1setwith2binop; pr1hSet;
 fromUUtoType] : ConstructiveField >-> Sortclass
[ConstructiveField_ConstructiveCommutativeDivisionRig;
 ConstructiveCommutativeDivisionRig_commrig; commrigtorig] : ConstructiveField >-> rig
[ConstructiveCommutativeDivisionRig_commrig; commrigtorig; pr1rig] : ConstructiveCommutativeDivisionRig >-> setwith2binop
[ConstructiveCommutativeDivisionRig_commrig; commrigtorig; pr1rig; pr1setwith2binop] : ConstructiveCommutativeDivisionRig >-> hSet
[ConstructiveCommutativeDivisionRig_commrig; commrigtorig; pr1rig; pr1setwith2binop; pr1hSet] : ConstructiveCommutativeDivisionRig >-> UU
[ConstructiveCommutativeDivisionRig_commrig; commrigtorig; pr1rig; pr1setwith2binop; pr1hSet;
 fromUUtoType] : ConstructiveCommutativeDivisionRig >-> Sortclass
[ConstructiveCommutativeDivisionRig_commrig; commrigtorig] : ConstructiveCommutativeDivisionRig >-> rig
Ambiguous paths:
[ringaddabgr; abgrtogr; grtomonoid; pr1monoid; pr1setwithbinop] : ring >-> hSet
[ringaddabgr; abgrtogr; grtomonoid; pr1monoid; pr1setwithbinop; pr1hSet] : ring >-> UU
[ringaddabgr; abgrtogr; grtomonoid; pr1monoid; pr1setwithbinop; pr1hSet; fromUUtoType] : ring >-> Sortclass
Ambiguous paths:
[ringtorig; pr1rig] : ring >-> setwith2binop
[ringtorig; pr1rig; pr1setwith2binop] : ring >-> hSet
[ringtorig; pr1rig; pr1setwith2binop; pr1hSet] : ring >-> UU
[ringtorig; pr1rig; pr1setwith2binop; pr1hSet; fromUUtoType] : ring >-> Sortclass
Ambiguous paths:
[carrierofasubring; pr1ring] : subring >-> setwith2binop
[carrierofasubring; pr1ring; pr1setwith2binop] : subring >-> hSet
[carrierofasubring; pr1ring; pr1setwith2binop; pr1hSet] : subring >-> UU
[carrierofasubring; pr1ring; pr1setwith2binop; pr1hSet; fromUUtoType] : subring >-> Sortclass
Ambiguous paths:
[ConstructiveField_commring; commringtoring; pr1ring] : ConstructiveField >-> setwith2binop
[ConstructiveField_commring; commringtoring; ringtorig] : ConstructiveField >-> rig
[ConstructiveField_commring; commringtoring; pr1ring; pr1setwith2binop] : ConstructiveField >-> hSet
[ConstructiveField_commring; commringtoring; pr1ring; pr1setwith2binop; pr1hSet] : ConstructiveField >-> UU
[ConstructiveField_commring; commringtoring; pr1ring; pr1setwith2binop; pr1hSet; fromUUtoType] : ConstructiveField >-> Sortclass
Ambiguous paths:
[ConstructiveField_commring; commringtocommrig; commrigtorig; pr1rig] : ConstructiveField >-> setwith2binop
[ConstructiveField_commring; commringtocommrig; commrigtorig] : ConstructiveField >-> rig
[ConstructiveField_commring; commringtocommrig; commrigtorig; pr1rig; pr1setwith2binop] : ConstructiveField >-> hSet
[ConstructiveField_commring; commringtocommrig; commrigtorig; pr1rig; pr1setwith2binop; pr1hSet] : ConstructiveField >-> UU
[ConstructiveField_commring; commringtocommrig; commrigtorig; pr1rig; pr1setwith2binop;
 pr1hSet; fromUUtoType] : ConstructiveField >-> Sortclass
[ConstructiveField_commring; commringtocommrig] : ConstructiveField >-> commrig
[commringtocommrig; commrigtorig; pr1rig] : commring >-> setwith2binop
[commringtocommrig; commrigtorig] : commring >-> rig
[commringtocommrig; commrigtorig; pr1rig; pr1setwith2binop] : commring >-> hSet
[commringtocommrig; commrigtorig; pr1rig; pr1setwith2binop; pr1hSet] : commring >-> UU
[commringtocommrig; commrigtorig; pr1rig; pr1setwith2binop; pr1hSet; fromUUtoType] : commring >-> Sortclass
[fldtointdom; pr1intdom; commringtocommrig; commrigtorig; pr1rig] : fld >-> setwith2binop
[fldtointdom; pr1intdom; commringtocommrig; commrigtorig] : fld >-> rig
[fldtointdom; pr1intdom; commringtocommrig; commrigtorig; pr1rig; pr1setwith2binop] : fld >-> hSet
[fldtointdom; pr1intdom; commringtocommrig; commrigtorig; pr1rig; pr1setwith2binop; pr1hSet] : fld >-> UU
[fldtointdom; pr1intdom; commringtocommrig; commrigtorig; pr1rig; pr1setwith2binop; pr1hSet;
 fromUUtoType] : fld >-> Sortclass
[pr1intdom; commringtocommrig; commrigtorig; pr1rig] : intdom >-> setwith2binop
[pr1intdom; commringtocommrig; commrigtorig] : intdom >-> rig
[pr1intdom; commringtocommrig; commrigtorig; pr1rig; pr1setwith2binop] : intdom >-> hSet
[pr1intdom; commringtocommrig; commrigtorig; pr1rig; pr1setwith2binop; pr1hSet] : intdom >-> UU
[pr1intdom; commringtocommrig; commrigtorig; pr1rig; pr1setwith2binop; pr1hSet; fromUUtoType] : intdom >-> Sortclass
Ambiguous paths:
[@binophrelmodule_eqrel; pr1binopeqrel] : module_eqrel >-> eqrel
[@binophrelmodule_eqrel; pr1binopeqrel; pr1eqrel] : module_eqrel >-> Funclass
Ambiguous paths:
[@carrierofasubmodule; @pr1module; abgrtogr] : submodule >-> gr
[@carrierofasubmodule; @pr1module; abgrtoabmonoid] : submodule >-> abmonoid
[@carrierofasubmodule; @pr1module; abgrtogr; grtomonoid] : submodule >-> monoid
[@carrierofasubmodule; @pr1module; abgrtogr; grtomonoid; pr1monoid] : submodule >-> setwithbinop
[@carrierofasubmodule; @pr1module; abgrtogr; grtomonoid; pr1monoid; pr1setwithbinop] : submodule >-> hSet
[@carrierofasubmodule; @pr1module; abgrtogr; grtomonoid; pr1monoid; pr1setwithbinop; pr1hSet] : submodule >-> UU
[@carrierofasubmodule; @pr1module; abgrtogr; grtomonoid; pr1monoid; pr1setwithbinop; pr1hSet;
 fromUUtoType] : submodule >-> Sortclass
[@carrierofasubmodule; @pr1module] : submodule >-> abgr
Ambiguous paths: [@moduleiso_to_modulefun; @pr1modulefun] : moduleiso >-> Funclass
Overwriting previous delimiting key cat in scope cat
Ambiguous paths:
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_groupoid; groupoid_to_category;
 category_to_precategory; precategory_data_from_precategory] : discrete_category >-> precategory_data
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_groupoid; groupoid_to_category;
 category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data] : discrete_category >-> precategory_ob_mor
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_groupoid; groupoid_to_category;
 category_to_precategory; graph_from_precategory] : discrete_category >-> graph
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_groupoid; groupoid_to_category;
 category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data; ob] : discrete_category >-> UU
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_groupoid; groupoid_to_category;
 category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data; ob; fromUUtoType] : discrete_category >-> Sortclass
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_groupoid; groupoid_to_category;
 category_to_precategory] : discrete_category >-> precategory
[univalent_groupoid_to_groupoid; groupoid_to_category; category_to_precategory;
 precategory_data_from_precategory] : univalent_groupoid >-> precategory_data
[univalent_groupoid_to_groupoid; groupoid_to_category; category_to_precategory;
 precategory_data_from_precategory; precategory_ob_mor_from_precategory_data] : univalent_groupoid >-> precategory_ob_mor
[univalent_groupoid_to_groupoid; groupoid_to_category; category_to_precategory;
 graph_from_precategory] : univalent_groupoid >-> graph
[univalent_groupoid_to_groupoid; groupoid_to_category; category_to_precategory;
 precategory_data_from_precategory; precategory_ob_mor_from_precategory_data; ob] : univalent_groupoid >-> UU
[univalent_groupoid_to_groupoid; groupoid_to_category; category_to_precategory;
 precategory_data_from_precategory; precategory_ob_mor_from_precategory_data; ob; fromUUtoType] : univalent_groupoid >-> Sortclass
[univalent_groupoid_to_groupoid; groupoid_to_category; category_to_precategory] : univalent_groupoid >-> precategory
[groupoid_to_category; category_to_precategory; precategory_data_from_precategory] : groupoid >-> precategory_data
[groupoid_to_category; category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data] : groupoid >-> precategory_ob_mor
[groupoid_to_category; category_to_precategory; graph_from_precategory] : groupoid >-> graph
[groupoid_to_category; category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data; ob] : groupoid >-> UU
[groupoid_to_category; category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data; ob; fromUUtoType] : groupoid >-> Sortclass
[groupoid_to_category; category_to_precategory] : groupoid >-> precategory
Ambiguous paths: [morphism_from_z_iso] : z_iso >-> precategory_morphisms
Ambiguous paths:
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_univalent_category;
 univalent_category_to_category; category_to_precategory; precategory_data_from_precategory] : discrete_category >-> precategory_data
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_univalent_category;
 univalent_category_to_category; category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data] : discrete_category >-> precategory_ob_mor
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_univalent_category;
 univalent_category_to_category; category_to_precategory; graph_from_precategory] : discrete_category >-> graph
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_univalent_category;
 univalent_category_to_category; category_to_precategory] : discrete_category >-> precategory
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_univalent_category;
 univalent_category_to_category; category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data; ob] : discrete_category >-> UU
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_univalent_category;
 univalent_category_to_category; category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data; ob; fromUUtoType] : discrete_category >-> Sortclass
[discrete_category_to_univalent_groupoid; univalent_groupoid_to_univalent_category;
 univalent_category_to_category] : discrete_category >-> category
[univalent_groupoid_to_univalent_category; univalent_category_to_category;
 category_to_precategory; precategory_data_from_precategory] : univalent_groupoid >-> precategory_data
[univalent_groupoid_to_univalent_category; univalent_category_to_category;
 category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data] : univalent_groupoid >-> precategory_ob_mor
[univalent_groupoid_to_univalent_category; univalent_category_to_category;
 category_to_precategory; graph_from_precategory] : univalent_groupoid >-> graph
[univalent_groupoid_to_univalent_category; univalent_category_to_category;
 category_to_precategory] : univalent_groupoid >-> precategory
[univalent_groupoid_to_univalent_category; univalent_category_to_category;
 category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data; ob] : univalent_groupoid >-> UU
[univalent_groupoid_to_univalent_category; univalent_category_to_category;
 category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data; ob; fromUUtoType] : univalent_groupoid >-> Sortclass
[univalent_groupoid_to_univalent_category; univalent_category_to_category] : univalent_groupoid >-> category
Ambiguous paths:
[categoryWithAbgrops_category; category_to_precategory; precategory_data_from_precategory] : categoryWithAbgrops >-> precategory_data
[categoryWithAbgrops_category; category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data] : categoryWithAbgrops >-> precategory_ob_mor
[categoryWithAbgrops_category; category_to_precategory; graph_from_precategory] : categoryWithAbgrops >-> graph
[categoryWithAbgrops_category; category_to_precategory] : categoryWithAbgrops >-> precategory
[categoryWithAbgrops_category; category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data; ob] : categoryWithAbgrops >-> UU
[categoryWithAbgrops_category; category_to_precategory; precategory_data_from_precategory;
 precategory_ob_mor_from_precategory_data; ob; fromUUtoType] : categoryWithAbgrops >-> Sortclass
Ambiguous paths:
[ShortExact_RightShortExact; RightShortExact_ShortShortExact] : ShortExact >-> ShortShortExact
[ShortExact_RightShortExact; RightShortExact_ShortShortExact;
 ShortShortExact_ShortShortExactData; ShortShortExactData_MorphismPair] : ShortExact >-> MorphismPair
[ShortExact_RightShortExact; RightShortExact_ShortShortExact;
 ShortShortExact_ShortShortExactData] : ShortExact >-> ShortShortExactData
Ambiguous paths:
[@are_adjoints_from_adjunction; @are_adjoints_to_is_left_adjoint;
 @adjunction_data_from_is_left_adjoint] : adjunction >-> adjunction_data
Ambiguous paths:
[@adjunction_of_right_adjoint_over_id_data; @left_adj_over_id] : right_adjoint_over_id_data >-> disp_functor
[@adjunction_of_right_adjoint_over_id_data; @left_adj_over_id;
 @disp_functor_data_from_disp_functor] : right_adjoint_over_id_data >-> disp_functor_data
[@adjunction_of_right_adjoint_over_id_data; @left_adj_over_id;
 @disp_functor_data_from_disp_functor; @disp_functor_on_objects] : right_adjoint_over_id_data >-> Funclass
Ambiguous paths:
[@equiv_of_is_equiv_over_id; @adjunction_of_equiv_over_id; @data_of_disp_adjunction_id] : is_equiv_over_id >-> disp_adjunction_id_data
[@equiv_of_is_equiv_over_id; @adjunction_of_equiv_over_id; @data_of_disp_adjunction_id;
 @left_adj_over_id] : is_equiv_over_id >-> disp_functor
[@equiv_of_is_equiv_over_id; @adjunction_of_equiv_over_id; @data_of_disp_adjunction_id;
 @left_adj_over_id; @disp_functor_data_from_disp_functor] : is_equiv_over_id >-> disp_functor_data
[@equiv_of_is_equiv_over_id; @adjunction_of_equiv_over_id; @data_of_disp_adjunction_id;
 @left_adj_over_id; @disp_functor_data_from_disp_functor; @disp_functor_on_objects] : is_equiv_over_id >-> Funclass
Ambiguous paths:
[@are_adjoints_from_adjunction; @are_adjoints_to_is_left_adjoint;
 @adjunction_data_from_is_left_adjoint] : adjunction >-> adjunction_data
Ambiguous paths:
[@adj_from_adj_equiv; @data_from_adjunction] : adj_equiv >-> adjunction_data
[@adj_from_adj_equiv; @are_adjoints_from_adjunction; @are_adjoints_to_is_left_adjoint] : adj_equiv >-> is_left_adjoint
Ambiguous paths:
[@equiv_from_adj_equiv; @adjunction_data_from_equivalence_of_precats] : adj_equiv >-> adjunction_data
Ambiguous paths:
[@equiv_of_is_equiv_over; @adjunction_of_equiv_over; data_of_disp_adjunction] : is_equiv_over >-> disp_adjunction_data
Ambiguous paths:
[@internal_equivalence_from_internal_adjoint_equivalence;
 @internal_adjunction_data_from_internal_equivalence; @interna_adjunction_over_from_data] : internal_adjoint_equivalence >-> internal_adjunction_over
[@internal_equivalence_from_internal_adjoint_equivalence;
 @internal_adjunction_data_from_internal_equivalence] : internal_adjoint_equivalence >-> internal_adjunction_data
Ambiguous paths:
[@internal_adjunction_from_internal_adjoint_equivalence;
 @internal_adjunction_data_from_internal_adjunction; @interna_adjunction_over_from_data] : internal_adjoint_equivalence >-> internal_adjunction_over
[@internal_adjunction_from_internal_adjoint_equivalence;
 @internal_adjunction_data_from_internal_adjunction] : internal_adjoint_equivalence >-> internal_adjunction_data