12
data _≅_ {A : Set} (x : A) : ∀ {B : Set} → B → Set where
15
record Σ (A : Set) (B : A → Set) : Set where
23
data Bool : Set where true false : Bool
25
data Unit1 : Set where unit1 : Unit1
26
data Unit2 : Set where unit2 : Unit2
33
P S = Σ S (\s → s ≅ unit1)
38
¬pbool2 : ¬ P (D false)
39
¬pbool2 ( unit2 , () )
42
unit2 ≅ unit1 should be empty, but that's not obvious to me
43
when checking that the clause ¬pbool2 (unit2 , ()) has type