Mercurial > hg > Members > kono > Proof > category
annotate src/ToposIL.agda @ 1098:0484477868fe
explict x in Poly is bad in Internal Language
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 29 Aug 2021 13:44:54 +0900 |
| parents | f6d976d26c5a |
| children |
| rev | line source |
|---|---|
| 963 | 1 open import CCC |
| 2 open import Level | |
| 3 open import Category | |
| 4 open import cat-utility | |
| 5 open import HomReasoning | |
| 1038 | 6 open import Data.List hiding ( [_] ) |
| 1075 | 7 module ToposIL {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (n : ToposNat A (CCC.１ c)) where |
| 963 | 8 |
| 974 | 9 open Topos |
| 10 open Equalizer | |
| 1062 | 11 -- open ≈-Reasoning A hiding (_∙_) |
| 974 | 12 open CCC.CCC c |
| 13 | |
| 1038 | 14 open Functor |
| 15 open import Category.Sets hiding (_o_) | |
| 16 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym) | |
| 1049 | 17 open import Polynominal A c |
| 1048 | 18 |
| 1064 | 19 record IsLogic (Ω : Obj A) (⊤ : Hom A １ Ω) (P : Obj A → Obj A) |
| 20 (_==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A １ Ω) | |
| 21 (_∈_ : {a : Obj A} (x : Hom A １ a ) (α : Hom A １ (P a) ) → Hom A １ Ω) | |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
22 (select : {a : Obj A} (x : Hom A １ a) → ( φ : Poly x Ω １ ) → Hom A １ (P a)) |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
23 (apply : {a : Obj A} (x : Hom A １ a) (p : Poly x Ω １ ) → ( x : Hom A １ a ) → Poly x Ω １ ) |
| 1064 | 24 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where |
| 25 field | |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
26 isSelect : {a : Obj A} → (x : Hom A １ a) → ( φ : Poly x Ω １ ) → {c : Obj A} (h : Hom A c １ ) |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
27 → A [ ( ( x ∈ select x φ ) == Poly.f φ ) ∙ h ≈ ⊤ ∙ ○ c ] |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
28 uniqueSelect : {a : Obj A} → (x : Hom A １ a) → ( φ : Poly x Ω １ ) → (α : Hom A １ (P a) ) |
| 1065 | 29 → {c : Obj A} (h : Hom A c １ ) |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
30 → A [ ( Poly.f φ == ( x ∈ α ) ) ∙ h ≈ ⊤ ∙ ○ c ] |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
31 → A [ ( select x φ == α ) ∙ h ≈ ⊤ ∙ ○ c ] |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
32 isApply : {a : Obj A} (x y : Hom A １ a ) → (q p : Poly x Ω １ ) |
| 1064 | 33 → {c : Obj A} (h : Hom A c １ ) → A [ ( x == y ) ∙ h ≈ ⊤ ∙ ○ c ] |
| 34 → A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] | |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
35 → A [ Poly.f (apply x p x ) ∙ h ≈ ⊤ ∙ ○ c ] |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
36 → A [ Poly.f (apply x p y ) ∙ h ≈ ⊤ ∙ ○ c ] |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
37 applyCong : {a : Obj A} (x : Hom A １ a ) → (q p : Poly x Ω １ ) |
| 1065 | 38 → {c : Obj A} (h : Hom A c １ ) |
| 39 → ( A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] ) | |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
40 → ( A [ Poly.f (apply x q x ) ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f (apply x p x ) ∙ h ≈ ⊤ ∙ ○ c ] ) |
| 1062 | 41 |
| 1046 | 42 record InternalLanguage (Ω : Obj A) (⊤ : Hom A １ Ω) (P : Obj A → Obj A) |
|
1042
a929a58a389d
fix depenency in internal language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1041
diff
changeset
|
43 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where |
| 1038 | 44 field |
| 1046 | 45 _==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A １ Ω |
| 46 _∈_ : {a : Obj A} (x : Hom A １ a ) (α : Hom A １ (P a) ) → Hom A １ Ω | |
| 1039 | 47 -- { x ∈ a | φ x } : P a |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
48 select : {a : Obj A} → (x : Hom A １ a) → ( φ : Poly x Ω １ ) → Hom A １ (P a) |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
49 apply : {a : Obj A} (x : Hom A １ a) (p : Poly x Ω １ ) → ( x : Hom A １ a ) → Poly x Ω １ |
| 1065 | 50 isIL : IsLogic Ω ⊤ P _==_ _∈_ select apply |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
51 _⊢_ : {a b : Obj A} (x : Hom A １ a) (p : Poly x Ω b ) (q : Poly x Ω b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
52 _⊢_ {a} {b} x p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] |
| 1062 | 53 → A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
54 _,_⊢_ : {a b : Obj A} (x : Hom A １ a) (p : Poly x Ω b ) (p1 : Poly x Ω b ) (q : Poly x Ω b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
55 _,_⊢_ {a} {b} x p p1 q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] |
| 1063 | 56 → A [ Poly.f p1 ∙ h ≈ ⊤ ∙ ○ c ] |
| 57 → A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] | |
|
1080
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1077
diff
changeset
|
58 -- expr : {a b c : Obj A} (p : Hom A １ Ω ) → ( x : Hom A １ a ) → Poly a Ω １ |
|
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1077
diff
changeset
|
59 -- expr p x = record { x = x ; f = p ; phi = i ; idx = {!!} } |
| 1063 | 60 ⊨_ : (p : Hom A １ Ω ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) |
| 61 ⊨ p = {c : Obj A} (h : Hom A c １ ) → A [ p ∙ h ≈ ⊤ ∙ ○ c ] | |
| 62 | |
| 963 | 63 -- ○ b |
| 64 -- b -----------→ 1 | |
| 65 -- | | | |
| 66 -- m | | ⊤ | |
| 67 -- ↓ char m ↓ | |
| 68 -- a -----------→ Ω | |
| 971 | 69 |
| 1046 | 70 -- (n : ToposNat A １) |
|
1042
a929a58a389d
fix depenency in internal language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1041
diff
changeset
|
71 -- open NatD |
|
a929a58a389d
fix depenency in internal language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1041
diff
changeset
|
72 -- open ToposNat n |
| 971 | 73 |
|
1042
a929a58a389d
fix depenency in internal language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1041
diff
changeset
|
74 -- N : Obj A |
|
a929a58a389d
fix depenency in internal language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1041
diff
changeset
|
75 -- N = Nat iNat |
| 980 | 76 |
|
1042
a929a58a389d
fix depenency in internal language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1041
diff
changeset
|
77 open import ToposEx A c using ( δmono ) |
| 980 | 78 |
| 1048 | 79 -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) → f ∙ x ≈ φ x |
| 80 | |
| 1093 | 81 |
| 1049 | 82 -- functional completeness |
| 1064 | 83 FC0 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
84 FC0 = {a b : Obj A} (t : Topos A c) (x : Hom A １ a) ( φ : Poly x (Ω t) b) → Functional-completeness x φ |
| 1064 | 85 |
| 1049 | 86 FC1 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
87 FC1 = {a : Obj A} (t : Topos A c) (x : Hom A １ a) ( φ : Poly x (Ω t) １) → Fc x φ |
| 1039 | 88 |
| 1064 | 89 topos→logic : (t : Topos A c ) → ToposNat A １ → FC0 → FC1 → InternalLanguage (Topos.Ω t) (Topos.⊤ t) (λ a → (Topos.Ω t) <= a) |
| 90 topos→logic t n fc0 fc = record { | |
|
1042
a929a58a389d
fix depenency in internal language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1041
diff
changeset
|
91 _==_ = λ {b} f g → A [ char t < id1 A b , id1 A b > (δmono t n ) o < f , g > ] |
| 1046 | 92 ; _∈_ = λ {a} x α → A [ ε o < α , x > ] |
| 1040 | 93 -- { x ∈ a | φ x } : P a |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
94 ; select = λ {a} x φ → Fc.g ( fc t x φ ) |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
95 ; apply = λ {a} φ x y → record { x = x ; f = Functional-completeness.fun (fc0 t y ? ) ∙ < ? ∙ ○ _ , id1 A _ > ; phi = i _ } |
| 1065 | 96 ; isIL = record { |
| 1064 | 97 isSelect = {!!} |
| 98 ; uniqueSelect = {!!} | |
| 99 ; isApply = {!!} | |
| 1065 | 100 ; applyCong = {!!} |
| 1064 | 101 } |
| 1066 | 102 } where |
| 103 open ≈-Reasoning A hiding (_∙_) | |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
104 _⊢_ : {a b : Obj A} {x : Hom A １ a} (p : Poly x (Topos.Ω t) b ) (q : Poly x (Topos.Ω t) b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
105 _⊢_ {a} {b} {x} p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] |
| 1066 | 106 → A [ Poly.f q ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] |
| 1067 | 107 -- |
| 1069 | 108 -- iso ○ c |
| 109 -- e ⇐====⇒ c -----------→ 1 | |
| 1067 | 110 -- | | | |
| 111 -- | h | | ⊤ | |
| 112 -- | ↓ char h ↓ | |
| 1069 | 113 -- + ------→ b -----------→ Ω |
| 1067 | 114 -- ker h fp / fq |
| 115 -- | |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
116 tl01 : {a b : Obj A} (x : Hom A １ a) (p q : Poly x (Topos.Ω t) b ) |
| 1066 | 117 → p ⊢ q → q ⊢ p → A [ Poly.f p ≈ Poly.f q ] |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
118 tl01 {a} {b} x p q p<q q<p = begin |
| 1075 | 119 Poly.f p ≈↑⟨ tt p ⟩ |
|
1095
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1093
diff
changeset
|
120 char t (equalizer (kp p) ) (eMonic A (kp p)) ≈⟨ IsTopos.char-iso (Topos.isTopos t) (equalizer (kp p) ) (equalizer (kp q) ) (eMonic A (kp p)) (eMonic A (kp q)) pqiso ei ⟩ |
| 1077 | 121 char t (equalizer (kp q) ) (eMonic A (kp q)) ≈⟨ tt q ⟩ |
| 1075 | 122 Poly.f q ∎ where |
| 1066 | 123 open import equalizer using ( monic ) |
| 1075 | 124 open IsEqualizer renaming ( k to ek ) |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
125 kp : (p : Poly x (Topos.Ω t) b ) → Equalizer A _ _ |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
126 kp p = Ker t ( Poly.f p ) |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
127 ee : (p q : Poly x (Topos.Ω t) b ) → q ⊢ p |
| 1077 | 128 → A [ A [ Poly.f p o equalizer (Ker t ( Poly.f q )) ] ≈ A [ A [ ⊤ t o ○ b ] o equalizer (Ker t ( Poly.f q ))] ] |
| 129 ee p q q<p = begin | |
| 130 Poly.f p o equalizer (Ker t ( Poly.f q )) ≈⟨ q<p _ ( begin | |
| 131 Poly.f q ∙ equalizer (Ker t ( Poly.f q )) ≈⟨ fe=ge (isEqualizer (Ker t ( Poly.f q))) ⟩ | |
| 132 ( ⊤ t ∙ ○ b ) ∙ equalizer (Ker t ( Poly.f q )) ≈↑⟨ assoc ⟩ | |
| 133 ⊤ t ∙ ( ○ b ∙ equalizer (Ker t ( Poly.f q ))) ≈⟨ cdr e2 ⟩ | |
| 134 ⊤ t ∙ ○ (equalizer-c (Ker t ( Poly.f q ))) ∎ ) ⟩ | |
| 135 ⊤ t ∙ ○ (equalizer-c (Ker t ( Poly.f q ))) ≈↑⟨ cdr e2 ⟩ | |
| 1073 | 136 ⊤ t ∙ ( ○ b ∙ equalizer (Ker t (Poly.f q) )) ≈⟨ assoc ⟩ |
| 1077 | 137 (⊤ t ∙ ○ b) ∙ equalizer (Ker t (Poly.f q) ) ∎ |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
138 qtop : (p q : Poly x (Topos.Ω t) b ) → q ⊢ p → Hom A (equalizer-c (Ker t ( Poly.f q ))) (equalizer-c (Ker t ( Poly.f p ))) |
| 1077 | 139 qtop p q q<p = ek (isEqualizer (Ker t ( Poly.f p))) (equalizer (Ker t ( Poly.f q))) (ee p q q<p) |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
140 qq=1 : (p q : Poly x (Topos.Ω t) b ) → (q<p : q ⊢ p ) → (p<q : p ⊢ q) → A [ A [ qtop p q q<p o qtop q p p<q ] ≈ id1 A (equalizer-c (Ker t ( Poly.f p ))) ] |
| 1077 | 141 qq=1 p q q<p p<q = begin |
| 142 qtop p q q<p o qtop q p p<q ≈↑⟨ uniqueness (isEqualizer (Ker t ( Poly.f p ))) (begin | |
| 143 equalizer (kp p) ∙ (qtop p q q<p ∙ qtop q p p<q ) ≈⟨ assoc ⟩ | |
| 144 (equalizer (kp p) ∙ qtop p q q<p ) ∙ qtop q p p<q ≈⟨ car (ek=h (isEqualizer (kp p))) ⟩ | |
| 145 equalizer (kp q) ∙ qtop q p p<q ≈⟨ ek=h (isEqualizer (kp q)) ⟩ | |
| 146 equalizer (kp p) ∎ ) ⟩ | |
| 147 ek (isEqualizer (kp p)) (equalizer (kp p)) (fe=ge (isEqualizer (kp p))) ≈⟨ uniqueness (isEqualizer (kp p)) idR ⟩ | |
| 148 id1 A _ ∎ | |
| 149 pqiso : Iso A (equalizer-c (kp p)) (equalizer-c (kp q)) | |
| 150 pqiso = record { ≅← = qtop p q q<p ; ≅→ = qtop q p p<q ; iso→ = qq=1 p q q<p p<q ; iso← = qq=1 q p p<q q<p } | |
|
1095
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1093
diff
changeset
|
151 ei : A [ equalizer (Ker t (Poly.f p)) ≈ A [ equalizer (Ker t (Poly.f q)) o Iso.≅→ pqiso ] ] |
|
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1093
diff
changeset
|
152 ei = sym (ek=h (isEqualizer (kp q)) ) |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
153 tt : (q : Poly x (Topos.Ω t) b ) → A [ char t (equalizer (Ker t (Poly.f q))) (eMonic A (Ker t (Poly.f q))) ≈ Poly.f q ] |
| 1069 | 154 tt q = IsTopos.char-uniqueness (Topos.isTopos t) {b} {a} |
| 1062 | 155 |
| 1066 | 156 module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P : Obj A → Obj A) (il : InternalLanguage Ω ⊤ P) (t : Topos A c) where |
| 1062 | 157 open InternalLanguage il |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
158 il00 : {a : Obj A} (x : Hom A １ a) (p : Poly x Ω １ ) → ?-- p ⊢ p |
| 1062 | 159 il00 {a} p h eq = eq |
| 160 | |
| 1066 | 161 --- Poly.f p ∙ h ≈ ⊤ ∙ ○ c |
| 162 --- Poly.f q ∙ h ≈ ⊤ ∙ ○ c | |
| 1063 | 163 |
| 1068 | 164 il011 : {a b : Obj A} (p q q1 : Poly a Ω b ) |
| 1063 | 165 → q ⊢ p → q , q1 ⊢ p |
| 166 il011 {a} p q q1 p<q h tq tq1 = p<q h tq | |
| 167 | |
| 1068 | 168 il012 : {a b : Obj A} (p q r : Poly a Ω b ) |
| 1063 | 169 → q ⊢ p → q , p ⊢ r → q ⊢ r |
| 170 il012 {a} p q r p<q pq<r h qt = pq<r h qt (p<q h qt) | |
| 171 | |
| 172 | |
| 1064 | 173 il02 : {a : Obj A} (x : Hom A １ a ) → ⊨ (x == x) |
| 1063 | 174 il02 = {!!} |
| 175 | |
| 1064 | 176 --- (b : Hom A １ a) → φ y ⊢ φ' y → φ b ⊢ φ' b |
| 177 il03 : {a : Obj A} (b : Hom A １ a ) → (q p : Poly a Ω １ ) | |
| 178 → q ⊢ p → apply q b ⊢ apply p b | |
| 1065 | 179 il03 {a} b q p q<p h = IsLogic.applyCong (InternalLanguage.isIL il ) b q p h (q<p h) |
| 1064 | 180 |
| 1063 | 181 --- a == b → φ a ⊢ φ b |
| 182 il04 : {a : Obj A} (x y : Hom A １ a ) → (q p : Poly a Ω １ ) | |
| 1064 | 183 → ⊨ (x == y) |
| 1063 | 184 → q ⊢ apply p x → q ⊢ apply p y |
| 1065 | 185 il04 {a} x y q p eq q<px h qt = IsLogic.isApply (InternalLanguage.isIL il ) x y q p h (eq h) qt (q<px h qt ) |
| 1062 | 186 |
| 1064 | 187 --- ⊨ x ∈ select φ == φ x |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
188 il05 : {a : Obj A} (x : Hom A １ a) → (q : Poly x Ω １ ) |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
189 → ⊨ ( ( x ∈ select q ) == Poly.f q ) |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
190 il05 {a} x = IsLogic.isSelect (InternalLanguage.isIL il ) |
| 1064 | 191 |
| 192 --- q ⊢ φ x == x ∈ α | |
| 193 --- ----------------------- | |
| 194 --- q ⊢ select φ == α | |
| 195 --- | |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
196 il06 : {a : Obj A} (x : Hom A １ a) → (q : Poly a Ω １ ) → (α : Hom A １ (P a) ) |
|
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
197 → ⊨ ( Poly.f q == ( x ∈ α ) ) |
| 1064 | 198 → ⊨ ( select q == α ) |
|
1098
0484477868fe
explict x in Poly is bad in Internal Language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1096
diff
changeset
|
199 il06 {a} x q p eq h = IsLogic.uniqueSelect (InternalLanguage.isIL il ) q p h (eq h) |
| 1064 | 200 |