Skip to content

Commit

Permalink
chore(category_theory/subterminal): update docstring (#7289)
Browse files Browse the repository at this point in the history
  • Loading branch information
b-mehta committed Apr 22, 2021
1 parent 07e9dd4 commit d9df8fb
Showing 1 changed file with 1 addition and 3 deletions.
4 changes: 1 addition & 3 deletions src/category_theory/subterminal.lean
Expand Up @@ -21,9 +21,7 @@ We also construct the subcategory of subterminal objects.
## TODO
* Define exponential ideals, and show this subcategory is an exponential ideal.
* Define subobject lattices in general, show that `subterminals C` is equivalent to the subobject
category of a terminal object.
* Use both the above to show that in a locally cartesian closed category, every subobject lattice
* Use the above to show that in a locally cartesian closed category, every subobject lattice
is cartesian closed (equivalently, a Heyting algebra).
-/
Expand Down

0 comments on commit d9df8fb

Please sign in to comment.