Prove that open maps of locales are closed under composition

JetBrains / arend-lib

Apache License 2.0

79 stars 23 forks source link

Prove that open maps of locales are closed under composition #48

Open valis opened 2 years ago

valis commented 2 years ago

This is Topology.Locale/open-comp. A proof of this proposition can be found in Handbook of Categorical Algebra: Volume 3, Francis Borceux, 1994 (Chapter 1), Corollary 1.6.3.