Cohesion/Prop.agda at master · DavidJaz/Cohesion · GitHub

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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
{-# OPTIONS --without-K #-}

module Prop where

  open import Base


  open import lib.Basics
  open import lib.types.Sigma
  open import lib.NType2
  open import lib.types.Truncation
  open import lib.types.Lift


  _is-contractible : {i : ULevel} (A : Type i) → Type i
  _is-contractible = is-contr

  ⊤-is-contr : ⊤ is-contractible
  ⊤-is-contr = has-level-in (unit , (λ {unit → refl}))

  contr-≃-⊤ : {i : ULevel} {A : Type i} (c : A is-contractible)
              → A ≃ ⊤
  contr-≃-⊤ {A = A} c =
    equiv (λ _ → unit) (λ { unit → contr-center c })
          (λ {unit → refl})
          (λ a → contr-path c a)

  _is-a-prop : ∀ {i} → (A : Type i)  → Type i
  A is-a-prop = is-prop A


  Prop : (i : ULevel) → Type _
  Prop = hProp

  Prop₀ = hProp₀

  _holds : ∀ {i} (P : Prop i) → Type i
  _holds = fst

  _holds-is-a-prop : {i : ULevel} (P : Prop i) → (P holds) is-a-prop
  _holds-is-a-prop = snd


  ∥_∥ : ∀ {i} (A :  Type i) → Type i
  ∥_∥ = Trunc -1

  True : Prop₀
  True = ⊤ , contr-is-prop ⊤-is-contr

  False : Prop₀
  False = ⊥ , has-level-in (λ x → quodlibet x)

  _And_ : ∀ {i j} → (A : Type i) (B : Type j) → Type (lmax i j)
  A And B = Σ A (λ _ → B)

  _And→_ : ∀ {i j k l} {A : Type i} {B : Type j} {C : Type k} {D : Type l}
           (f : A → C) (g : B → D)
           → (A And B) → (C And D)
  f And→ g = λ { (a , b) → f a , g b }

  infixl 30 _∧_
  _∧_ : ∀ {i j} (P : Prop i) (Q : Prop j) → Prop (lmax i j)
  P ∧ Q = ((P holds) And (Q  holds)) , Σ-level (P holds-is-a-prop) (λ _ → Q holds-is-a-prop)

  infixl 35 _∨_
  _∨_ : ∀ {i j} (P : Prop i) (Q : Prop j) → Prop (lmax i j)
  P ∨ Q = ∥ (P holds) ⊔ (Q holds) ∥ , ⟨⟩

  mapping-into-prop-is-a-prop : {i j : ULevel} {A : Type i} {P : A → Type j}
                                (f : (a : A) → ((P a) is-a-prop))
                                → ((a : A) → P a) is-a-prop
  mapping-into-prop-is-a-prop f = all-paths-is-prop (λ x y →
                                    λ= (λ a → prop-path (f a) (x a) (y a)))


  _⇒_ : ∀ {i j} (P : Prop i) (Q : Prop j) → Prop (lmax i j)
  P ⇒ Q = (P holds → Q holds) , mapping-into-prop-is-a-prop (λ _ → Q holds-is-a-prop)

  not : ∀ {i} (P : Prop i) → Prop i
  not P = P ⇒ False

  {-
    To say ``There exists an a : A such that B a", write
      ∃ (λ (a : A) → B a)
  -}
  ∃ : {i j : ULevel} {A : Type i} (B : A → Type j) → Prop (lmax i j)
  ∃ {_} {_} {A} B = ∥ (Σ A B) ∥ , ⟨⟩

  ∃ₚ : ∀ {i j} {A : Type i} (B : A → Prop j) → Prop (lmax i j)
  ∃ₚ {A = A} B = ∃ λ (a : A) → (B a) holds

  ∀ₚ : ∀ {i j} {A : Type i} (P : A → Prop j) → Prop (lmax i j)
  ∀ₚ P = (∀ a → (P a) holds) , mapping-into-prop-is-a-prop (λ a → (P a) holds-is-a-prop)

  _holds-implies-dec-eq : {i : ULevel} (P : Prop i)
                          → P holds → (P holds) ≃ (Dec (P holds))
  (P holds-implies-dec-eq) p  = equiv (λ _ → inl p)
                                      ((λ { (inl q) → q ; (inr nq) → quodlibet (nq p) }))
                                      (λ { (inl q) → ap inl (prop-path (P holds-is-a-prop) p q)
                                         ; (inr nq) → quodlibet (nq p) })
                                      (λ q → prop-path (P holds-is-a-prop) p q)

  _holds-by_implies-=-True : (P : Prop₀) (p : P holds)
                             → P == True
  (P , q) holds-by p implies-=-True = pair= left-id right-id
    where
      left-id : P == ⊤
      left-id = (ua {A = P} {B = True holds} (contr-≃-⊤ {A = P} (inhab-prop-is-contr p {{q}})))

      right-id : q == (snd True) [ _is-a-prop ↓ left-id ]
      right-id = from-transp _is-a-prop left-id
                      (prop-path (has-level-is-prop) (transport _is-a-prop left-id q) (snd True) )

  ¬-_holds-by_implies-=-False : (P : Prop₀) (p : ¬ (P holds))
                                → P == False
  ¬- (P , q) holds-by np implies-=-False = pair= left-id right-id
    where
      left-id : P == ⊥
      left-id = ua {A = P} {B = False holds} e
        where e : P ≃ ⊥
              e = equiv np (λ ()) (λ ()) (λ p → quodlibet (np p))

      right-id : q == (snd False) [ _is-a-prop ↓ left-id ]
      right-id =
        from-transp _is-a-prop left-id
          (prop-path (has-level-is-prop) (transport _is-a-prop left-id q) (snd False))

  iff-to-≃ : ∀ {i j} {P : Prop i} {Q : Prop j}
             → (P holds → Q holds)
             → (Q holds → P holds)
             → (P holds) ≃ (Q holds)
  iff-to-≃ {P = P} {Q = Q} f g =
    equiv f g
      (λ b → prop-path (snd Q) (f (g b)) b)
      (λ a → prop-path (snd P) (g (f a)) a)

  -- Propositional Resizing

  lift-prop : {i j : ULevel} → Prop i → Prop (lmax i j)
  lift-prop {i} {j} (P , q) = (Lift {i} {j} P) , Lift-level q

  postulate prop-resize : {i j : ULevel} → (lift-prop {i} {j}) is-an-equiv

  resize-eq : {i j : ULevel} → Prop i ≃ Prop (lmax i j)
  resize-eq {i} {j} = (lift-prop {i} {j}) , prop-resize

  resize₀ : {i : ULevel} → Prop i → Prop₀
  resize₀ {i} = <– (resize-eq {lzero} {i})

  unresize₀ : {i : ULevel} → Prop₀ → Prop i
  unresize₀ {i} = –> (resize-eq {lzero} {i})