@inproceedings{https://doi.org/10.4230/lipics.fscd.2019.5,<br/><span class="tab"></span>
  doi = {10.4230/LIPICS.FSCD.2019.5},<br/><span class="tab"></span>
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.5},<br/><span class="tab"></span>
  author = {Ahrens,<br/><span class="tab"></span> Benedikt and Frumin,<br/><span class="tab"></span> Dan and Maggesi,<br/><span class="tab"></span> Marco and van der Weide,<br/><span class="tab"></span> Niels},<br/><span class="tab"></span>
  keywords = {bicategory theory,<br/><span class="tab"></span> univalent mathematics,<br/><span class="tab"></span> dependent type theory,<br/><span class="tab"></span> Coq,<br/><span class="tab"></span> Theory of computation → Type theory},<br/><span class="tab"></span>
  language = {en},<br/><span class="tab"></span>
  title = {Bicategories in Univalent Foundations},<br/><span class="tab"></span>
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},<br/><span class="tab"></span>
  year = {2019},<br/><span class="tab"></span>
  copyright = {Creative Commons Attribution 3.0 Unported license}
}