@InProceedings{donko_et_al:LIPIcs.TYPES.2021.6, author = {Donk\'{o}, Istv\'{a}n and Kaposi, Ambrus}, title = {{Internal Strict Propositions Using Point-Free Equations}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {6:1--6:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.6}, URN = {urn:nbn:de:0030-drops-167759}, doi = {10.4230/LIPIcs.TYPES.2021.6}, annote = {Keywords: Martin-L\"{o}f’s type theory, intensional type theory, function extensionality, setoid model, homotopy type theory} }