6
open import Common.Equality
11
record _×_ (A B : Set) : Set where
18
swap : {A B : Set} → A × B → B × A
23
prop_swap : {A B : Set}{p : A × B} →
24
(fst (swap p) ≡ snd p) ×
25
(snd (swap p) ≡ fst p)
26
prop_swap = refl , refl
28
rot3 : {A B C : Set} → A × B × C → B × C × A
45
test = let tt , _ = tt , tt in A