Mercurial > hg > Members > kono > Proof > category

comparison src/Polynominal.agda @ 1015:e01a1d29492b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Functional Completeness
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 21 Mar 2021 10:16:57 +0900
parents 4f1db956d3b4
children bbbe97d2a5ea
comparison
equal deleted inserted replaced
1014:4f1db956d3b4 1015:e01a1d29492b
1 open import Category 1 open import Category
2 open import CCC 2 open import CCC
3 open import Level 3 open import Level
4 open import HomReasoning 4 open import HomReasoning
5 open import cat-utility 5 open import cat-utility
6 6
7 module Polynominal { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( C : CCC A ) where 7 module Polynominal { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( C : CCC A ) where
8
9 module coKleisli { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where
10
11 open coMonad
12
13 open Functor
14 open NTrans
15
16 --
17 -- Hom in Kleisli Category
18 --
19
20 record SHom (a : Obj A) (b : Obj A)
21 : Set c₂ where
22 field
23 SMap : Hom A ( FObj S a ) b
24
25 open SHom
26
27 S-id : (a : Obj A) → SHom a a
28 S-id a = record { SMap = TMap (ε SM) a }
29
30 open import Relation.Binary
31
32 _⋍_ : { a : Obj A } { b : Obj A } (f g : SHom a b ) → Set ℓ
33 _⋍_ {a} {b} f g = A [ SMap f ≈ SMap g ]
34
35 _*_ : { a b c : Obj A } → ( SHom b c) → ( SHom a b) → SHom a c
36 _*_ {a} {b} {c} g f = record { SMap = coJoin SM {a} {b} {c} (SMap g) (SMap f) }
37
38 isSCat : IsCategory ( Obj A ) SHom _⋍_ _*_ (λ {a} → S-id a)
39 isSCat = record { isEquivalence = isEquivalence
40 ; identityL = SidL
41 ; identityR = SidR
42 ; o-resp-≈ = So-resp
43 ; associative = Sassoc
44 }
45 where
46 open ≈-Reasoning A
47 isEquivalence : { a b : Obj A } → IsEquivalence {_} {_} {SHom a b} _⋍_
48 isEquivalence {C} {D} = record { refl = refl-hom ; sym = sym ; trans = trans-hom }
49 SidL : {a b : Obj A} → {f : SHom a b} → (S-id _ * f) ⋍ f
50 SidL {a} {b} {f} = begin
51 SMap (S-id _ * f) ≈⟨⟩
52 (TMap (ε SM) b o (FMap S (SMap f))) o TMap (δ SM) a ≈↑⟨ car (nat (ε SM)) ⟩
53 (SMap f o TMap (ε SM) (FObj S a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩
54 SMap f o TMap (ε SM) (FObj S a) o TMap (δ SM) a ≈⟨ cdr (IsCoMonad.unity1 (isCoMonad SM)) ⟩
55 SMap f o id1 A _ ≈⟨ idR ⟩
56 SMap f ∎
57 SidR : {C D : Obj A} → {f : SHom C D} → (f * S-id _ ) ⋍ f
58 SidR {a} {b} {f} = begin
59 SMap (f * S-id a) ≈⟨⟩
60 (SMap f o FMap S (TMap (ε SM) a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩
61 SMap f o (FMap S (TMap (ε SM) a) o TMap (δ SM) a) ≈⟨ cdr (IsCoMonad.unity2 (isCoMonad SM)) ⟩
62 SMap f o id1 A _ ≈⟨ idR ⟩
63 SMap f ∎
64 So-resp : {a b c : Obj A} → {f g : SHom a b } → {h i : SHom b c } →
65 f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
66 So-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = resp refl-hom (resp (fcong S eq-fg ) eq-hi )
67 Sassoc : {a b c d : Obj A} → {f : SHom c d } → {g : SHom b c } → {h : SHom a b } →
68 (f * (g * h)) ⋍ ((f * g) * h)
69 Sassoc {a} {b} {c} {d} {f} {g} {h} = begin
70 SMap (f * (g * h)) ≈⟨ car (cdr (distr S)) ⟩
71 (SMap f o ( FMap S (SMap g o FMap S (SMap h)) o FMap S (TMap (δ SM) a) )) o TMap (δ SM) a ≈⟨ car assoc ⟩
72 ((SMap f o FMap S (SMap g o FMap S (SMap h))) o FMap S (TMap (δ SM) a) ) o TMap (δ SM) a ≈↑⟨ assoc ⟩
73 (SMap f o FMap S (SMap g o FMap S (SMap h))) o (FMap S (TMap (δ SM) a) o TMap (δ SM) a ) ≈↑⟨ cdr (IsCoMonad.assoc (isCoMonad SM)) ⟩
74 (SMap f o (FMap S (SMap g o FMap S (SMap h)))) o ( TMap (δ SM) (FObj S a) o TMap (δ SM) a ) ≈⟨ assoc ⟩
75 ((SMap f o (FMap S (SMap g o FMap S (SMap h)))) o TMap (δ SM) (FObj S a) ) o TMap (δ SM) a ≈⟨ car (car (cdr (distr S))) ⟩
76 ((SMap f o (FMap S (SMap g) o FMap S (FMap S (SMap h)))) o TMap (δ SM) (FObj S a) ) o TMap (δ SM) a ≈↑⟨ car assoc ⟩
77 (SMap f o ((FMap S (SMap g) o FMap S (FMap S (SMap h))) o TMap (δ SM) (FObj S a) )) o TMap (δ SM) a ≈↑⟨ assoc ⟩
78 SMap f o (((FMap S (SMap g) o FMap S (FMap S (SMap h))) o TMap (δ SM) (FObj S a) ) o TMap (δ SM) a) ≈↑⟨ cdr (car assoc ) ⟩
79 SMap f o ((FMap S (SMap g) o (FMap S (FMap S (SMap h)) o TMap (δ SM) (FObj S a) )) o TMap (δ SM) a) ≈⟨ cdr (car (cdr (nat (δ SM)))) ⟩
80 SMap f o ((FMap S (SMap g) o ( TMap (δ SM) b o FMap S (SMap h))) o TMap (δ SM) a) ≈⟨ assoc ⟩
81 (SMap f o (FMap S (SMap g) o ( TMap (δ SM) b o FMap S (SMap h)))) o TMap (δ SM) a ≈⟨ car (cdr assoc) ⟩
82 (SMap f o ((FMap S (SMap g) o TMap (δ SM) b ) o FMap S (SMap h))) o TMap (δ SM) a ≈⟨ car assoc ⟩
83 ((SMap f o (FMap S (SMap g) o TMap (δ SM) b )) o FMap S (SMap h)) o TMap (δ SM) a ≈⟨ car (car assoc) ⟩
84 (((SMap f o FMap S (SMap g)) o TMap (δ SM) b ) o FMap S (SMap h)) o TMap (δ SM) a ≈⟨⟩
85 SMap ((f * g) * h) ∎
86
87 SCat : Category c₁ c₂ ℓ
88 SCat = record { Obj = Obj A ; Hom = SHom ; _o_ = _*_ ; _≈_ = _⋍_ ; Id = λ {a} → S-id a ; isCategory = isSCat }
89
90 module coKleisli' { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where
91 8
92 open CCC.CCC C 9 open CCC.CCC C
93 open coMonad 10 open coMonad
94 open Functor 11 open Functor
95 open NTrans 12 open NTrans
96 open import Category.Cat 13 open import Category.Cat
97 14
98 open ≈-Reasoning A 15 open ≈-Reasoning A hiding (_∙_)
99 SA : (a : Obj A) → Functor A A 16 SA : (a : Obj A) → Functor A A
100 SA a = record { 17 SA a = record {
101 FObj = λ x → a ∧ x 18 FObj = λ x → a ∧ x
102 ; FMap = λ f → < π , A [ f o π' ] > 19 ; FMap = λ f → < π , A [ f o π' ] >
103 ; isFunctor = record { 20 ; isFunctor = record {
160 < π , < π , id1 A _ > > ≈↑⟨ IsCCC.π-cong isCCC refl-hom idR ⟩ 77 < π , < π , id1 A _ > > ≈↑⟨ IsCCC.π-cong isCCC refl-hom idR ⟩
161 < π , < π , id1 A _ > o id1 A _ > ≈↑⟨ IsCCC.π-cong isCCC refl-hom (cdr (IsCCC.e3b isCCC)) ⟩ 78 < π , < π , id1 A _ > o id1 A _ > ≈↑⟨ IsCCC.π-cong isCCC refl-hom (cdr (IsCCC.e3b isCCC)) ⟩
162 < π , < π , id1 A _ > o ( π' o < π , id1 A _ > ) > ≈↑⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (sym assoc) ⟩ 79 < π , < π , id1 A _ > o ( π' o < π , id1 A _ > ) > ≈↑⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (sym assoc) ⟩
163 < π o < π , id1 A _ > , (< π , id1 A _ > o π' ) o < π , id1 A _ > > ≈↑⟨ IsCCC.distr-π isCCC ⟩ 80 < π o < π , id1 A _ > , (< π , id1 A _ > o π' ) o < π , id1 A _ > > ≈↑⟨ IsCCC.distr-π isCCC ⟩
164 FMap (SA a) < π , id1 A (a ∧ x) > o < π , id1 A _ > ∎ 81 FMap (SA a) < π , id1 A (a ∧ x) > o < π , id1 A _ > ∎
165 82 --
166 83 -- coKleisli category of SM should give the fucntional completeness
167 84 --
168 -- open import deductive A C 85
169 86 _∙_ = _[_o_] A
170 _・_ = _[_o_] A 87
171 88 --
172 -- every proof b → c with assumption a has following forms 89 -- Polynominal (p.57) in Introduction to Higher order categorical logic
90 --
91 -- Given object a₀ and a of a caterisian closed category A, how does one adjoin an interminate arraow x : a₀ → a to A?
92 -- A[x] based on the `assumption' x, as was done in Section 2 (data φ). The formulas of A[x] are the objects of A and the
93 -- proofs of A[x] are formed from the arrows of A and the new arrow x : a₀ → a by the appropriate ules of inference.
173 -- 94 --
174 -- Here, A is actualy A[x]. It contains x and all the arrow generated from x. 95 -- Here, A is actualy A[x]. It contains x and all the arrow generated from x.
175 -- If we can put constraints on rule i, then A is strictly smaller than A[x]. 96 -- If we can put constraints on rule i (sub : Hom A b c → Set), then A is strictly smaller than A[x],
97 -- that is, a subscategory of A[x].
98 --
99 -- i : {b c : Obj A} {k : Hom A b c } → sub k → φ x k
100 --
101 -- this makes a few changes, but we don't care.
102 -- from page. 51
176 -- 103 --
177 data φ {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ⊔ ℓ) where 104 data φ {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ⊔ ℓ) where
178 i : {b c : Obj A} {k : Hom A b c } → φ x k 105 i : {b c : Obj A} {k : Hom A b c } → φ x k
179 ii : φ x {⊤} {a} x 106 ii : φ x {⊤} {a} x
180 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 > 107 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 >
181 iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g ) 108 iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ∙ g )
182 v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' } (ψ : φ x f ) → φ x {b} {c'' <= c'} ( f * ) 109 v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' } (ψ : φ x f ) → φ x {b} {c'' <= c'} ( f * )
183 φ-cong : {b c : Obj A} {k k' : Hom A b c } → A [ k ≈ k' ] → φ x k → φ x k' 110 φ-cong : {b c : Obj A} {k k' : Hom A b c } → A [ k ≈ k' ] → φ x k → φ x k'
184 111
185 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) ) 112 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
186 α = < π ・ π , < π' ・ π , π' > > 113 α = < π ∙ π , < π' ∙ π , π' > >
187 114
188 -- genetate (a ∧ b) → c proof from proof b → c with assumption a 115 -- genetate (a ∧ b) → c proof from proof b → c with assumption a
116 -- from page. 51
189 117
190 k : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → {z : Hom A b c } → ( y : φ {a} x∈a z ) → Hom A (a ∧ b) c 118 k : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → {z : Hom A b c } → ( y : φ {a} x∈a z ) → Hom A (a ∧ b) c
191 k x∈a {k} i = k ・ π' 119 k x∈a {k} i = k ∙ π'
192 k x∈a ii = π 120 k x∈a ii = π
193 k x∈a (iii ψ χ ) = < k x∈a ψ , k x∈a χ > 121 k x∈a (iii ψ χ ) = < k x∈a ψ , k x∈a χ >
194 k x∈a (iv ψ χ ) = k x∈a ψ ・ < π , k x∈a χ > 122 k x∈a (iv ψ χ ) = k x∈a ψ ∙ < π , k x∈a χ >
195 k x∈a (v ψ ) = ( k x∈a ψ ・ α ) * 123 k x∈a (v ψ ) = ( k x∈a ψ ∙ α ) *
196 k x∈a (φ-cong eq ψ) = k x∈a ψ 124 k x∈a (φ-cong eq ψ) = k x∈a ψ
197 125
198 toφ : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z 126 toφ : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z
199 toφ {a} {⊤} {b} {c} x∈a z = i 127 toφ {a} {⊤} {b} {c} x∈a z = i
200 128
202 field 130 field
203 hom : Hom A b c 131 hom : Hom A b c
204 phi : φ x {b} {c} hom 132 phi : φ x {b} {c} hom
205 133
206 open PHom 134 open PHom
207 -- open import HomReasoning 135
208 -- open import cat-utility 136 -- A is A[x]
209
210 -- date _≅_ : {a b c : Hom A} → { x : Hom A ⊤ a } → (f g : PHom b c ) → Set (c₁ ⊔ c₂ ⊔ ℓ) where
211 -- pcomp : { a b c : Hom A } → A [ A [ hom g o hom f ] ≈ hom h ] → (A [ hom g o hom f ]) ≅ hom h
212
213 -- this is too easy, so what is A[x]?
214 Polynominal : {a ⊤ : Obj A } ( x : Hom A ⊤ a ) → Category c₁ (c₁ ⊔ c₂ ⊔ ℓ) ℓ 137 Polynominal : {a ⊤ : Obj A } ( x : Hom A ⊤ a ) → Category c₁ (c₁ ⊔ c₂ ⊔ ℓ) ℓ
215 Polynominal {a} {⊤} x = record { 138 Polynominal {a} {⊤} x = record {
216 Obj = Obj A; 139 Obj = Obj A;
217 Hom = λ b c → PHom {a} {⊤} {x} b c ; 140 Hom = λ b c → PHom {a} {⊤} {x} b c ;
218 _o_ = λ{a} {b} {c} x y → record { hom = A [ hom x o hom y ] ; phi = iv (phi x) (phi y) } ; 141 _o_ = λ{a} {b} {c} x y → record { hom = hom x ∙ hom y ; phi = iv (phi x) (phi y) } ;
219 _≈_ = λ x y → A [ hom x ≈ hom y ] ; 142 _≈_ = λ x y → A [ hom x ≈ hom y ] ;
220 Id = λ{a} → record { hom = id1 A a ; phi = i } ; 143 Id = λ{a} → record { hom = id1 A a ; phi = i } ;
221 isCategory = record { 144 isCategory = record {
222 isEquivalence = record { sym = sym-hom ; trans = trans-hom ; refl = refl-hom } ; 145 isEquivalence = record { sym = sym-hom ; trans = trans-hom ; refl = refl-hom } ;
223 identityL = λ {a b f} → idL ; 146 identityL = λ {a b f} → idL ;
236 ; distr = refl-hom 159 ; distr = refl-hom
237 ; ≈-cong = λ eq → eq 160 ; ≈-cong = λ eq → eq
238 } 161 }
239 } 162 }
240 163
164 --
165 -- Proposition 6.1
166 --
167 -- For every polynominal ψ(x) : b → c in an indeterminate x : 1 → a over a cartesian or cartesian closed
168 -- category A there is a unique arrow f : a ∧ b → c in A such that f ∙ < x ∙ ○ b , id1 A b > ≈ ψ(x).
169 --
170
241 record Functional-completeness {a : Obj A} ( x : Hom A １ a ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where 171 record Functional-completeness {a : Obj A} ( x : Hom A １ a ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
242 field 172 field
243 fun : {b c : Obj A} → PHom {a} {１} {x} b c → Hom A (a ∧ b) c 173 fun : {b c : Obj A} → PHom {a} {１} {x} b c → Hom A (a ∧ b) c
244 fp : {b c : Obj A} → (p : PHom b c) → A [ A [ fun p o < A [ x o ○ b ] , id1 A b > ] ≈ hom p ] 174 fp : {b c : Obj A} → (p : PHom b c) → A [ fun p ∙ < x ∙ ○ b , id1 A b > ≈ hom p ]
245 uniq : {b c : Obj A} → (p : PHom b c) → (f : Hom A (a ∧ b) c) → A [ A [ f o < A [ x o ○ b ] , id1 A b > ] ≈ hom p ] 175 uniq : {b c : Obj A} → (p : PHom b c) → (f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b , id1 A b > ≈ hom p ]
246 → A [ f ≈ fun p ] 176 → A [ f ≈ fun p ]
247 177
178 π-cong = IsCCC.π-cong isCCC
179 e2 = IsCCC.e2 isCCC
180 {-# TERMINATING #-}
248 functional-completeness : {a : Obj A} ( x : Hom A １ a ) → Functional-completeness x 181 functional-completeness : {a : Obj A} ( x : Hom A １ a ) → Functional-completeness x
249 functional-completeness {a} x = record { 182 functional-completeness {a} x = record {
250 fun = λ y → k x (phi y) 183 fun = λ y → k x (phi y)
251 ; fp = fc0 184 ; fp = fc0
252 ; uniq = uniq 185 ; uniq = uniq
253 } where 186 } where
254 open φ 187 open φ
255 fc0 : {b c : Obj A} (p : PHom b c) → A [ A [ k x (phi p) o < A [ x o ○ b ] , id1 A b > ] ≈ hom p ] 188 fc0 : {b c : Obj A} (p : PHom b c) → A [ k x (phi p) ∙ < x ∙ ○ b , id1 A b > ≈ hom p ]
256 fc0 {b} {c} p with phi p 189 fc0 {b} {c} p with phi p
257 ... | i {_} {_} {s} = begin 190 ... | i {_} {_} {s} = begin
258 (s o π') o < ( x o ○ b ) , id1 A b > ≈↑⟨ assoc ⟩ 191 (s ∙ π') ∙ < ( x ∙ ○ b ) , id1 A b > ≈↑⟨ assoc ⟩
259 s o (π' o < ( x o ○ b ) , id1 A b >) ≈⟨ cdr (IsCCC.e3b isCCC ) ⟩ 192 s ∙ (π' ∙ < ( x ∙ ○ b ) , id1 A b >) ≈⟨ cdr (IsCCC.e3b isCCC ) ⟩
260 s o id1 A b ≈⟨ idR ⟩ 193 s ∙ id1 A b ≈⟨ idR ⟩
261 s ∎ 194 s ∎
262 ... | ii = begin 195 ... | ii = begin
263 π o < ( x o ○ b ) , id1 A b > ≈⟨ IsCCC.e3a isCCC ⟩ 196 π ∙ < ( x ∙ ○ b ) , id1 A b > ≈⟨ IsCCC.e3a isCCC ⟩
264 x o ○ b ≈↑⟨ cdr (IsCCC.e2 isCCC ) ⟩ 197 x ∙ ○ b ≈↑⟨ cdr (e2 ) ⟩
265 x o id1 A b ≈⟨ idR ⟩ 198 x ∙ id1 A b ≈⟨ idR ⟩
266 x ∎ 199 x ∎
267 ... | iii {_} {_} {_} {f} {g} y z = begin 200 ... | iii {_} {_} {_} {f} {g} y z = begin
268 < k x y , k x z > o < (x o ○ b ) , id1 A b > ≈⟨ IsCCC.distr-π isCCC ⟩ 201 < k x y , k x z > ∙ < (x ∙ ○ b ) , id1 A b > ≈⟨ IsCCC.distr-π isCCC ⟩
269 < k x y o < (x o ○ b ) , id1 A b > , k x z o < (x o ○ b ) , id1 A b > > 202 < k x y ∙ < (x ∙ ○ b ) , id1 A b > , k x z ∙ < (x ∙ ○ b ) , id1 A b > >
270 ≈⟨ IsCCC.π-cong isCCC (fc0 record { hom = f ; phi = y } ) (fc0 record { hom = g ; phi = z } ) ⟩ 203 ≈⟨ π-cong (fc0 record { hom = f ; phi = y } ) (fc0 record { hom = g ; phi = z } ) ⟩
271 < f , g > ≈⟨⟩ 204 < f , g > ≈⟨⟩
272 hom p ∎ 205 hom p ∎
273 ... | iv {_} {_} {d} {f} {g} y z = begin 206 ... | iv {_} {_} {d} {f} {g} y z = begin
274 (k x y o < π , k x z >) o < ( x o ○ b ) , id1 A b > ≈↑⟨ assoc ⟩ 207 (k x y ∙ < π , k x z >) ∙ < ( x ∙ ○ b ) , id1 A b > ≈↑⟨ assoc ⟩
275 k x y o ( < π , k x z > o < ( x o ○ b ) , id1 A b > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ 208 k x y ∙ ( < π , k x z > ∙ < ( x ∙ ○ b ) , id1 A b > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
276 k x y o ( < π o < ( x o ○ b ) , id1 A b > , k x z o < ( x o ○ b ) , id1 A b > > ) 209 k x y ∙ ( < π ∙ < ( x ∙ ○ b ) , id1 A b > , k x z ∙ < ( x ∙ ○ b ) , id1 A b > > )
277 ≈⟨ cdr (IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (fc0 record { hom = g ; phi = z} ) ) ⟩ 210 ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) (fc0 record { hom = g ; phi = z} ) ) ⟩
278 k x y o ( < x o ○ b , g > ) ≈↑⟨ cdr (IsCCC.π-cong isCCC (cdr (IsCCC.e2 isCCC)) refl-hom ) ⟩ 211 k x y ∙ ( < x ∙ ○ b , g > ) ≈↑⟨ cdr (π-cong (cdr (e2)) refl-hom ) ⟩
279 k x y o ( < x o ( ○ d o g ) , g > ) ≈⟨ cdr (IsCCC.π-cong isCCC assoc (sym idL)) ⟩ 212 k x y ∙ ( < x ∙ ( ○ d ∙ g ) , g > ) ≈⟨ cdr (π-cong assoc (sym idL)) ⟩
280 k x y o ( < (x o ○ d) o g , id1 A d o g > ) ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩ 213 k x y ∙ ( < (x ∙ ○ d) ∙ g , id1 A d ∙ g > ) ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩
281 k x y o ( < x o ○ d , id1 A d > o g ) ≈⟨ assoc ⟩ 214 k x y ∙ ( < x ∙ ○ d , id1 A d > ∙ g ) ≈⟨ assoc ⟩
282 (k x y o < x o ○ d , id1 A d > ) o g ≈⟨ car (fc0 record { hom = f ; phi = y }) ⟩ 215 (k x y ∙ < x ∙ ○ d , id1 A d > ) ∙ g ≈⟨ car (fc0 record { hom = f ; phi = y }) ⟩
283 f o g ∎ 216 f ∙ g ∎
284 ... | v {_} {_} {_} {f} y = begin 217 ... | v {_} {_} {_} {f} y = begin
285 ( (k x y o < π o π , < π' o π , π' > >) *) o < x o (○ b) , id1 A b > ≈⟨ IsCCC.distr-* isCCC ⟩ 218 ( (k x y ∙ < π ∙ π , < π' ∙ π , π' > >) *) ∙ < x ∙ (○ b) , id1 A b > ≈⟨ IsCCC.distr-* isCCC ⟩
286 ( (k x y o < π o π , < π' o π , π' > >) o < < x o ○ b , id1 A _ > o π , π' > ) * ≈⟨ IsCCC.*-cong isCCC ( begin 219 ( (k x y ∙ < π ∙ π , < π' ∙ π , π' > >) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) * ≈⟨ IsCCC.*-cong isCCC ( begin
287 ( k x y o < π o π , < π' o π , π' > >) o < < x o ○ b , id1 A _ > o π , π' > ≈↑⟨ assoc ⟩ 220 ( k x y ∙ < π ∙ π , < π' ∙ π , π' > >) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ≈↑⟨ assoc ⟩
288 k x y o ( < π o π , < π' o π , π' > > o < < x o ○ b , id1 A _ > o π , π' > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ 221 k x y ∙ ( < π ∙ π , < π' ∙ π , π' > > ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
289 k x y o < (π o π) o < < x o ○ b , id1 A _ > o π , π' > , < π' o π , π' > o < < x o ○ b , id1 A _ > o π , π' > > 222 k x y ∙ < (π ∙ π) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > , < π' ∙ π , π' > ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > >
290 ≈⟨ cdr (IsCCC.π-cong isCCC (sym assoc) (IsCCC.distr-π isCCC )) ⟩ 223 ≈⟨ cdr (π-cong (sym assoc) (IsCCC.distr-π isCCC )) ⟩
291 k x y o < π o (π o < < x o ○ b , id1 A _ > o π , π' > ) , 224 k x y ∙ < π ∙ (π ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) ,
292 < (π' o π) o < < x o ○ b , id1 A _ > o π , π' > , π' o < < x o ○ b , id1 A _ > o π , π' > > > 225 < (π' ∙ π) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > , π' ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > > >
293 ≈⟨ cdr ( IsCCC.π-cong isCCC (cdr (IsCCC.e3a isCCC))( IsCCC.π-cong isCCC (sym assoc) (IsCCC.e3b isCCC) )) ⟩ 226 ≈⟨ cdr ( π-cong (cdr (IsCCC.e3a isCCC))( π-cong (sym assoc) (IsCCC.e3b isCCC) )) ⟩
294 k x y o < π o ( < x o ○ b , id1 A _ > o π ) , < π' o (π o < < x o ○ b , id1 A _ > o π , π' >) , π' > > 227 k x y ∙ < π ∙ ( < x ∙ ○ b , id1 A _ > ∙ π ) , < π' ∙ (π ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' >) , π' > >
295 ≈⟨ cdr ( IsCCC.π-cong isCCC refl-hom ( IsCCC.π-cong isCCC (cdr (IsCCC.e3a isCCC)) refl-hom )) ⟩ 228 ≈⟨ cdr ( π-cong refl-hom ( π-cong (cdr (IsCCC.e3a isCCC)) refl-hom )) ⟩
296 k x y o < (π o < x o ○ b , id1 A _ > o π ) , < π' o (< x o ○ b , id1 A _ > o π ) , π' > > 229 k x y ∙ < (π ∙ ( < x ∙ ○ b , id1 A _ > ∙ π ) ) , < π' ∙ (< x ∙ ○ b , id1 A _ > ∙ π ) , π' > >
297 ≈⟨ cdr ( IsCCC.π-cong isCCC assoc (IsCCC.π-cong isCCC assoc refl-hom )) ⟩ 230 ≈⟨ cdr ( π-cong assoc (π-cong assoc refl-hom )) ⟩
298 k x y o < (π o < x o ○ b , id1 A _ > ) o π , < (π' o < x o ○ b , id1 A _ > ) o π , π' > > 231 k x y ∙ < (π ∙ < x ∙ ○ b , id1 A _ > ) ∙ π , < (π' ∙ < x ∙ ○ b , id1 A _ > ) ∙ π , π' > >
299 ≈⟨ cdr (IsCCC.π-cong isCCC (car (IsCCC.e3a isCCC)) (IsCCC.π-cong isCCC (car (IsCCC.e3b isCCC)) refl-hom )) ⟩ 232 ≈⟨ cdr (π-cong (car (IsCCC.e3a isCCC)) (π-cong (car (IsCCC.e3b isCCC)) refl-hom )) ⟩
300 k x y o < ( (x o ○ b ) o π ) , < id1 A _ o π , π' > > ≈⟨ cdr (IsCCC.π-cong isCCC (sym assoc) (IsCCC.π-cong isCCC idL refl-hom )) ⟩ 233 k x y ∙ < ( (x ∙ ○ b ) ∙ π ) , < id1 A _ ∙ π , π' > > ≈⟨ cdr (π-cong (sym assoc) (π-cong idL refl-hom )) ⟩
301 k x y o < x o (○ b o π ) , < π , π' > > ≈⟨ cdr (IsCCC.π-cong isCCC (cdr (IsCCC.e2 isCCC)) (IsCCC.π-id isCCC) ) ⟩ 234 k x y ∙ < x ∙ (○ b ∙ π ) , < π , π' > > ≈⟨ cdr (π-cong (cdr (e2)) (IsCCC.π-id isCCC) ) ⟩
302 k x y o < x o ○ _ , id1 A _ > ≈⟨ fc0 record { hom = f ; phi = y} ⟩ 235 k x y ∙ < x ∙ ○ _ , id1 A _ > ≈⟨ fc0 record { hom = f ; phi = y} ⟩
303 f ∎ ) ⟩ 236 f ∎ ) ⟩
304 f * ∎ 237 f * ∎
305 ... | φ-cong {_} {_} {f} {f'} f=f' y = trans-hom (fc0 record { hom = f ; phi = y}) f=f' 238 ... | φ-cong {_} {_} {f} {f'} f=f' y = trans-hom (fc0 record { hom = f ; phi = y}) f=f'
239 --
240 -- f ∙ < x ∙ ○ b , id1 A b > ≈ hom p → f ≈ k x (phi p)
241 --
306 uniq : {b c : Obj A} (p : PHom b c) (f : Hom A (a ∧ b) c) → 242 uniq : {b c : Obj A} (p : PHom b c) (f : Hom A (a ∧ b) c) →
307 A [ A [ f o < A [ x o ○ b ] , id1 A b > ] ≈ hom p ] → A [ f ≈ k x (phi p) ] 243 A [ f ∙ < x ∙ ○ b , id1 A b > ≈ hom p ] → A [ f ≈ k x (phi p) ]
308 uniq {b} {c} p f fx=p with phi p 244 uniq {b} {c} p f fx=p = sym (begin
309 ... | i {_} {_} {s} = begin -- f o < x o ○ b , id1 A b > ≈ s 245 k x (phi p) ≈⟨ fc1 p ⟩
310 f ≈↑⟨ idR ⟩ 246 k x {hom p} i ≈⟨⟩
311 f o id1 A (a ∧ b) ≈⟨ {!!} ⟩ 247 hom p ∙ π' ≈↑⟨ car fx=p ⟩
312 f o (< x o ○ b , id1 A b > o π' ) ≈⟨ assoc ⟩ 248 (f ∙ < x ∙ ○ b , id1 A b > ) ∙ π' ≈↑⟨ assoc ⟩
313 (f o < x o ○ b , id1 A b > ) o π' ≈⟨ car fx=p ⟩ 249 f ∙ (< x ∙ ○ b , id1 A b > ∙ π') ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
314 s o π' ∎ 250 f ∙ < (x ∙ ○ b) ∙ π' , id1 A b ∙ π' > ≈⟨⟩
315 ... | ii = begin -- fx=p : f o < x o ○ b , id1 A b > ≈ x 251 f ∙ < k x {x ∙ ○ b} i , id1 A b ∙ π' > ≈⟨ cdr (π-cong (sym (fc1 record { hom = x ∙ ○ b ; phi = iv ii i } )) refl-hom) ⟩
316 f ≈⟨ {!!} ⟩ 252 f ∙ < k x (phi record { hom = x ∙ ○ b ; phi = iv ii i }) , id1 A b ∙ π' > ≈⟨ cdr (π-cong refl-hom idL) ⟩
317 π ∎ 253 f ∙ < π ∙ < π , (○ b ∙ π' ) > , π' > ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) refl-hom) ⟩
318 ... | iii {_} {_} {_} {g} {h} y z = begin -- fx=p : f o < x o ○ b , id1 A b > ≈ < g , h > 254 f ∙ < π , π' > ≈⟨ cdr (IsCCC.π-id isCCC) ⟩
319 f ≈⟨ {!!} ⟩ 255 f ∙ id1 A _ ≈⟨ idR ⟩
320 < k x y , k x z > ∎ 256 f ∎ ) where
321 ... | iv t t₁ = {!!} 257 fc1 : {b c : Obj A} (p : PHom b c) → A [ k x (phi p) ≈ k x {hom p} i ] -- it looks like (*) in page 60
322 ... | v t = {!!} 258 fc1 {b} {c} p = uniq record { hom = hom p ; phi = i } ( k x (phi p)) ( begin -- non terminating because of the record, which we may avoid
323 ... | φ-cong x t = {!!} 259 k x (phi p) ∙ < x ∙ ○ b , id1 A b > ≈⟨ fc0 p ⟩
324 260 hom p ∎ )
325 261
326 262
327 -- end 263 -- end