PR summary 343350d6bf

Import changes for modified files

No significant changes to the import graph

Declarations diff

+ expTerminalNatIso
+ unitNatIso

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@dagurtomas and @adamtopaz this is the issue we discussed. I left this as a draft because of the questions (1) and (2) above.

For (1), it's because it uses conjugateIsoEquiv, which is noncomputable because it uses asIso which produces an isomorphism (containing the data of an inverse) just by knowing that a morphism has an inverse.

For (2), I would supply MonoidalClosed.unitNatIso with an arbitrary instance variable [Closed (𝟙_ C)] instead (which will be automatically inferred whenever your in a monoidal closed category anyway) instead of using the explicit unitClosed. Then do the same with Exponentiable in the cartesian one. See this branch (you can just merge that branch into this one if you'd like)

Regarding computability, note that CategoryTheory.Adjunction.natIsoEquiv is computable, so conjuagateIsoEquiv shouldn't need to be noncomputable.

These two APIs should really be merged at some point, see the TODO in the file Adjunction.Unique. I wrote that part of the uniqueness file without knowing I was duplicating API, then when I discovered it it turned out to be nontrivial to deduplicate

Thanks @dagurtomas. I would like to merge your branch with this one. How do I do this?

Thanks also for pointing out the issue with the way I defined natIsoEquiv. When I get a moment (sometime this week) I'll go back into mates and do that part of the TODO from the Adjunction.Unique file.

I would like to merge your branch with this one. How do I do this?

git checkout closedUnit 
git merge dagur/closedUnit

The idea of having [Exponentiable (⊤_ C)] as an argument rather than having it be inferred is, approximately, to ensure that the proof works given any proof that 1 is exponentiable. If this argument weren't given directly, then the proof would be for a particular choice of the exponential of 1. Of course any choice is naturally isomorphic to any other, but it's convenient to not need to add this isomorphism where necessary. Admittedly my docstring "The typeclass argument is explicit: any instance can be used." isn't particularly clear about this, although hopefully "any instance can be used" makes a little more sense now.
Thus I agree with Dagur's comments about (2). And as he says, since the argument is given in [] brackets, it's automatically inferred in any application anyway.

I would like to merge your branch with this one. How do I do this?

git checkout closedUnit 
git merge dagur/closedUnit

This returns the error merge: dagur/closedUnit - not something we can merge. I'm working from the command line on my computer in case this is relevant. I tried also running git fetch first but that didn't help.

But no need to reply. I just manually recreated your suggestions.

The idea of having [Exponentiable (⊤_ C)] as an argument rather than having it be inferred is, approximately, to ensure that the proof works given any proof that 1 is exponentiable. If this argument weren't given directly, then the proof would be for a particular choice of the exponential of 1. Of course any choice is naturally isomorphic to any other, but it's convenient to not need to add this isomorphism where necessary. Admittedly my docstring "The typeclass argument is explicit: any instance can be used." isn't particularly clear about this, although hopefully "any instance can be used" makes a little more sense now. Thus I agree with Dagur's comments about (2). And as he says, since the argument is given in [] brackets, it's automatically inferred in any application anyway.

Thanks for the explanation. I guess I hadn't quite figured out how to interpret typeclass arguments. I guess the idea is that even though we might specify a particular instance of [Exponentiable (⊤_ C)] some other term might be used somewhere else?

By the way, does Lean allow you to label two distinct terms of a given type as instances?

Thanks!

maintainer merge

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

Regarding merging branches, I guess my suggestion requires you to have a local copy of my branch. So for future reference, I think it would have worked after running git fetch and git checkout dagur/closedUnit or something like that

maintainer merge

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

Thanks for the explanation. I guess I hadn't quite figured out how to interpret typeclass arguments. I guess the idea is that even though we might specify a particular instance of [Exponentiable (⊤_ C)] some other term might be used somewhere else?

Yeah essentially - we can give an instance of Exponentiable (⊤_ C) directly, but it could also be the case that we have that the category is cartesian closed (eg because it's equivalent to another cartesian closed one), which gives a different Exponentiable (⊤_ C) instance. And the point of writing the proof like this is that it works regardless of which of the above are used as the construction.

By the way, does Lean allow you to label two distinct terms of a given type as instances?

Yes. In this example, we could have two different constructions of the right adjoint, which are not equal on the nose. It's usually not a good idea to do this, but it's possible.