I am getting an error which I don't know how to interpret.

```
Error:
The term
"{|
morphism_isomorphic := associator_nat_trans;
isisomorphism_isomorphic := associator_is_iso
|}" has type
"(right_assoc@{Top.AugmentedSimplexCategoryMonoidalStructure.17454
Top.AugmentedSimplexCategoryMonoidalStructure.17455
Top.AugmentedSimplexCategoryMonoidalStructure.17452
Top.AugmentedSimplexCategoryMonoidalStructure.17456
Top.AugmentedSimplexCategoryMonoidalStructure.17457
Top.AugmentedSimplexCategoryMonoidalStructure.17458
Top.AugmentedSimplexCategoryMonoidalStructure.17459
Top.AugmentedSimplexCategoryMonoidalStructure.17460
Top.AugmentedSimplexCategoryMonoidalStructure.17461}
tensor@{Top.AugmentedSimplexCategoryMonoidalStructure.17454
Top.AugmentedSimplexCategoryMonoidalStructure.17455
....
while it is expected to have type
"(right_assoc@{Top.AugmentedSimplexCategoryMonoidalStructure.16875
Top.AugmentedSimplexCategoryMonoidalStructure.16876
Top.AugmentedSimplexCategoryMonoidalStructure.16877
Top.AugmentedSimplexCategoryMonoidalStructure.16879
Top.AugmentedSimplexCategoryMonoidalStructure.16880
Top.AugmentedSimplexCategoryMonoidalStructure.16881
Top.AugmentedSimplexCategoryMonoidalStructure.16882
Top.AugmentedSimplexCategoryMonoidalStructure.16883
Top.AugmentedSimplexCategoryMonoidalStructure.16884}
tensor@{Top.AugmentedSimplexCategoryMonoidalStructure.16875
Top.AugmentedSimplexCategoryMonoidalStructure.16876
Top.AugmentedSimplexCategoryMonoidalStructure.16875
...
```

Where should I start with tracking down the source of this error

I don't know if it's really a universe error or if the error is somewhere else and is just obscured by the massive wall of universes.

Is there a flag i can enable which would suppress all these universes so i can see what else is going on

Universes are hidden by default — you must use `Set Printing Universes`

to show them. (IIRC, `Set Printing All`

does not show them). In Coqide/VSCode/..., you need the corresponding "Display" commands.

Let me assume you have _not_ set some fancy option. Then AFAIK Coq only shows universes if they're relevant.

I see, ok, thank you

Re troubleshooting, I'm fairly clueless on universes but some starting points:

- any change you have a partially applied inductive somewhere? They're a well-known cause of unwarranted universe inconsistencies. IIUC, already this is bad:

```
Definition f : Type -> Type = option.
```

replace with

```
Definition f : Type -> Type = fun x => option x.
```

- are you mechanizing some large category or such, where you'd expect challenges with universes?
- http://adam.chlipala.net/cpdt/html/Cpdt.Universes.html could be helpful reading.

(I have not seen material on universes in Software Foundations)

Thank you. I turned on `Set Printing All`

and it simplified the message a lot and cleared away the universes

The matter was context dependencies

Patrick Nicodemus has marked this topic as resolved.

the type mismatch came from the fact that the term and the type were both borrowing an assumption declared as a context (an instance of a typeclass) but they were two different assumptions declared in two different files.

Last updated: Jun 20 2024 at 13:02 UTC