-
Notifications
You must be signed in to change notification settings - Fork 0
/
BaseLogic.agda
66 lines (52 loc) · 1.73 KB
/
BaseLogic.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
module BaseLogic where
open import Agda.Primitive
open import Data.False
open import Data.True
open import Data.Disjunction
open import Data.Product
open import Data.PropositionalEquality
open import Data.Irrelevance
{-
Move this to Data.False
-}
~ : ∀ {α} (A : Set α) → Set α
~ A = A → ⊥
¬ : ∀ {α} (A : Set α) → Set α
¬ = ~
_↔_ : ∀ {i j} (A : Set i) (B : Set j) → Set (i ⊔ j)
A ↔ B = (A → B) ∧ (B → A)
{-
Move this to Data.Functions.Proofs
-}
[x≡y]→[fx≡fy] : ∀ {α β} {A : Set α} {B : Set β} (f : A → B) → (x y : A) → x ≡ y → (f x) ≡ (f y)
[x≡y]→[fx≡fy] {α} {β} {A} {B} f x .x refl = refl
[x≡y]→[Px→Py] : ∀ {α β} {A : Set α} (P : A → Set β) → (x y : A) → x ≡ y → P x → P y
[x≡y]→[Px→Py] {α} {β} {A} P x .x refl Px = Px
{-
Move this to Data.Product.Proofs
-}
p≡[π₁-p,π₂-p] : ∀ {α β} {A : Set α} {B : Set β} (p : A × B) → p ≡ (first p , second p)
p≡[π₁-p,π₂-p] {α} {β} {A} {B} (p1 , p2) = refl
{-
Move this to Data.PropositionalEquality
-}
_≠_ : ∀ {α} {A : Set α} (x y : A) → Set α
x ≠ y = (x ≡ y) → ⊥
≠-↑↓ : ∀ {α} {A : Set α} {x y : A} → x ≠ y → y ≠ x
≠-↑↓ [x≠y] [y≡x] = ☢
where
☢ : ⊥
☢ = [x≠y] (≡-↑↓ [y≡x])
≠-sym : ∀ {i} {A : Set i} {x y : A} → x ≠ y → y ≠ x
≠-sym = ≠-↑↓
[A≡B]→[A→B] : ∀ {α} {A B : Set α} → A ≡ B → A → B
[A≡B]→[A→B] refl a = a
⊤≠⊥ : ⊤ ≠ ⊥
⊤≠⊥ [⊤≡⊥] = ☢
where
[⊤→⊥] : ⊤ → ⊥
[⊤→⊥] = [A≡B]→[A→B] [⊤≡⊥]
☢ : ⊥
☢ = [⊤→⊥] ●
_<=>_ : ∀ {α β} (A : Set α) (B : Set β) → Set (α ⊔ β)
A <=> B = (A → B) ∧ (B → A)