@ARTICLE{FINTOPO8,
    TITLE = {A Case Study of Transport Urysohn's Lemma from TopSpace Defined with Open   Sets to TopSpace Defined with Neighborhoods},
    AUTHOR = {Coghetto, Roland},
    ADDRESS1 = {Rue de la Brasserie 5\\7100 La Louvi\`ere, Belgium},
    DAY = {25},
    MONTH = {October},
    YEAR = {2020},
    SUMMARY = {Jozef Bialas and Yatsuka Nakamura has completely formalized a proof 
  of Urysohn's lemma in the article \cite{URYSOHN3.ABS}, in the context of a 
  topological space defined from the open sets. In the MML, the topological space 
  is defined in this way by Beata Padlewska and Agata Darmochwa\l in the article 
  \cite{PRE_TOPC.ABS}. In \cite{FINTOPO7.ABS} the topological space is defined with  
  neighborhoods. It is well known that these definitions are equivalent
  \cite{Bourbaki2013general,bourbaki2007topologie}. \par
  In the definitions, an abstract structure (i.e. the article \verb!STRUCT_0! and 
  its descendants, all of them directly or indirectly using Mizar structures
  \cite{bancerek2018role}) has been used (see \cite{Grabowski2020}).
  The first topological definition is based with the Mizar structure 
  {\tt TopStruct} and the topological space defined with neighborhood with 
  the Mizar structure: \textit{FMT_Space_Str}.
  To emphasize the notion of neighborhood, we 
  rename {\tt FMT_TOPSPACE} to {\tt NTopSpace}.\par
  Using Mizar \cite{Mizar-State-2015}, we transport the 
  Urysohn's lemma from {\tt TopSpace} to {\tt NTopSpace}.\par
  In some cases, Mizar allows certain techniques for transporting 
  proof, definitions or theorems. Generally speaking, there is no 
  automatic transport but some methods. \par
  In Coq, Isabelle/Hol or homotpy type theory transport is 
  also studied, sometimes with a more systematic 
  aim \cite{magaud2003changing,zimmermann2015automatic,
  huffman2013lifting,johnsen2004theorem,coquand2014theorie,
  tabareau2018equivalences}.
  In \cite{chad_brown_2019_3548609}, two co-existing Isabelle libraries,
  Isabelle/HOL and Isabelle/Mizar, have been aligned in a single 
  foundation in the Isabelle logical framework.\par
  In the MML, they have been used since the beginning: 
  {\tt reconsider}, {\tt registration}, {\tt cluster}
  others were later implemented \cite{Korni2009}: {\tt identify}.\par
  In some proofs, it is possible to define particular functors between different   
  structures, mainly useful when results are already obtained in 
  a given structure. This technique is used, for example, in 
  \cite{MATRIXR1.ABS} to define two functors {\tt MXR2MXF} and {\tt MXF2MXF} 
  between {\tt Matrix of REAL} and {\tt Matrix of F_Real} and to transport the     
  definition of the addition from one structure to the other: 
  [...] {\tt A + B -> Matrix of REAL equals MXF2MXR 
  ((MXR2MXF A) + (MXR2MXF B))} [...].\par
  In this paper, first we align the necessary topological concepts.
  For the formalization, we were inspired by the works of Claude 
  Wagschal \cite{wagschal}. It allows us to transport more naturally 
  the Urysohn's lemma (\verb!URYSOHN3:20!) to the topological space 
  defined with neighborhoods.\par
  Nakasho and Shidama have developed a solution to explore the 
  notions introduced by different authors 
  \url{https://mimosa-project.github.io/mmlreference/current/}\cite  {nakasho2015documentation}.\par
  The definitions can be directly linked in the HTML version of the Mizar 
  library. (Example: 
  Urysohn's lemma \url{http://mizar.org/version/current/html/urysohn3.html#T20})},
    MSC2010 = {54A05;03B35;68V20},
    KEYWORDS = {filter;topological from neighborhoods;transfer principle; transport of structure;align},}

@article{coquand2014theorie,
  title={Th{\'e}orie des types d{\'e}pendants et axiome d’univalence},
  author={Coquand, Thierry},
  journal={S{\'e}minaire Bourbaki},
  volume={66},
  pages={1085},
  year={2014}
}

@article{tabareau2018equivalences,
  title={Equivalences for free: univalent parametricity for effective transport},
  author={Tabareau, Nicolas and Tanter, {\'E}ric and Sozeau, Matthieu},
  journal={Proceedings of the ACM on Programming Languages},
  volume={2},
  number={ICFP},
  pages={1--29},
  year={2018},
  publisher={ACM New York, NY, USA}
}

@inproceedings{johnsen2004theorem,
  title={Theorem reuse by proof term transformation},
  author={Johnsen, Einar Broch and L{\"u}th, Christoph},
  booktitle={International Conference on Theorem Proving in Higher Order Logics},
  pages={152--167},
  year={2004},
  organization={Springer}
}

@inproceedings{huffman2013lifting,
  title={Lifting and Transfer: A modular design for quotients in Isabelle/HOL},
  author={Huffman, Brian and Kun{\v{c}}ar, Ond{\v{r}}ej},
  booktitle={International Conference on Certified Programs and Proofs},
  pages={131--146},
  year={2013},
  organization={Springer}
}

@article{zimmermann2015automatic,
  title={Automatic and transparent transfer of theorems along isomorphisms in the Coq proof assistant},
  author={Zimmermann, Theo and Herbelin, Hugo},
  journal={arXiv preprint arXiv:1505.05028},
  year={2015}
}

@inproceedings{magaud2003changing,
  title={Changing data representation within the Coq system},
  author={Magaud, Nicolas},
  booktitle={International Conference on Theorem Proving in Higher Order Logics},
  pages={87--102},
  year={2003},
  organization={Springer}
}


@Inbook{Korni2009,
author="Korni{\l}owicz, Artur",
title="How to define terms in Mizar effectively",
editor="Grabowski, Adam 
and Naumowicz, Adam",
booktitle="Computer Reconstruction of the Body of Mathematics. Studies in Logic, Grammar and Rhetoric", 
VOLUME="18",
NUMBER="31",
pages="67–77",
publisher="University of Bia{\l}ystok",
year="2009"
}


@article{bancerek2018role,
  title={The role of the Mizar Mathematical Library for interactive proof development in Mizar},
  author={Bancerek, Grzegorz and Byli{\'n}ski, Czes{\l}aw and 
    Grabowski, Adam and Korni{\l}owicz, Artur and Matuszewski, Roman and 
	Naumowicz, Adam and P{\k{a}}k, Karol},
  journal={Journal of Automated Reasoning},
  volume={61},
  number={1-4},
  pages={9--32},
  year={2018},
  publisher={Springer}
}

@Inbook{Grabowski2020,
author="Grabowski, Adam
and Korni{\l}owicz, Artur
and Schwarzweller, Christoph",
editor="Grabowski, Adam
and Loukanova, Roussanka
and Schwarzweller, Christoph",
title="Refining Algebraic Hierarchy in Mathematical Repository of Mizar",
bookTitle="AI Aspects in Reasoning, Languages, and Computation",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="49--75",
isbn="978-3-030-41425-2",
doi="10.1007/978-3-030-41425-2_2",
url="https://doi.org/10.1007/978-3-030-41425-2_2"
}


@Inbook{Grabo2020EFT,
author="Grabowski, Adam
and Coghetto, Roland",
editor="Grabowski, Adam
and Loukanova, Roussanka
and Schwarzweller, Christoph",
title="Extending Formal Topology in Mizar by Uniform Spaces",
bookTitle="AI Aspects in Reasoning, Languages, and Computation",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="77--105",

isbn="978-3-030-41425-2",
doi="10.1007/978-3-030-41425-2_3",
url="https://doi.org/10.1007/978-3-030-41425-2_3"
}

@proceedings{chad_brown_2019_3548609,
  title        = {{Higher-Order Tarski Grothendieck as a Foundation 
                   for Formal Proof}},
  year         = 2019,
  publisher    = {Zenodo},
  month        = sep,
  doi          = {10.4230/lipics.itp.2019.9},
  url          = {https://doi.org/10.4230/lipics.itp.2019.9}
}

