@@ -8,7 +8,7 @@ isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)
9class Set univ => HasPower univ where
9class Set univ => HasPower univ where
10 Powerset : (a : univ) ->
10 Powerset : (a : univ) ->
11− Pair univ (\Pa => (c : univ) ->
11+ Sigma univ (\Pa => (c : univ) ->
12 (isSubsetOf c a) -> member c Pa)
12 (isSubsetOf c a) -> member c Pa)
14powerset : HasPower univ => univ -> univ
14powerset : HasPower univ => univ -> univ