← Back to branch summary

~ubuntu-branches/ubuntu/precise/agda-stdlib/precise

« back to all changes in this revision

Viewing changes to src/Relation/Nullary/Universe.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (2.1.4 sid)
  • Revision ID: package-import@ubuntu.com-20111129170035-be8cbok8ojft5tjl
Tags: 0.6~darcs20111129t1640-1
* [ef445ab] Imported Upstream version 0.6~darcs20111129t1640
  + Darcs snapshot required for Agda 2.3.0 compatibility
* [f801f83] Update BDs and deps to require Agda 2.3.0
* [c52be90] Use 3.0 (quilt) for bz2 orig

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Nullary/Universe.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- A universe of proposition functors, along with some properties
3
5
------------------------------------------------------------------------
4
6
 
29
31
 
30
32
-- The universe.
31
33
 
32
 
data PropF : Set₁ where
33
 
  Id   : PropF
34
 
  K    : (P : Set) → PropF
35
 
  _∨_  : (F₁ F₂ : PropF) → PropF
36
 
  _∧_  : (F₁ F₂ : PropF) → PropF
37
 
  _⇒_  : (P₁ : Set) (F₂ : PropF) → PropF
38
 
  ¬¬_  : (F : PropF) → PropF
 
34
data PropF p : Set (suc p) where
 
35
  Id   : PropF p
 
36
  K    : (P : Set p) → PropF p
 
37
  _∨_  : (F₁ F₂ : PropF p) → PropF p
 
38
  _∧_  : (F₁ F₂ : PropF p) → PropF p
 
39
  _⇒_  : (P₁ : Set p) (F₂ : PropF p) → PropF p
 
40
  ¬¬_  : (F : PropF p) → PropF p
39
41
 
40
42
-- Equalities for universe inhabitants.
41
43
 
42
44
mutual
43
45
 
44
 
  setoid : PropF → {P : Set} → Setoid zero zero
45
 
  setoid Id {P}    = PropEq.setoid P
46
 
  setoid (K P)     = PropEq.setoid P
47
 
  setoid (F₁ ∨ F₂) = setoid F₁ ⊎-setoid setoid F₂
48
 
  setoid (F₁ ∧ F₂) = setoid F₁ ×-setoid setoid F₂
49
 
  setoid (P₁ ⇒ F₂) = FunS.≡-setoid P₁
50
 
                         (Setoid.indexedSetoid (setoid F₂))
51
 
  setoid (¬¬ F) {P} = Always-setoid (¬ ¬ ⟦ F ⟧ P)
52
 
 
53
 
  ⟦_⟧ : PropF → (Set → Set)
54
 
  ⟦ F ⟧ P = Setoid.Carrier (setoid F {P})
55
 
 
56
 
⟨_⟩_≈_ : (F : PropF) {P : Set} → Rel (⟦ F ⟧ P) zero
57
 
⟨_⟩_≈_ F = Setoid._≈_ (setoid F)
 
46
  setoid : ∀ {p} → PropF p → Set p → Setoid p p
 
47
  setoid Id        P = PropEq.setoid P
 
48
  setoid (K P)     _ = PropEq.setoid P
 
49
  setoid (F₁ ∨ F₂) P = (setoid F₁ P) ⊎-setoid (setoid F₂ P)
 
50
  setoid (F₁ ∧ F₂) P = (setoid F₁ P) ×-setoid (setoid F₂ P)
 
51
  setoid (P₁ ⇒ F₂) P = FunS.≡-setoid P₁
 
52
                         (Setoid.indexedSetoid (setoid F₂ P))
 
53
  setoid (¬¬ F)    P = Always-setoid (¬ ¬ ⟦ F ⟧ P)
 
54
 
 
55
  ⟦_⟧ : ∀ {p} → PropF p → (Set p → Set p)
 
56
  ⟦ F ⟧ P = Setoid.Carrier (setoid F P)
 
57
 
 
58
⟨_⟩_≈_ : ∀ {p} (F : PropF p) {P : Set p} → Rel (⟦ F ⟧ P) p
 
59
⟨_⟩_≈_ F = Setoid._≈_ (setoid F _)
58
60
 
59
61
-- ⟦ F ⟧ is functorial.
60
62
 
61
 
map : ∀ F {P Q} → (P → Q) → ⟦ F ⟧ P → ⟦ F ⟧ Q
 
