Library UniMath.Bicategories.DoubleCategories.DoubleBicat.Core

Require Export UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat.
Require Export UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws.
Require Export UniMath.Bicategories.DoubleCategories.DoubleBicat.UnderlyingCats.
Require Export UniMath.Bicategories.DoubleCategories.Examples.TransposeDoubleBicat.
Require Export UniMath.Bicategories.DoubleCategories.DoubleBicat.CellsAndSquares.
Require Export UniMath.Bicategories.DoubleCategories.DoubleBicat.LocalUnivalence.
Require Export UniMath.Bicategories.DoubleCategories.Examples.HorizontalDual.
Require Export UniMath.Bicategories.DoubleCategories.DoubleBicat.CompanionPairs.
Require Export UniMath.Bicategories.DoubleCategories.DoubleBicat.CompanionPairUnique.
Require Export UniMath.Bicategories.DoubleCategories.DoubleBicat.CompanionPairAdjEquiv.
Require Export UniMath.Bicategories.DoubleCategories.DoubleBicat.Conjoints.
Require Export UniMath.Bicategories.DoubleCategories.DoubleBicat.GregariousEquivalence.
Require Export UniMath.Bicategories.DoubleCategories.DoubleBicat.GlobalUnivalence.