Mercurial > hg > Members > kono > Proof > category

annotate src/limit-to.agda @ 1110:45de2b31bf02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add original library and fix for safe mode
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 07 Oct 2023 19:43:31 +0900
parents ac53803b3b2a
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1110
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
1 {-# OPTIONS --cubical-compatible --safe #-}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
2
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
3 open import Category -- https://github.com/konn/category-agda
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Level
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
403
375edfefbf6a maybe CAT
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 402
diff changeset
6 module limit-to where
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
1110
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
8 open import Definitions
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import HomReasoning
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Binary.Core
796
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 778
diff changeset
11 open import Relation.Binary.PropositionalEquality hiding ([_])
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 778
diff changeset
12
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
825
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
14 open import graph
427
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
15
365
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
16
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
17 --- Equalizer from Limit ( 2→A IdnexFunctor Γ and IndexNat : K →　Γ)
458
fd79b6d9f350 fix comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 457
diff changeset
18 ---
fd79b6d9f350 fix comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 457
diff changeset
19 ---
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
20 --- f
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
21 --- e -----→
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
22 --- c -----→ a b A
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
23 --- ^ / -----→
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
24 --- |k h g
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
25 --- | /
426
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
26 --- | / ^
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
27 --- | / |
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
28 --- |/ | Γ
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
29 --- d _ |
432
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
30 --- |\ |
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
31 --- \ K af
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
32 --- \ -----→
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
33 --- \ t0 t1 I
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
34 --- -----→
426
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
35 --- ag
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
36 ---
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
37 ---
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
38
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
39 open Complete
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 open Limit
487
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
41 open IsLimit
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
42 open NTrans
352
f589e71875ea bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 351
diff changeset
43
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
44 -- Functor Γ : TwoCat → A
424
4329525f5085 fix imit-to-edu for MaybeCat / TwoCat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 423
diff changeset
45
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 796
diff changeset
46 IndexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat ) A
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
47 IndexFunctor {c₁} {c₂} {ℓ} A a b f g = record {
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
48 FObj = λ a → fobj a
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
49 ; FMap = λ {a} {b} f → fmap {a} {b} f
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
50 ; isFunctor = record {
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
51 identity = λ{x} → identity x
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
52 ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g}
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
53 ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f}
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
54 }
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
55 } where
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 796
diff changeset
56 T = TwoCat
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
57 fobj : Obj T → Obj A
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
58 fobj t0 = a
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
59 fobj t1 = b
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
60 fmap : {x y : Obj T } → (Hom T x y ) → Hom A (fobj x) (fobj y)
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
61 fmap {t0} {t0} id-t0 = id1 A a
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
62 fmap {t1} {t1} id-t1 = id1 A b
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
63 fmap {t0} {t1} arrow-f = f
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
64 fmap {t0} {t1} arrow-g = g
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
65 ≈-cong : {a : Obj T} {b : Obj T} {f g : Hom T a b} → T [ f ≈ g ] → A [ fmap f ≈ fmap g ]
796
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 778
diff changeset
66 ≈-cong {a} {b} {f} {_} refl = let open ≈-Reasoning A in refl-hom
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
67 identity : (x : Obj T ) → A [ fmap (id1 T x) ≈ id1 A (fobj x) ]
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
68 identity t0 = let open ≈-Reasoning A in refl-hom
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
69 identity t1 = let open ≈-Reasoning A in refl-hom
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
70 distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} →
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
71 A [ fmap (T [ g o f ]) ≈ A [ fmap g o fmap f ] ]
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
72 distr1 {t0} {t0} {t0} {id-t0 } { id-t0 } = let open ≈-Reasoning A in sym-hom idL
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
73 distr1 {t1} {t1} {t1} { id-t1 } { id-t1 } = let open ≈-Reasoning A in begin
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
74 id b
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
75 ≈↑⟨ idL ⟩
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
76 id b o id b
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
77 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
78 distr1 {t0} {t0} {t1} { id-t0 } { arrow-f } = let open ≈-Reasoning A in begin
462
e618db534987 clean up fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
79 fmap (T [ arrow-f o id-t0 ] )
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
80 ≈⟨⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
81 fmap arrow-f
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
82 ≈↑⟨ idR ⟩
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
83 fmap arrow-f o id a
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
84 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
85 distr1 {t0} {t0} {t1} { id-t0 } { arrow-g } = let open ≈-Reasoning A in begin
462
e618db534987 clean up fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
86 fmap (T [ arrow-g o id-t0 ] )
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
87 ≈⟨⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
88 fmap arrow-g
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
89 ≈↑⟨ idR ⟩
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
90 fmap arrow-g o id a
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
91 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
92 distr1 {t0} {t1} {t1} { arrow-f } { id-t1 } = let open ≈-Reasoning A in begin
462
e618db534987 clean up fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
93 fmap (T [ id-t1 o arrow-f ] )
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
94 ≈⟨⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
95 fmap arrow-f
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
96 ≈↑⟨ idL ⟩
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
97 id b o fmap arrow-f
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
98 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
99 distr1 {t0} {t1} {t1} { arrow-g } { id-t1 } = let open ≈-Reasoning A in begin
462
e618db534987 clean up fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
100 fmap (T [ id-t1 o arrow-g ] )
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
101 ≈⟨⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
102 fmap arrow-g
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
103 ≈↑⟨ idL ⟩
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
104 id b o fmap arrow-g
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
105 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
106
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
107 --- Nat for Limit
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
108 --
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
109 -- Nat : K → IndexFunctor
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
110 --
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
111
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
112 open Functor
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
113
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
114 IndexNat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
115 → {a b : Obj A} (f g : Hom A a b )
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
116 (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] →
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
117 NTrans TwoCat A (K TwoCat A d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
118 IndexNat {c₁} {c₂} {ℓ} A {a} {b} f g d h fh=gh = record {
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
119 TMap = λ x → nmap x d h ;
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
120 isNTrans = record {
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
121 commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
122 }
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
123 } where
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 796
diff changeset
124 I = TwoCat
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
125 Γ : Functor I A
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
126 Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
127 nmap : (x : Obj I ) ( d : Obj (A) ) (h : Hom A d a ) → Hom A (FObj (K I A d) x) (FObj Γ x)
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
128 nmap t0 d h = h
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
129 nmap t1 d h = A [ f o h ]
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
130 commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ]
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
131 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K I A d) f' ] ]
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
132 commute1 {t0} {t1} {arrow-f} d h fh=gh = let open ≈-Reasoning A in begin
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
133 f o h
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
134 ≈↑⟨ idR ⟩
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
135 (f o h ) o id d
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
136 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
137 commute1 {t0} {t1} {arrow-g} d h fh=gh = let open ≈-Reasoning A in begin
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
138 g o h
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
139 ≈↑⟨ fh=gh ⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
140 f o h
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
141 ≈↑⟨ idR ⟩
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
142 (f o h ) o id d
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
143 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
144 commute1 {t0} {t0} {id-t0} d h fh=gh = let open ≈-Reasoning A in begin
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
145 id a o h
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
146 ≈⟨ idL ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
147 h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
148 ≈↑⟨ idR ⟩
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
149 h o id d
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
150 ∎
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
151 commute1 {t1} {t1} {id-t1} d h fh=gh = let open ≈-Reasoning A in begin
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
152 id b o ( f o h )
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
153 ≈⟨ idL ⟩
428
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
154 f o h
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
155 ≈↑⟨ idR ⟩
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
156 ( f o h ) o id d
428
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
157 ∎
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
158
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
159
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
160 equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} → (f g : Hom A a b) (lim : Limit TwoCat A (IndexFunctor A a b f g) ) →
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
161 Hom A (a0 lim) a
825
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
162 equlimit A {a} {b} f g lim = TMap (Limit.t0 lim) graph.t0
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
163
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
164 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
165 → {a b : Obj A} (f g : Hom A a b )
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
166 (lim : Limit TwoCat A (IndexFunctor A a b f g) )
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
167 → IsEqualizer A (equlimit A f g lim) f g
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
168 lim-to-equ {c₁} {c₂} {ℓ} A {a} {b} f g lim = record {
601
2e7b5a777984 prove fe=ge in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
169 fe=ge = fe=ge0
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
170 ; k = λ {d} h fh=gh → k {d} h fh=gh
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
171 ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
172 ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
173 } where
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 796
diff changeset
174 I : Category Level.zero Level.zero Level.zero
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
175 I = TwoCat
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
176 Γ : Functor I A
461
8436a018f88a clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
177 Γ = IndexFunctor A a b f g
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
178 e : Hom A (a0 lim) a
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
179 e = equlimit A f g lim
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
180 c : Obj A
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
181 c = a0 lim
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
182 inat : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K I A d) Γ
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
183 inat = IndexNat A f g
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
184 fe=ge0 : A [ A [ f o (equlimit A f g lim ) ] ≈ A [ g o (equlimit A f g lim ) ] ]
601
2e7b5a777984 prove fe=ge in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
185 fe=ge0 = let open ≈-Reasoning A in begin
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
186 f o (equlimit A f g lim )
601
2e7b5a777984 prove fe=ge in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
187 ≈⟨⟩
825
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
188 FMap Γ arrow-f o TMap (Limit.t0 lim) graph.t0
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
189 ≈⟨ IsNTrans.commute ( isNTrans (Limit.t0 lim)) {graph.t0} {graph.t1} {arrow-f} ⟩
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
190 TMap (Limit.t0 lim) graph.t1 o FMap (K (TwoCat ) A (a0 lim)) id-t0
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
191 ≈↑⟨ IsNTrans.commute ( isNTrans (Limit.t0 lim)) {graph.t0} {graph.t1} {arrow-g} ⟩
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
192 FMap Γ arrow-g o TMap (Limit.t0 lim) graph.t0
601
2e7b5a777984 prove fe=ge in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
193 ≈⟨⟩
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
194 g o (equlimit A f g lim )
601
2e7b5a777984 prove fe=ge in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
195 ∎
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
196 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
487
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
197 k {d} h fh=gh = limit (isLimit lim) d (inat d h fh=gh )
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
198 ek=h : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → A [ A [ e o k h fh=gh ] ≈ h ]
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
199 ek=h d h fh=gh = let open ≈-Reasoning A in begin
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
200 e o k h fh=gh
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
201 ≈⟨⟩
825
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
202 TMap (Limit.t0 lim) graph.t0 o k h fh=gh
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
203 ≈⟨ t0f=t (isLimit lim) {d} {inat d h fh=gh } {graph.t0} ⟩
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
204 TMap (inat d h fh=gh) graph.t0
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
205 ≈⟨⟩
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
206 h
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
207 ∎
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
208 uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c )
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
209 ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ]) → A [ A [ e o k' ] ≈ h ] →
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
210 A [ A [ TMap (Limit.t0 lim) i o k' ] ≈ TMap (inat d h fh=gh) i ]
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
211 uniq-nat {t0} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin
825
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
212 TMap (Limit.t0 lim) graph.t0 o k'
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
213 ≈⟨⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
214 e o k'
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
215 ≈⟨ ek'=h ⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
216 h
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
217 ≈⟨⟩
825
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
218 TMap (inat d h fh=gh) graph.t0
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
219 ∎
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
220 uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
221 TMap (Limit.t0 lim) t1 o k'
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
222 ≈↑⟨ car (idR) ⟩
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
223 ( TMap (Limit.t0 lim) t1 o id c ) o k'
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
224 ≈⟨⟩
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
225 ( TMap (Limit.t0 lim) t1 o FMap (K I A c) arrow-f ) o k'
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
226 ≈↑⟨ car ( nat1 (Limit.t0 lim) arrow-f ) ⟩
825
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
227 ( FMap Γ arrow-f o TMap (Limit.t0 lim) graph.t0 ) o k'
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
228 ≈⟨⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
229 (f o e ) o k'
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
230 ≈↑⟨ assoc ⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
231 f o ( e o k' )
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
232 ≈⟨ cdr ek'=h ⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
233 f o h
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
234 ≈⟨⟩
466
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 462
diff changeset
235 TMap (inat d h fh=gh) t1
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
236 ∎
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
237 uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) →
372
b4855a3ebd34 add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
238 ( k' : Hom A d c )
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
239 → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
240 uniquness d h fh=gh k' ek'=h = let open ≈-Reasoning A in begin
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
241 k h fh=gh
495
633df882db86 fryed1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 487
diff changeset
242 ≈⟨ limit-uniqueness (isLimit lim) ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
243 k'
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
244 ∎
368
b18585089d2e add more parameter to nat in lim-to-equ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
245
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
246
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
247 --- Product from Limit ( given Discrete→A functor Γ and pnat : K →　Γ)
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
248
796
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 778
diff changeset
249 open import Relation.Binary.PropositionalEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 778
diff changeset
250
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
251 open DiscreteHom
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
252
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
253 plimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set c₁)
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
254 → ( Γ : Functor (DiscreteCat S ) A ) → (lim : Limit ( DiscreteCat S ) A Γ ) → Obj A
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
255 plimit A S Γ lim = a0 lim
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
256
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 691
diff changeset
257 discrete-identity : { c₁ : Level} { S : Set c₁} { a : S } → (f : DiscreteHom a a ) → (DiscreteCat S) [ f ≈ id1 (DiscreteCat S) a ]
472
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
258 discrete-identity f = refl
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
259
474
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 472
diff changeset
260 pnat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set c₁)
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
261 → (Γ : Functor (DiscreteCat S) A )
474
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 472
diff changeset
262 → {q : Obj A } ( qi : (i : Obj ( DiscreteCat S)) → Hom A q (FObj Γ i) )
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
263 → NTrans (DiscreteCat S )A (K (DiscreteCat S) A q) Γ
474
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 472
diff changeset
264 pnat A S Γ {q} qi = record {
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
265 TMap = qi ;
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
266 isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
267 } where
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
268 commute : {a b : Obj (DiscreteCat S) } {f : Hom (DiscreteCat S) a b} →
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
269 A [ A [ FMap Γ f o qi a ] ≈ A [ qi b o FMap (K (DiscreteCat S) A q) f ] ]
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
270 commute {a} {b} {f} with discrete f
472
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
271 commute {a} {.a} {f} | refl = let open ≈-Reasoning A in begin
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
272 FMap Γ f o qi a
472
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
273 ≈⟨ car ( fcong Γ (discrete-identity f )) ⟩
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
274 FMap Γ (id1 (DiscreteCat S) a ) o qi a
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
275 ≈⟨ car ( IsFunctor.identity (isFunctor Γ) ) ⟩
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
276 id1 A (FObj Γ a) o qi a
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
277 ≈⟨ idL ⟩
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
278 qi a
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
279 ≈↑⟨ idR ⟩
472
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
280 qi a o id q
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
281 ≈⟨⟩
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
282 qi a o FMap (K (DiscreteCat S) A q) f
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
283 ∎
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
284
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
285 lim-to-product : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( S : Set c₁ )
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 691
diff changeset
286 → ( Γ : Functor (DiscreteCat S) A ) -- could be constructed from S → Obj A
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
287 → (lim : Limit (DiscreteCat S) A Γ )
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
288 → IProduct (Obj (DiscreteCat S)) A (FObj Γ)
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
289 lim-to-product A S Γ lim = record {
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
290 iprod = plimit A S Γ lim
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
291 ; pi = λ i → TMap (Limit.t0 lim) i
508
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 495
diff changeset
292 ; isIProduct = record {
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
293 iproduct = λ {q} qi → iproduct {q} qi ;
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 670
diff changeset
294 pif=q = λ {q} {qi} {i} → pif=q {q} qi {i} ;
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
295 ip-uniqueness = λ {q } { h } → ip-uniqueness {q} {h} ;
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
296 ip-cong = λ {q } { qi } { qi' } qi=qi' → ip-cong {q} {qi} {qi'} qi=qi'
508
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 495
diff changeset
297 }
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
298 } where
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
299 D = DiscreteCat S
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
300 I = Obj ( DiscreteCat S )
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
301 ai = λ i → FObj Γ i
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
302 p = a0 lim
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
303 pi = λ i → TMap (Limit.t0 lim) i
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
304 iproduct : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
487
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
305 iproduct {q} qi = limit (isLimit lim) q (pnat A S Γ qi )
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
306 pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( iproduct qi ) ] ≈ (qi i) ]
487
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
307 pif=q {q} qi {i} = t0f=t (isLimit lim) {q} {pnat A S Γ qi } {i}
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
308 ipu : {i : Obj D} → (q : Obj A) (h : Hom A q p ) → A [ A [ TMap (Limit.t0 lim) i o h ] ≈ A [ pi i o h ] ]
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
309 ipu {i} q h = let open ≈-Reasoning A in refl-hom
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
310 ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ]
495
633df882db86 fryed1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 487
diff changeset
311 ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i o h ] )} (ipu q h)
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
312 ipc : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
313 → (i : I ) → A [ qi i ≈ qi' i ] →
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
314 A [ A [ TMap (Limit.t0 lim) i o iproduct qi' ] ≈ TMap (pnat A S Γ qi) i ]
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
315 ipc {q} {qi} {qi'} i qi=qi' = let open ≈-Reasoning A in begin
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
316 TMap (Limit.t0 lim) i o iproduct qi'
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
317 ≈⟨⟩
670
99065a1e56ea remove comp from limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 662
diff changeset
318 TMap (Limit.t0 lim) i o limit (isLimit lim) q (pnat A S Γ qi' )
487
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
319 ≈⟨ t0f=t (isLimit lim) {q} {pnat A S Γ qi'} {i} ⟩
474
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 472
diff changeset
320 TMap (pnat A S Γ qi') i
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
321 ≈⟨⟩
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
322 qi' i
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
323 ≈↑⟨ qi=qi' ⟩
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
324 qi i
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
325 ≈⟨⟩
474
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 472
diff changeset
326 TMap (pnat A S Γ qi) i
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
327 ∎
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
328 ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
329 → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ]
495
633df882db86 fryed1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 487
diff changeset
330 ip-cong {q} {qi} {qi'} qi=qi' = limit-uniqueness (isLimit lim) {q} {pnat A S Γ qi} (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i))