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
}.