63
map : ∀ {p} (F : PropF p) {P Q} → (P → Q) → ⟦ F ⟧ P → ⟦ F ⟧ Q
62
64
map Id        f  p = f p
63
65
map (K P)     f  p = p
64
66
map (F₁ ∨ F₂) f FP = Sum.map  (map F₁ f) (map F₂ f) FP
66
68
map (P₁ ⇒ F₂) f FP = map F₂ f ∘ FP
67
69
map (¬¬ F)    f FP = ¬¬-map (map F f) FP
68
70
 
69
 
map-id : ∀ F {P} → ⟨ ⟦ F ⟧ P ⇒ F ⟩ map F id ≈ id
 
71
map-id : ∀ {p} (F : PropF p) {P} → ⟨ ⟦ F ⟧ P ⇒ F ⟩ map F id ≈ id
70
72
map-id Id        x        = refl
71
73
map-id (K P)     x        = refl
72
74
map-id (F₁ ∨ F₂) (inj₁ x) = ₁∼₁ (map-id F₁ x)
75
77
map-id (P₁ ⇒ F₂) f        = λ x → map-id F₂ (f x)
76
78
map-id (¬¬ F)    ¬¬x      = _
77
79
 
78
 
map-∘ : ∀ F {P Q R} (f : Q → R) (g : P → Q) →
 
80
map-∘ : ∀ {p} (F : PropF p) {P Q R} (f : Q → R) (g : P → Q) →
79
81
        ⟨ ⟦ F ⟧ P ⇒ F ⟩ map F f ∘ map F g ≈ map F (f ∘ g)
80
82
map-∘ Id        f g x        = refl
81
83
map-∘ (K P)     f g x        = refl
88
90
 
89
91
-- A variant of sequence can be implemented for ⟦ F ⟧.
90
92
 
91
 
sequence : ∀ {AF} → RawApplicative AF →
92
 
           (AF ⊥ → ⊥) →
93
 
           ({A B : Set} → (A → AF B) → AF (A → B)) →
 
93
sequence : ∀ {p AF} → RawApplicative AF →
 
94
           (AF (Lift ⊥) → ⊥) →
 
95
           ({A B : Set p} → (A → AF B) → AF (A → B)) →
94
96
           ∀ F {P} → ⟦ F ⟧ (AF P) → AF (⟦ F ⟧ P)
95
 
sequence {AF} A extract-⊥ sequence-⇒ = helper
 
97
sequence {AF = AF} A extract-⊥ sequence-⇒ = helper
96
98
  where
97
99
  open RawApplicative A
98
100
 
104
106
  helper (F₁ ∧ F₂) (x , y)  = _,_  <$> helper F₁ x ⊛ helper F₂ y
105
107
  helper (P₁ ⇒ F₂) f        = sequence-⇒ (helper F₂ ∘ f)
106
108
  helper (¬¬ F)    x        =
107
 
    pure (λ ¬FP → x (λ fp → extract-⊥ (¬FP <$> helper F fp)))
 
109
    pure (λ ¬FP → x (λ fp → extract-⊥ (lift ∘ ¬FP <$> helper F fp)))
108
110
 
109
111
-- Some lemmas about double negation.
110
112
 
111
 
open RawMonad ¬¬-Monad
 
113
private
 
114
  open module M {p} = RawMonad (¬¬-Monad {p = p})
112
115
 
113
 
¬¬-pull : ∀ F {P} → ⟦ F ⟧ (¬ ¬ P) → ¬ ¬ ⟦ F ⟧ P
 
116
¬¬-pull : ∀ {p} (F : PropF p) {P} →
 
117
          ⟦ F ⟧ (¬ ¬ P) → ¬ ¬ ⟦ F ⟧ P
114
118
¬¬-pull = sequence rawIApplicative
115
 
                   (λ f → f id)
 
119
                   (λ f → f lower)
116
120
                   (λ f g → g (λ x → ⊥-elim (f x (λ y → g (λ _ → y)))))
117
121
 
118
 
¬¬-remove : ∀ F {P} → ¬ ¬ ⟦ F ⟧ (¬ ¬ P) → ¬ ¬ ⟦ F ⟧ P
 
122
¬¬-remove : ∀ {p} (F : PropF p) {P} →
 
123
            ¬ ¬ ⟦ F ⟧ (¬ ¬ P) → ¬ ¬ ⟦ F ⟧ P
119
124
¬¬-remove F = negated-stable ∘ ¬¬-pull (¬¬ F)