Library HoTT.Tests.Metatheory.FunextVarieties
From
HoTT.Metatheory
Require
Import
FunextVarieties
.
Checking the universes of FunextVarieties.v
Check
NaiveFunext@
{
i
j
max
}
.
Check
NaiveNondepFunext@
{
i
j
max
}
.
Check
WeakFunext@
{
i
j
max
}
.