Mercurial > hg > Members > kono > Proof > category

comparison src/Polynominal.agda @ 1098:0484477868fe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
1097:321f0fef54c2 1098:0484477868fe
32 -- 32 --
33 -- this makes a few changes, but we don't care. 33 -- this makes a few changes, but we don't care.
34 -- from page. 51 34 -- from page. 51
35 -- 35 --
36 36
37 open Functor
38 open import Relation.Binary.PropositionalEquality hiding ( [_] ; resp ) renaming ( sym to ≡sym )
39
40
37 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 41 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
42
43 data _H≈_ {a b c d : Obj A } ( x : Hom A a b ) (y : Hom A c d ) : Set ( c₁ ⊔ c₂ ⊔ ℓ) where
44 feq : a ≡ c → b ≡ d → (z : Hom A a b) → z ≅ y → A [ x ≈ z ] → x H≈ y
45
46 record SA {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ) where
47 field
48 F : Functor A A
49 without-x : {b c : Obj A} → (f : Hom A b c) → ¬ ( FMap F f H≈ x )
38 50
39 data φ {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ⊔ ℓ) where 51 data φ {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ⊔ ℓ) where
40 i : {b c : Obj A} (k : Hom A b c ) → φ x k 52 i : {b c : Obj A} (k : Hom A b c ) → φ x k
41 ii : φ x {⊤} {a} x 53 ii : φ x {⊤} {a} x
42 iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c' ∧ c''} < f , g > 54 iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c' ∧ c''} < f , g >
65 -- the smallest equivalence relation 77 -- the smallest equivalence relation
66 -- 78 --
67 -- if we use equality on f as in A, Poly is ovioously Hom c b of a Category. 79 -- if we use equality on f as in A, Poly is ovioously Hom c b of a Category.
68 -- it is better to define A[x] as an extension of A as described before 80 -- it is better to define A[x] as an extension of A as described before
69 81
70 record Poly (a c b : Obj A ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where 82 record Poly {a} (x : Hom A １ a) (c b : Obj A ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
71 field 83 field
72 x : Hom A １ a
73 f : Hom A b c 84 f : Hom A b c
74 phi : φ x {b} {c} f 85 phi : φ x {b} {c} f
75 86
76 -- an assuption needed in k x phi ≈ k x phi' 87 -- an assuption needed in k x phi ≈ k x phi'
77 -- k x (i x) ≈ k x ii 88 -- k x (i x) ≈ k x ii
81 -- this is justified equality f ≈ g in A[x] is used in f ∙ < x , id1 A _> ≈ f ∙ < x , id1 A _> 92 -- this is justified equality f ≈ g in A[x] is used in f ∙ < x , id1 A _> ≈ f ∙ < x , id1 A _>
82 -- ( x ∙ π' ) ∙ < x , id1 A _ > ≈ π ∙ < x , id1 A _ > 93 -- ( x ∙ π' ) ∙ < x , id1 A _ > ≈ π ∙ < x , id1 A _ >
83 94
84 -- since we have A[x] now, we can proceed the proof on p.64 in some possible future 95 -- since we have A[x] now, we can proceed the proof on p.64 in some possible future
85 96
97 Ax : {a ⊤ : Obj A } ( x : Hom A １ a ) → SA x → Functor A A
98 Ax {a} {⊤} x sa = record {
99 FObj = λ a → FObj (SA.F sa) a
100 ; FMap = λ {c} {d} f → {!!}
101 ; isFunctor = {!!}
102 }
103
86 -- 104 --
87 -- Proposition 6.1 105 -- Proposition 6.1
88 -- 106 --
89 -- For every polynominal ψ(x) : b → c in an indeterminate x : 1 → a over a cartesian or cartesian closed 107 -- For every polynominal ψ(x) : b → c in an indeterminate x : 1 → a over a cartesian or cartesian closed
90 -- category A there is a unique arrow f : a ∧ b → c in A such that f ∙ < x ∙ ○ b , id1 A b > ≈ ψ(x). 108 -- category A there is a unique arrow f : a ∧ b → c in A such that f ∙ < x ∙ ○ b , id1 A b > ≈ ψ(x).
91 109
92 record Functional-completeness {a b c : Obj A} ( p : Poly a c b ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where 110 record Functional-completeness {a b c : Obj A} (x : Hom A １ a ) ( p : Poly x c b ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
93 x = Poly.x p
94 field 111 field
95 fun : Hom A (a ∧ b) c 112 fun : Hom A (a ∧ b) c
96 fp : A [ fun ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p ] 113 fp : A [ fun ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p ]
97 uniq : ( f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p ] 114 uniq : ( f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p ]
98 → A [ f ≈ fun ] 115 → A [ f ≈ fun ]
99 116
100 -- ε form 117 -- ε form
101 -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) → f ∙ x ≈ φ x 118 -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) → f ∙ x ≈ φ x
102 record Fc {a b : Obj A } ( φ : Poly a b １ ) 119 record Fc {a b : Obj A } (x : Hom A １ a ) ( φ : Poly x b １ )
103 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where 120 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
104 field 121 field
105 sl : Hom A a b 122 sl : Hom A a b
106 g : Hom A １ (b <= a) 123 g : Hom A １ (b <= a)
107 g = ( sl ∙ π' ) * 124 g = ( sl ∙ π' ) *
108 field 125 field
109 isSelect : A [ ε ∙ < g , Poly.x φ > ≈ Poly.f φ ] 126 isSelect : A [ ε ∙ < g , x > ≈ Poly.f φ ]
110 isUnique : (f : Hom A １ (b <= a) ) → A [ ε ∙ < f , Poly.x φ > ≈ Poly.f φ ] 127 isUnique : (f : Hom A １ (b <= a) ) → A [ ε ∙ < f , x > ≈ Poly.f φ ]
111 → A [ g ≈ f ] 128 → A [ g ≈ f ]
112 129
113 -- we should open IsCCC isCCC 130 -- we should open IsCCC isCCC
114 π-cong = IsCCC.π-cong isCCC 131 π-cong = IsCCC.π-cong isCCC
115 *-cong = IsCCC.*-cong isCCC 132 *-cong = IsCCC.*-cong isCCC
142 ( f ∙ < π' ∙ π , π' > ) * ≈↑⟨ *-cong (cdr (IsCCC.e3b isCCC)) ⟩ 159 ( f ∙ < π' ∙ π , π' > ) * ≈↑⟨ *-cong (cdr (IsCCC.e3b isCCC)) ⟩
143 ( f ∙ ( π' ∙ < π ∙ π , < π' ∙ π , π' > > ) ) * ≈⟨ *-cong assoc ⟩ 160 ( f ∙ ( π' ∙ < π ∙ π , < π' ∙ π , π' > > ) ) * ≈⟨ *-cong assoc ⟩
144 ( (f ∙ π') ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨ *-cong ( car ( ki x _ fp )) ⟩ 161 ( (f ∙ π') ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨ *-cong ( car ( ki x _ fp )) ⟩
145 ( k x fp ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨⟩ 162 ( k x fp ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨⟩
146 k x (v fp ) ∎ 163 k x (v fp ) ∎
147 k-cong : {a b c : Obj A} → (f g : Poly a c b ) 164 k-cong : {a b c : Obj A} → (x : Hom A １ a ) → (f g : Poly x c b )
148 → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f) ≈ k (Poly.x g) (Poly.phi g) ] 165 → A [ Poly.f f ≈ Poly.f g ] → A [ k x (Poly.phi f) ≈ k x (Poly.phi g) ]
149 k-cong {a} {b} {c} f g f=f = begin 166 k-cong {a} {b} {c} x f g f=f = begin
150 k (Poly.x f) (Poly.phi f) ≈↑⟨ ki (Poly.x f) (Poly.f f) (Poly.phi f) ⟩ 167 k x (Poly.phi f) ≈↑⟨ ki x (Poly.f f) (Poly.phi f) ⟩
151 Poly.f f ∙ π' ≈⟨ car f=f ⟩ 168 Poly.f f ∙ π' ≈⟨ car f=f ⟩
152 Poly.f g ∙ π' ≈⟨ ki (Poly.x g) (Poly.f g) (Poly.phi g) ⟩ 169 Poly.f g ∙ π' ≈⟨ ki x (Poly.f g) (Poly.phi g) ⟩
153 k (Poly.x g) (Poly.phi g) ∎ 170 k x (Poly.phi g) ∎
154 171
155 -- proof in p.59 Lambek 172 -- proof in p.59 Lambek
156 -- 173 --
157 -- (ψ : Poly a c b) is basically λ x.ψ(x). To use x from outside as a ψ(x), apply x ψ will work. 174 -- (ψ : Poly a c b) is basically λ x.ψ(x). To use x from outside as a ψ(x), apply x ψ will work.
158 -- Instead of replacing x in Poly.phi ψ, we can use simple application with this fuctional completeness 175 -- Instead of replacing x in Poly.phi ψ, we can use simple application with this fuctional completeness
159 -- in the internal language of Topos. 176 -- in the internal language of Topos.
160 -- 177 --
161 functional-completeness : {a b c : Obj A} ( p : Poly a c b ) → Functional-completeness p 178 functional-completeness : {a b c : Obj A} (x : Hom A １ a ) ( p : Poly x c b ) → Functional-completeness x p
162 functional-completeness {a} {b} {c} p = record { 179 functional-completeness {a} {b} {c} x p = record {
163 fun = k (Poly.x p) (Poly.phi p) 180 fun = k x (Poly.phi p)
164 ; fp = fc0 (Poly.x p) (Poly.f p) (Poly.phi p) 181 ; fp = fc0 x (Poly.f p) (Poly.phi p)
165 ; uniq = λ f eq → uniq (Poly.x p) (Poly.f p) (Poly.phi p) f eq 182 ; uniq = λ f eq → uniq x (Poly.f p) (Poly.phi p) f eq
166 } where 183 } where
167 fc0 : {a b c : Obj A} → (x : Hom A １ a) (f : Hom A b c) (phi : φ x {b} {c} f ) 184 fc0 : {a b c : Obj A} → (x : Hom A １ a) (f : Hom A b c) (phi : φ x {b} {c} f )
168 → A [ k x phi ∙ < x ∙ ○ b , id1 A b > ≈ f ] 185 → A [ k x phi ∙ < x ∙ ○ b , id1 A b > ≈ f ]
169 fc0 {a} {b} {c} x f' phi with phi 186 fc0 {a} {b} {c} x f' phi with phi
170 ... | i {_} {_} s = begin 187 ... | i {_} {_} s = begin
243 -- a -> d <= b <-> (a ∧ b ) -> d 260 -- a -> d <= b <-> (a ∧ b ) -> d
244 -- 261 --
245 -- fun ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p 262 -- fun ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p
246 -- (ε ∙ < g ∙ π , π' >) ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p 263 -- (ε ∙ < g ∙ π , π' >) ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p
247 -- could be simpler 264 -- could be simpler
248 FC : {a b : Obj A} → (φ : Poly a b １ ) → Fc {a} {b} φ 265 FC : {a b : Obj A} → (x : Hom A １ a ) → (φ : Poly x b １ ) → Fc {a} {b} x φ
249 FC {a} {b} φ = record { 266 FC {a} {b} x φ = record {
250 sl = k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > 267 sl = k x (Poly.phi φ) ∙ < id1 A _ , ○ a >
251 ; isSelect = isSelect 268 ; isSelect = isSelect
252 ; isUnique = uniq 269 ; isUnique = uniq
253 } where 270 } where
254 π-exchg = IsCCC.π-exchg isCCC 271 π-exchg = IsCCC.π-exchg isCCC
255 fc0 : {b c : Obj A} (p : Poly b c １) → A [ k (Poly.x p ) (Poly.phi p) ∙ < Poly.x p ∙ ○ １ , id1 A １ > ≈ Poly.f p ] 272 fc0 : {b c : Obj A} (p : Poly x c １) → A [ k x (Poly.phi p) ∙ < x ∙ ○ １ , id1 A １ > ≈ Poly.f p ]
256 fc0 p = Functional-completeness.fp (functional-completeness p) 273 fc0 p = Functional-completeness.fp (functional-completeness x p)
257 gg : A [ ( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ Poly.x φ ≈ Poly.f φ ] 274 gg : A [ ( k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ x ≈ Poly.f φ ]
258 gg = begin 275 gg = begin
259 ( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ Poly.x φ ≈⟨ trans-hom (sym assoc) (cdr (IsCCC.distr-π isCCC ) ) ⟩ 276 ( k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ x ≈⟨ trans-hom (sym assoc) (cdr (IsCCC.distr-π isCCC ) ) ⟩
260 k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ∙ Poly.x φ , ○ a ∙ Poly.x φ > ≈⟨ cdr (π-cong idL e2 ) ⟩ 277 k x (Poly.phi φ) ∙ < id1 A _ ∙ x , ○ a ∙ x > ≈⟨ cdr (π-cong idL e2 ) ⟩
261 k (Poly.x φ ) (Poly.phi φ) ∙ < Poly.x φ , ○ １ > ≈⟨ cdr (π-cong (trans-hom (sym idR) (cdr e2) ) (sym e2) ) ⟩ 278 k x (Poly.phi φ) ∙ < x , ○ １ > ≈⟨ cdr (π-cong (trans-hom (sym idR) (cdr e2) ) (sym e2) ) ⟩
262 k (Poly.x φ ) (Poly.phi φ) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ≈⟨ fc0 φ ⟩ 279 k x (Poly.phi φ) ∙ < x ∙ ○ １ , id1 A １ > ≈⟨ fc0 φ ⟩
263 Poly.f φ ∎ 280 Poly.f φ ∎
264 isSelect : A [ ε ∙ < ( ( k (Poly.x φ ) ( Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ π' ) * , Poly.x φ > ≈ Poly.f φ ] 281 isSelect : A [ ε ∙ < ( ( k x ( Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ π' ) * , x > ≈ Poly.f φ ]
265 isSelect = begin 282 isSelect = begin
266 ε ∙ < ((k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ , ○ a > ) ∙ π') * , Poly.x φ > ≈↑⟨ cdr (π-cong idR refl-hom ) ⟩ 283 ε ∙ < ((k (x) (Poly.phi φ)∙ < id1 A _ , ○ a > ) ∙ π') * , x > ≈↑⟨ cdr (π-cong idR refl-hom ) ⟩
267 ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ id1 A _ , Poly.x φ > ) ≈⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩ 284 ε ∙ (< ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ id1 A _ , x > ) ≈⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩
268 ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ １ , Poly.x φ > ) ≈↑⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩ 285 ε ∙ (< ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ １ , x > ) ≈↑⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩
269 ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ (○ a ∙ Poly.x φ) , Poly.x φ > ) ≈↑⟨ cdr (π-cong (sym assoc) idL ) ⟩ 286 ε ∙ (< ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ (○ a ∙ x) , x > ) ≈↑⟨ cdr (π-cong (sym assoc) idL ) ⟩
270 ε ∙ (< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ a ) ∙ Poly.x φ , id1 A _ ∙ Poly.x φ > ) 287 ε ∙ (< (((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ a ) ∙ x , id1 A _ ∙ x > )
271 ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩ 288 ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩
272 ε ∙ ((< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ a ) , id1 A _ > ) ∙ Poly.x φ ) 289 ε ∙ ((< (((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ a ) , id1 A _ > ) ∙ x )
273 ≈↑⟨ cdr (car (π-cong (cdr (IsCCC.e3a isCCC) ) refl-hom)) ⟩ 290 ≈↑⟨ cdr (car (π-cong (cdr (IsCCC.e3a isCCC) ) refl-hom)) ⟩
274 ε ∙ ((< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ (π ∙ < ○ a , id1 A _ > )) , id1 A _ > ) ∙ Poly.x φ ) 291 ε ∙ ((< (((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ (π ∙ < ○ a , id1 A _ > )) , id1 A _ > ) ∙ x )
275 ≈⟨ cdr (car (π-cong assoc (sym (IsCCC.e3b isCCC)) )) ⟩ 292 ≈⟨ cdr (car (π-cong assoc (sym (IsCCC.e3b isCCC)) )) ⟩
276 ε ∙ ((< ((((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π ) ∙ < ○ a , id1 A _ > ) , (π' ∙ < ○ a , id1 A _ > ) > ) ∙ Poly.x φ ) 293 ε ∙ ((< ((((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π ) ∙ < ○ a , id1 A _ > ) , (π' ∙ < ○ a , id1 A _ > ) > ) ∙ x )
277 ≈↑⟨ cdr (car (IsCCC.distr-π isCCC)) ⟩ 294 ≈↑⟨ cdr (car (IsCCC.distr-π isCCC)) ⟩
278 ε ∙ ((< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ∙ < ○ a , id1 A _ > ) ∙ Poly.x φ ) ≈⟨ assoc ⟩ 295 ε ∙ ((< ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ∙ < ○ a , id1 A _ > ) ∙ x ) ≈⟨ assoc ⟩
279 (ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ∙ < ○ a , id1 A _ > ) ) ∙ Poly.x φ ≈⟨ car assoc ⟩ 296 (ε ∙ (< ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ∙ < ○ a , id1 A _ > ) ) ∙ x ≈⟨ car assoc ⟩
280 ((ε ∙ < ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ) ∙ < ○ a , id1 A _ > ) ∙ Poly.x φ 297 ((ε ∙ < ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ) ∙ < ○ a , id1 A _ > ) ∙ x
281 ≈⟨ car (car (IsCCC.e4a isCCC)) ⟩ 298 ≈⟨ car (car (IsCCC.e4a isCCC)) ⟩
282 ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) ∙ < ○ a , id1 A _ > ) ∙ Poly.x φ ≈↑⟨ car assoc ⟩ 299 ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) ∙ < ○ a , id1 A _ > ) ∙ x ≈↑⟨ car assoc ⟩
283 (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ (π' ∙ < ○ a , id1 A _ > ) ) ∙ Poly.x φ ≈⟨ car (cdr (IsCCC.e3b isCCC)) ⟩ 300 (( k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ (π' ∙ < ○ a , id1 A _ > ) ) ∙ x ≈⟨ car (cdr (IsCCC.e3b isCCC)) ⟩
284 (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ id1 A _ ) ∙ Poly.x φ ≈⟨ car idR ⟩ 301 (( k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ id1 A _ ) ∙ x ≈⟨ car idR ⟩
285 ( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ Poly.x φ ≈⟨ gg ⟩ 302 ( k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ x ≈⟨ gg ⟩
286 Poly.f φ ∎ 303 Poly.f φ ∎
287 uniq : (f : Hom A １ (b <= a)) → A [ ε ∙ < f , Poly.x φ > ≈ Poly.f φ ] → 304 uniq : (f : Hom A １ (b <= a)) → A [ ε ∙ < f , x > ≈ Poly.f φ ] →
288 A [ (( k (Poly.x φ) (Poly.phi φ) ∙ < id1 A _ , ○ a > )∙ π' ) * ≈ f ] 305 A [ (( k (x) (Poly.phi φ) ∙ < id1 A _ , ○ a > )∙ π' ) * ≈ f ]
289 uniq f eq = begin 306 uniq f eq = begin
290 (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ π' ) * ≈⟨ IsCCC.*-cong isCCC ( begin 307 (( k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ π' ) * ≈⟨ IsCCC.*-cong isCCC ( begin
291 (k (Poly.x φ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ≈↑⟨ assoc ⟩ 308 (k (x) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ≈↑⟨ assoc ⟩
292 k (Poly.x φ) (Poly.phi φ) ∙ (< id1 A _ , ○ a > ∙ π') ≈⟨ car ( sym (Functional-completeness.uniq (functional-completeness φ) _ ( begin 309 k (x) (Poly.phi φ) ∙ (< id1 A _ , ○ a > ∙ π') ≈⟨ car ( sym (Functional-completeness.uniq (functional-completeness x φ) _ ( begin
293 ((ε ∙ < f ∙ π , π' >) ∙ < π' , π >) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ≈↑⟨ assoc ⟩ 310 ((ε ∙ < f ∙ π , π' >) ∙ < π' , π >) ∙ < x ∙ ○ １ , id1 A １ > ≈↑⟨ assoc ⟩
294 (ε ∙ < f ∙ π , π' >) ∙ ( < π' , π > ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ 311 (ε ∙ < f ∙ π , π' >) ∙ ( < π' , π > ∙ < x ∙ ○ １ , id1 A １ > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
295 (ε ∙ < f ∙ π , π' >) ∙ < π' ∙ < Poly.x φ ∙ ○ １ , id1 A １ > , π ∙ < Poly.x φ ∙ ○ １ , id1 A １ > > 312 (ε ∙ < f ∙ π , π' >) ∙ < π' ∙ < x ∙ ○ １ , id1 A １ > , π ∙ < x ∙ ○ １ , id1 A １ > >
296 ≈⟨ cdr (π-cong (IsCCC.e3b isCCC) (IsCCC.e3a isCCC)) ⟩ 313 ≈⟨ cdr (π-cong (IsCCC.e3b isCCC) (IsCCC.e3a isCCC)) ⟩
297 (ε ∙ < f ∙ π , π' >) ∙ < id1 A １ , Poly.x φ ∙ ○ １ > ≈↑⟨ assoc ⟩ 314 (ε ∙ < f ∙ π , π' >) ∙ < id1 A １ , x ∙ ○ １ > ≈↑⟨ assoc ⟩
298 ε ∙ ( < f ∙ π , π' > ∙ < id1 A １ , Poly.x φ ∙ ○ １ > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ 315 ε ∙ ( < f ∙ π , π' > ∙ < id1 A １ , x ∙ ○ １ > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
299 ε ∙ ( < (f ∙ π ) ∙ < id1 A １ , Poly.x φ ∙ ○ １ > , π' ∙ < id1 A １ , Poly.x φ ∙ ○ １ > > ) ≈⟨ cdr (π-cong (sym assoc) (IsCCC.e3b isCCC)) ⟩ 316 ε ∙ ( < (f ∙ π ) ∙ < id1 A １ , x ∙ ○ １ > , π' ∙ < id1 A １ , x ∙ ○ １ > > ) ≈⟨ cdr (π-cong (sym assoc) (IsCCC.e3b isCCC)) ⟩
300 ε ∙ ( < f ∙ (π ∙ < id1 A １ , Poly.x φ ∙ ○ １ > ) , Poly.x φ ∙ ○ １ > ) ≈⟨ cdr (π-cong (cdr (IsCCC.e3a isCCC)) (cdr (trans-hom e2 (sym e2)))) ⟩ 317 ε ∙ ( < f ∙ (π ∙ < id1 A １ , x ∙ ○ １ > ) , x ∙ ○ １ > ) ≈⟨ cdr (π-cong (cdr (IsCCC.e3a isCCC)) (cdr (trans-hom e2 (sym e2)))) ⟩
301 ε ∙ ( < f ∙ id1 A １ , Poly.x φ ∙ id1 A １ > ) ≈⟨ cdr (π-cong idR idR ) ⟩ 318 ε ∙ ( < f ∙ id1 A １ , x ∙ id1 A １ > ) ≈⟨ cdr (π-cong idR idR ) ⟩
302 ε ∙ < f , Poly.x φ > ≈⟨ eq ⟩ 319 ε ∙ < f , x > ≈⟨ eq ⟩
303 Poly.f φ ∎ ))) ⟩ 320 Poly.f φ ∎ ))) ⟩
304 ((ε ∙ < f ∙ π , π' > ) ∙ < π' , π > ) ∙ ( < id1 A _ , ○ a > ∙ π' ) ≈↑⟨ assoc ⟩ 321 ((ε ∙ < f ∙ π , π' > ) ∙ < π' , π > ) ∙ ( < id1 A _ , ○ a > ∙ π' ) ≈↑⟨ assoc ⟩
305 (ε ∙ < f ∙ π , π' > ) ∙ (< π' , π > ∙ ( < id1 A _ , ○ a > ∙ π' ) ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ 322 (ε ∙ < f ∙ π , π' > ) ∙ (< π' , π > ∙ ( < id1 A _ , ○ a > ∙ π' ) ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
306 (ε ∙ < f ∙ π , π' > ) ∙ (< π' ∙ ( < id1 A _ , ○ a > ∙ π' ) , π ∙ ( < id1 A _ , ○ a > ∙ π' ) > ) ≈⟨ cdr (π-cong assoc assoc ) ⟩ 323 (ε ∙ < f ∙ π , π' > ) ∙ (< π' ∙ ( < id1 A _ , ○ a > ∙ π' ) , π ∙ ( < id1 A _ , ○ a > ∙ π' ) > ) ≈⟨ cdr (π-cong assoc assoc ) ⟩
307 (ε ∙ < f ∙ π , π' > ) ∙ (< (π' ∙ < id1 A _ , ○ a > ) ∙ π' , (π ∙ < id1 A _ , ○ a > ) ∙ π' > ) 324 (ε ∙ < f ∙ π , π' > ) ∙ (< (π' ∙ < id1 A _ , ○ a > ) ∙ π' , (π ∙ < id1 A _ , ○ a > ) ∙ π' > )