Merge pull request #170 from fizruk/AKLV/comprehension-cats

Connect type categories with comprehension categories
UniMath · Apr 27, 2020 · bf85f4e · bf85f4e
2 parents ad54ca1 + fd1c122
commit bf85f4e
Show file tree

Hide file tree

Showing 2 changed files with 520 additions and 0 deletions.
diff --git a/TypeTheory/ALV2/.package/files b/TypeTheory/ALV2/.package/files
@@ -11,3 +11,4 @@ RelUniv_Cat.v
 RelUniv_Cat_Iso.v
 RelUniv_Cat_Yo_CwF_Iso.v
 RelUnivTransfer.v
+TypeCat_ComprehensionCat.v