| 123456789101112131415161718192021222324252627282930 |
- module Prelude where
- infixr 90 _∘_
- infixr 50 _∧_
- infix 20 _⟸⇒_
- infixl 3 _from_
- _from_ : (A : Set) -> A -> A
- A from a = a
- _∘_ : {A B C : Set} -> (A -> B) -> (C -> A) -> C -> B
- (f ∘ g) x = f (g x)
- record _∧_ (A B : Set) : Set where
- field
- p₁ : A
- p₂ : B
- open _∧_ public renaming (p₁ to fst; p₂ to snd)
- _,_ : {A B : Set} -> A -> B -> A ∧ B
- x , y = record { p₁ = x; p₂ = y }
- swap : {A B : Set} -> A ∧ B -> B ∧ A
- swap p = (snd p , fst p)
- _⇐⇒_ : Set -> Set -> Set
- A ⇐⇒ B = (A -> B) ∧ (B -> A)
|
