Merge pull request #173 from fizruk/AKLV/typecat-comprehension_cat_equiv

Type categories are equivalent to (full and faithful) comprehension categories
UniMath · May 7, 2020 · 521ac0d · 521ac0d
2 parents bf85f4e + b71db05
commit 521ac0d
Show file tree

Hide file tree

Showing 3 changed files with 959 additions and 27 deletions.
diff --git a/TypeTheory/ALV2/.package/files b/TypeTheory/ALV2/.package/files
@@ -12,3 +12,4 @@ RelUniv_Cat_Iso.v
 RelUniv_Cat_Yo_CwF_Iso.v
 RelUnivTransfer.v
 TypeCat_ComprehensionCat.v
+FullyFaithfulDispFunctor.v