Mercurial > hg > Members > kono > Proof > category
annotate freyd1.agda @ 493:de9ce7e0d97c
on going using limit-uniquness directly
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 14 Mar 2017 11:43:46 +0900 |
parents | c7b8017bcd4d |
children | ba6a67523523 |
rev | line source |
---|---|
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Category -- https://github.com/konn/category-agda |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Level |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 module freyd1 {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 ( F : Functor A C ) ( G : Functor A C ) where |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import cat-utility |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import HomReasoning |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open Functor |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 open import Comma1 F G |
492 | 12 -- open import freyd CommaCategory -- we don't need this yet |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 |
492 | 14 open import Category.Cat -- Functor composition |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 open NTrans |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 open Complete |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 open CommaObj |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 open CommaHom |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 open Limit |
487 | 20 open IsLimit |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 |
493
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
22 -- |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
23 -- |
483 | 24 -- F : A → C |
25 -- G : A → C | |
26 -- | |
493
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
27 -- if A is complete and G preserve limit, Comma Category F↓G is complete |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
28 -- i.e. it has limit for Γ : I → F↓G |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
29 -- |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
30 -- |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
31 -- |
483 | 32 |
493
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
33 --- Get a functor Functor I A from a functor I CommaCategory |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
34 --- |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 FIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I A |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 FIA {I} Γ = record { |
482 | 37 FObj = λ x → obj (FObj Γ x ) ; |
38 FMap = λ {a} {b} f → arrow (FMap Γ f ) ; | |
39 isFunctor = record { | |
40 identity = identity | |
41 ; distr = IsFunctor.distr (isFunctor Γ) | |
42 ; ≈-cong = IsFunctor.≈-cong (isFunctor Γ) | |
43 }} where | |
44 identity : {x : Obj I } → A [ arrow (FMap Γ (id1 I x)) ≈ id1 A (obj (FObj Γ x)) ] | |
45 identity {x} = let open ≈-Reasoning (A) in begin | |
46 arrow (FMap Γ (id1 I x)) | |
47 ≈⟨ IsFunctor.identity (isFunctor Γ) ⟩ | |
48 id1 A (obj (FObj Γ x)) | |
49 ∎ | |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 |
493
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
51 Γa : { I : Category c₁ c₂ ℓ } → ( a : Obj A) → Functor I A |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
52 Γa a = record { |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
53 FObj = λ x → a ; |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
54 FMap = λ {x} {y} f → id1 A a ; |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
55 isFunctor = record { |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
56 identity = let open ≈-Reasoning (A) in refl-hom |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
57 ; distr = let open ≈-Reasoning (A) in sym ( idL ) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
58 ; ≈-cong = λ _ → let open ≈-Reasoning (A) in refl-hom |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
59 }} where |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
60 |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
61 --- Get a nat on A from a nat on CommaCategory |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
62 -- |
491
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
63 NIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
64 (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ ) → NTrans I A ( K A I (obj c) ) (FIA Γ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
65 NIA {I} Γ c ta = record { |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
66 TMap = λ x → arrow (TMap ta x ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
67 ; isNTrans = record { commute = comm1 } |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
68 } where |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
69 comm1 : {a b : Obj I} {f : Hom I a b} → |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
70 A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K A I (obj c)) f ] ] |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
71 comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
72 |
485 | 73 |
487 | 74 open LimitPreserve |
483 | 75 |
493
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
76 -- Limit on A from Γ : I → CommaCategory |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
77 -- |
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
483
diff
changeset
|
78 LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) |
485 | 79 → ( Γ : Functor I CommaCategory ) |
487 | 80 → ( glimit : LimitPreserve A I C G ) |
491
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
81 → Limit C I (G ○ (FIA Γ)) |
492 | 82 LimitC {I} comp Γ glimit = plimit glimit (climit comp (FIA Γ)) |
486
56cf6581c5f6
add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
485
diff
changeset
|
83 |
489 | 84 frev : { I : Category c₁ c₂ ℓ } → (comp : Complete A I) → ( Γ : Functor I CommaCategory ) (i : Obj I ) → Hom A (limit-c comp (FIA Γ)) (obj (FObj Γ i)) |
85 frev comp Γ i = TMap (t0 ( climit comp (FIA Γ))) i | |
86 | |
87 tu : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) | |
491
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
88 → NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (G ○ (FIA Γ)) |
489 | 89 tu {I} comp Γ = record { |
493
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
90 TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ] |
489 | 91 ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } |
92 } where | |
93 commute : {a b : Obj I} {f : Hom I a b} → | |
491
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
94 C [ C [ FMap (G ○ (FIA Γ)) f o C [ hom (FObj Γ a) o FMap F (frev comp Γ a) ] ] |
489 | 95 ≈ C [ C [ hom (FObj Γ b) o FMap F (frev comp Γ b) ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ] |
96 commute {a} {b} {f} = let open ≈-Reasoning (C) in begin | |
491
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
97 FMap (G ○ (FIA Γ)) f o ( hom (FObj Γ a) o FMap F (frev comp Γ a) ) |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
98 ≈⟨⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
99 FMap G (arrow (FMap Γ f ) ) o ( hom (FObj Γ a) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a )) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
100 ≈⟨ assoc ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
101 (FMap G (arrow (FMap Γ f ) ) o hom (FObj Γ a)) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a ) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
102 ≈⟨ car ( comm (FMap Γ f)) ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
103 (hom (FObj Γ b) o FMap F (arrow (FMap Γ f)) ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a ) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
104 ≈↑⟨ assoc ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
105 hom (FObj Γ b) o ( FMap F (arrow (FMap Γ f)) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a ) ) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
106 ≈↑⟨ cdr (distr F) ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
107 hom (FObj Γ b) o ( FMap F (A [ arrow (FMap Γ f) o TMap (t0 ( climit comp (FIA Γ))) a ] ) ) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
108 ≈⟨⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
109 hom (FObj Γ b) o ( FMap F (A [ FMap (FIA Γ) f o TMap (t0 ( climit comp (FIA Γ))) a ] ) ) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
110 ≈⟨ cdr ( fcong F ( IsNTrans.commute (isNTrans (t0 ( climit comp (FIA Γ))) ))) ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
111 hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o FMap (K A I (a0 (climit comp (FIA Γ)))) f ] )) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
112 ≈⟨⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
113 hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o id1 A (limit-c comp (FIA Γ)) ] )) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
114 ≈⟨ cdr ( distr F ) ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
115 hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o FMap F (id1 A (limit-c comp (FIA Γ)))) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
116 ≈⟨ cdr ( cdr ( IsFunctor.identity (isFunctor F) ) ) ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
117 hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o id1 C (FObj F (limit-c comp (FIA Γ)))) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
118 ≈⟨ assoc ⟩ |
489 | 119 ( hom (FObj Γ b) o FMap F (frev comp Γ b)) o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
120 ∎ |
489 | 121 limitHom : { I : Category c₁ c₂ ℓ } → (comp : Complete A I) → ( Γ : Functor I CommaCategory ) |
122 → ( glimit : LimitPreserve A I C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) )) | |
123 limitHom comp Γ glimit = limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) | |
124 | |
125 commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) | |
126 → ( glimit : LimitPreserve A I C G ) | |
127 → Obj CommaCategory | |
128 commaLimit {I} comp Γ glimit = record { | |
129 obj = limit-c comp (FIA Γ) | |
130 ; hom = limitHom comp Γ glimit | |
131 } | |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
132 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
133 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
134 commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
135 → ( glimit : LimitPreserve A I C G ) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
136 → NTrans I CommaCategory (K CommaCategory I (commaLimit {I} comp Γ glimit)) Γ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
137 commaNat {I} comp Γ glimit = record { |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
138 TMap = λ x → record { |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
139 arrow = TMap ( limit-u comp (FIA Γ ) ) x |
489 | 140 ; comm = comm1 x |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
141 } |
489 | 142 ; isNTrans = record { commute = comm2 } |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
143 } where |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
144 comm1 : (x : Obj I ) → |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
145 C [ C [ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) ] |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
146 ≈ C [ hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) ] ] |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
147 comm1 x = let open ≈-Reasoning (C) in begin |
489 | 148 FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) |
149 ≈⟨⟩ | |
150 FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (commaLimit comp Γ glimit) | |
151 ≈⟨⟩ | |
152 FMap G (TMap (limit-u comp (FIA Γ)) x) o limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) | |
153 ≈⟨⟩ | |
154 TMap (t0 ( LimitC comp Γ glimit )) x o limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) | |
155 ≈⟨ t0f=t ( isLimit ( LimitC comp Γ glimit ) ) ⟩ | |
156 TMap (tu comp Γ) x | |
157 ≈⟨⟩ | |
158 hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) | |
159 ∎ | |
160 comm2 : {a b : Obj I} {f : Hom I a b} → | |
161 CommaCategory [ CommaCategory [ FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } ] | |
162 ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f ] ] | |
490 | 163 comm2 {a} {b} {f} = let open ≈-Reasoning (A) in begin |
164 FMap (FIA Γ) f o TMap (limit-u comp (FIA Γ)) a | |
165 ≈⟨ IsNTrans.commute (isNTrans (limit-u comp (FIA Γ))) ⟩ | |
166 TMap (limit-u comp (FIA Γ)) b o FMap (K A I (limit-c comp (FIA Γ))) f | |
489 | 167 ∎ |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
168 |
493
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
169 gnat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
170 → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) → |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
171 NTrans I C (K C I (FObj F (obj a))) (G ○ FIA Γ) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
172 gnat {I} comp Γ glimit a t = record { |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
173 TMap = ? |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
174 ; isNTrans = record { commute = ? } |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
175 } |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
176 |
491
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
177 comma-a0 : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
178 → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
179 comma-a0 {I} comp Γ glimit a t = record { |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
180 arrow = limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
181 ; comm = comm1 |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
182 } where |
493
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
183 tcomm : { x y : Obj I } { f : Hom I x y} → A [ A [ FMap (FIA Γ) f o TMap (NIA Γ a t) x ] ≈ A [ TMap (NIA Γ a t) y o id1 A (obj a) ] ] |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
184 tcomm {x} {y} {f} = ( IsNTrans.commute ( isNTrans t )) {x} {y} {f} |
491
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
185 comm1 : C [ C [ FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a ] |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
186 ≈ C [ hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ] ] |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
187 comm1 = let open ≈-Reasoning (C) in begin |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
188 FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
189 ≈⟨ {!!} ⟩ |
493
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
190 limit (isLimit (LimitC comp Γ glimit )) (FObj F (obj a)) {!!} |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
191 ≈⟨ limit-uniqueness (isLimit (LimitC comp Γ glimit )) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
192 (limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
193 o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
194 ) ( λ {i} → begin |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
195 TMap (t0 (LimitC comp Γ glimit )) i o |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
196 ( limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
197 o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
198 ≈⟨ assoc ⟩ |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
199 ( TMap (t0 (LimitC comp Γ glimit )) i o |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
200 ( limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) )) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
201 o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
202 ≈⟨ car ( t0f=t ( isLimit (LimitC comp Γ glimit )) ) ⟩ |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
203 TMap (tu comp Γ ) i o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
204 ≈⟨⟩ |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
205 ( hom ( FObj Γ i ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
206 o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
207 ≈↑⟨ assoc ⟩ |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
208 hom ( FObj Γ i ) o |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
209 ((FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
210 ≈↑⟨ cdr ( distr F ) ⟩ |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
211 hom ( FObj Γ i ) o |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
212 FMap F ( A [ TMap (t0 ( climit comp (FIA Γ))) i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] ) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
213 ≈⟨ cdr ( fcong F ( t0f=t (isLimit (climit comp (FIA Γ))))) ⟩ |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
214 hom ( FObj Γ i ) o FMap F ( TMap {!!} i ) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
215 ≈⟨ {!!} ⟩ |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
216 TMap {!!} i |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
217 ∎ |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
218 ) ⟩ |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
219 limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) |
de9ce7e0d97c
on going using limit-uniquness directly
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
492
diff
changeset
|
220 o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) |
491
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
221 ≈⟨⟩ |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
222 hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
223 ∎ |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
224 |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
225 comma-t0f=t : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
226 → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) (i : Obj I ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
227 → CommaCategory [ CommaCategory [ TMap (commaNat comp Γ glimit) i o comma-a0 comp Γ glimit a t ] ≈ TMap t i ] |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
228 comma-t0f=t {I} comp Γ glimit a t i = let open ≈-Reasoning (A) in begin |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
229 TMap ( limit-u comp (FIA Γ ) ) i o limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
230 ≈⟨ t0f=t (isLimit ( climit comp (FIA Γ) ) ) ⟩ |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
231 TMap (NIA {I} Γ a t ) i |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
232 ∎ |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
233 |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
234 comma-uniqueness : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
235 → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
236 → ( f : Hom CommaCategory a (commaLimit comp Γ glimit)) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
237 → ( ∀ { i : Obj I } → CommaCategory [ CommaCategory [ TMap ( commaNat { I} comp Γ glimit ) i o f ] ≈ TMap t i ] ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
238 → CommaCategory [ comma-a0 comp Γ glimit a t ≈ f ] |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
239 comma-uniqueness {I} comp Γ glimit a t f t=f = let open ≈-Reasoning (A) in begin |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
240 limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
241 ≈⟨ limit-uniqueness (isLimit ( climit comp (FIA Γ) ) ) (arrow f) t=f ⟩ |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
242 arrow f |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
243 ∎ |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
244 |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
245 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
246 → ( glimit : LimitPreserve A I C G ) |
485 | 247 → ( Γ : Functor I CommaCategory ) |
248 → Limit CommaCategory I Γ | |
249 hasLimit {I} comp glimit Γ = record { | |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
250 a0 = commaLimit {I} comp Γ glimit ; |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
251 t0 = commaNat { I} comp Γ glimit ; |
487 | 252 isLimit = record { |
491
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
253 limit = λ a t → comma-a0 comp Γ glimit a t ; |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
254 t0f=t = λ {a t i } → comma-t0f=t comp Γ glimit a t i ; |
04da2c458d44
comma-a0 commuativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
490
diff
changeset
|
255 limit-uniqueness = λ {a} {t} f t=f → comma-uniqueness {I} comp Γ glimit a t f t=f |
487 | 256 } |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
257 } |