Mercurial > hg > Members > kono > Proof > category

annotate freyd.agda @ 672:749df4959d19

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix completeness
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Nov 2017 09:00:01 +0900
parents 959954fc29f8
children 917e51be9bbf
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Category -- https://github.com/konn/category-agda
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
628
b99660fa14e1 remove arrow's yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 617
diff changeset
4 module freyd where
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
307
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
6 open import cat-utility
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
7 open import HomReasoning
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Relation.Binary.Core
307
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
9 open Functor
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
311
cf278f4d0b32 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 310
diff changeset
11 -- C is small full subcategory of A ( C is image of F )
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
307
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
13 record SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
14 : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
306
92475fe5f59e Small Full Subcategory (underconstruction)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 305
diff changeset
15 field
442
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
16 SFSF : Functor A A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
17 SFSFMap← : { a b : Obj A } → Hom A (FObj SFSF a) (FObj SFSF b ) → Hom A a b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
18 full→ : { a b : Obj A } { x : Hom A (FObj SFSF a) (FObj SFSF b) } → A [ FMap SFSF ( SFSFMap← x ) ≈ x ]
632
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
19 full← : { a b : Obj A } { x : Hom A (FObj SFSF a) (FObj SFSF b) } → A [ SFSFMap← ( FMap SFSF x ) ≈ x ]
442
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
20
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
21 -- ≈→≡ : {a b : Obj A } → { x y : Hom A (FObj SFSF a) (FObj SFSF b) } →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
22 -- (x≈y : A [ FMap SFSF x ≈ FMap SFSF y ]) → FMap SFSF x ≡ FMap SFSF y -- codomain of FMap is local small
305
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 304
diff changeset
23
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
24 -- pre-initial
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
25
311
cf278f4d0b32 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 310
diff changeset
26 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
27 (F : Functor A A) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
308
7f00cd09274c pre-initial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
28 field
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
29 preinitialObj : Obj A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
30 preinitialArrow : ∀{a : Obj A } → Hom A ( FObj F preinitialObj ) a
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
31
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
32 -- initial object
671
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 636
diff changeset
33 -- now in cat-utility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 636
diff changeset
34 -- record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 636
diff changeset
35 -- field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 636
diff changeset
36 -- initial : ∀( a : Obj A ) → Hom A i a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 636
diff changeset
37 -- uniqueness : { a : Obj A } → ( f : Hom A i a ) → A [ f ≈ initial a ]
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
38
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 314
diff changeset
39 -- A complete catagory has initial object if it has PreInitial-SmallFullSubcategory
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
40
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
41 open NTrans
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
42 open Limit
487
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
43 open IsLimit
313
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
44 open SmallFullSubcategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
45 open PreInitial
440
ff36c500962e fix limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 439
diff changeset
46 open Complete
ff36c500962e fix limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 439
diff changeset
47 open Equalizer
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 442
diff changeset
48 open IsEqualizer
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
49
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
50 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
440
ff36c500962e fix limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 439
diff changeset
51 (comp : Complete A A)
442
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
52 (SFS : SmallFullSubcategory A ) →
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
53 (PI : PreInitial A (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS))
442
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
54 initialFromPreInitialFullSubcategory A comp SFS PI = record {
314
d1af69c4aaf8 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 313
diff changeset
55 initial = initialArrow ;
636
3e663c7f88c4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 632
diff changeset
56 uniqueness = λ {a} f → lemma1 a f
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
57 } where
442
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
58 F : Functor A A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
59 F = SFSF SFS
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
60 FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
61 FMap← = SFSFMap← SFS
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
62 a00 : Obj A
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
63 a00 = limit-c comp F
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
64 lim : ( Γ : Functor A A ) → Limit A A Γ
487
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
65 lim Γ = climit comp Γ
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
66 u : NTrans A A (K A A a00) F
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
67 u = t0 ( lim F )
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 442
diff changeset
68 equ : {a b : Obj A} → (f g : Hom A a b) → IsEqualizer A (equalizer-e comp f g ) f g
672
749df4959d19 fix completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 671
diff changeset
69 equ f g = isEqualizer ( Complete.cequalizer comp f g )
442
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
70 ep : {a b : Obj A} → {f g : Hom A a b} → Obj A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
71 ep {a} {b} {f} {g} = equalizer-p comp f g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
72 ee : {a b : Obj A} → {f g : Hom A a b} → Hom A (ep {a} {b} {f} {g} ) a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
73 ee {a} {b} {f} {g} = equalizer-e comp f g
617
34540494fdcf initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
74 f : Hom A a00 (FObj F (preinitialObj PI ) )
34540494fdcf initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
75 f = TMap u (preinitialObj PI )
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
76 initialArrow : ∀( a : Obj A ) → Hom A a00 a
437
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
77 initialArrow a = A [ preinitialArrow PI {a} o f ]
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
78 equ-fi : { a : Obj A} → {f' : Hom A a00 a} →
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 442
diff changeset
79 IsEqualizer A ee ( A [ preinitialArrow PI {a} o f ] ) f'
440
ff36c500962e fix limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 439
diff changeset
80 equ-fi {a} {f'} = equ ( A [ preinitialArrow PI {a} o f ] ) f'
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
81 e=id : {e : Hom A a00 a00} → ( {c : Obj A} → A [ A [ TMap u c o e ] ≈ TMap u c ] ) → A [ e ≈ id1 A a00 ]
438
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
82 e=id {e} uce=uc = let open ≈-Reasoning (A) in
437
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
83 begin
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
84 e
495
633df882db86 fryed1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 487
diff changeset
85 ≈↑⟨ limit-uniqueness (isLimit (lim F)) ( λ {i} → uce=uc ) ⟩
487
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
86 limit (isLimit (lim F)) a00 u
495
633df882db86 fryed1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 487
diff changeset
87 ≈⟨ limit-uniqueness (isLimit (lim F)) ( λ {i} → idR ) ⟩
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
88 id1 A a00
437
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
89 ∎
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
90 kfuc=uc : {c k1 : Obj A} → {p : Hom A k1 a00} → A [ A [ TMap u c o
440
ff36c500962e fix limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 439
diff changeset
91 A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ]
ff36c500962e fix limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 439
diff changeset
92 ≈ TMap u c ]
441
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
93 kfuc=uc {c} {k1} {p} = let open ≈-Reasoning (A) in
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
94 begin
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
95 TMap u c o ( p o ( preinitialArrow PI {k1} o TMap u (preinitialObj PI) ))
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
96 ≈⟨ cdr assoc ⟩
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
97 TMap u c o ((p o preinitialArrow PI) o TMap u (preinitialObj PI))
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
98 ≈⟨ assoc ⟩
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
99 (TMap u c o ( p o ( preinitialArrow PI {k1} ))) o TMap u (preinitialObj PI)
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
100 ≈↑⟨ car ( full→ SFS ) ⟩
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
101 FMap F (FMap← (TMap u c o p o preinitialArrow PI)) o TMap u (preinitialObj PI)
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
102 ≈⟨ nat u ⟩
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
103 TMap u c o FMap (K A A a00) (FMap← (TMap u c o p o preinitialArrow PI))
441
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
104 ≈⟨⟩
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
105 TMap u c o id1 A a00
441
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
106 ≈⟨ idR ⟩
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
107 TMap u c
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
108 ∎
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
109 kfuc=1 : {k1 : Obj A} → {p : Hom A k1 a00} → A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a00 ]
439
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 438
diff changeset
110 kfuc=1 {k1} {p} = e=id ( kfuc=uc )
435
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
111 -- if equalizer has right inverse, f = g
438
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
112 lemma2 : (a b : Obj A) {c : Obj A} ( f g : Hom A a b )
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 442
diff changeset
113 {e : Hom A c a } {e' : Hom A a c } ( equ : IsEqualizer A e f g ) (inv-e : A [ A [ e o e' ] ≈ id1 A a ] )
442
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
114 → A [ f ≈ g ]
438
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
115 lemma2 a b {c} f g {e} {e'} equ inv-e = let open ≈-Reasoning (A) in
435
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
116 let open Equalizer in
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
117 begin
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
118 f
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
119 ≈↑⟨ idR ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
120 f o id1 A a
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
121 ≈↑⟨ cdr inv-e ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
122 f o ( e o e' )
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
123 ≈⟨ assoc ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
124 ( f o e ) o e'
441
61550782be4a preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
125 ≈⟨ car ( fe=ge equ ) ⟩ ( g o e ) o e'
435
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
126 ≈↑⟨ assoc ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
127 g o ( e o e' )
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
128 ≈⟨ cdr inv-e ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
129 g o id1 A a
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
130 ≈⟨ idR ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
131 g
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
132 ∎
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
133 lemma1 : (a : Obj A) (f' : Hom A a00 a) → A [ f' ≈ initialArrow a ]
438
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
134 lemma1 a f' = let open ≈-Reasoning (A) in
436
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
135 sym (
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
136 begin
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
137 initialArrow a
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
138 ≈⟨⟩
440
ff36c500962e fix limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 439
diff changeset
139 preinitialArrow PI {a} o f
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
140 ≈⟨ lemma2 a00 a (A [ preinitialArrow PI {a} o f ]) f' {ee {a00} {a} {A [ preinitialArrow PI {a} o f ]} {f'} } (equ-fi )
442
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 441
diff changeset
141 (kfuc=1 {ep} {ee} ) ⟩
438
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
142 f'
436
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
143 ∎ )
435
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
144
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
145
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
146