4
open import Common.Equality
5
open import Common.Irrelevance
7
record Unit : Set where
10
bla6 : (F : Unit -> Set) ->
11
let X : Unit -> Unit -> Set
13
in (z : Unit) -> X z z ≡ F z
16
bla7 : (F : Unit -> Set) ->
19
in (z : Unit) -> X ≡ F z
23
record R (A : Set) : Set where
30
Sing = (A : Set) -> A -> R (A -> Unit)
32
test : (F : Sing -> Set) ->
35
in (z : Sing) -> X ≡ F z
40
Sing' = (A : Set) -> A -> R (Squash A)
42
test' : (F : Sing' -> Set) ->
43
let X : Sing' -> Sing' -> Set
45
in (z : Sing') -> X z z ≡ F z