### view limit-to.agda @ 790:1e7319868d77

Sets is CCC
author Shinji KONO Fri, 19 Apr 2019 23:42:19 +0900 06388660995b 472a615c6e09
line wrap: on
line source
```
open import Category -- https://github.com/konn/category-agda
open import Level

module limit-to where

open import cat-utility
open import HomReasoning
open import Relation.Binary.Core

open import discrete

---  Equalizer  from Limit ( 2→A IdnexFunctor Γ and  IndexNat :  K →　Γ)
---
---
---                     f
---          e       -----→
---     c -----→  a         b     A
---     ^      /     -----→
---     |k   h          g
---     |   /
---     |  /            ^
---     | /             |
---     |/              | Γ
---     d _             |
---      |\             |
---        \ K          af
---         \       -----→
---          \    t0        t1    I
---                  -----→
---                     ag
---
---

open Complete
open Limit
open IsLimit
open NTrans

-- Functor Γ : TwoCat → A

IndexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat  {c₁} {c₂}) A
IndexFunctor  {c₁} {c₂} {ℓ} A a b f g = record {
FObj = λ a → fobj a
; FMap = λ {a} {b} f → fmap {a} {b} f
; isFunctor = record {
identity = λ{x} → identity x
; distr = λ {a} {b} {c} {f} {g}   → distr1 {a} {b} {c} {f} {g}
; ≈-cong = λ {a} {b} {c} {f}   → ≈-cong  {a} {b} {c} {f}
}
} where
T = TwoCat   {c₁} {c₂}
fobj :  Obj T → Obj A
fobj t0 = a
fobj t1 = b
fmap :  {x y : Obj T } →  (Hom T x y  ) → Hom A (fobj x) (fobj y)
fmap  {t0} {t0} id-t0 = id1 A a
fmap  {t1} {t1} id-t1 = id1 A b
fmap  {t0} {t1} arrow-f = f
fmap  {t0} {t1} arrow-g = g
≈-cong :  {a : Obj T} {b : Obj T} {f g : Hom T a b}  → T [ f ≈ g ]  → A [ fmap f ≈ fmap g ]
≈-cong  {a} {b} {f} {.f} refl = let open  ≈-Reasoning A in refl-hom
identity : (x : Obj T ) →  A [ fmap (id1 T x) ≈  id1 A (fobj x) ]
identity t0  = let open  ≈-Reasoning A in refl-hom
identity t1  = let open  ≈-Reasoning A in refl-hom
distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} →
A [ fmap (T [ g o f ])  ≈  A [ fmap g o fmap f ] ]
distr1  {t0} {t0} {t0} {id-t0 } { id-t0 } = let open  ≈-Reasoning A in sym-hom idL
distr1  {t1} {t1} {t1} { id-t1 } { id-t1 } = let open  ≈-Reasoning A in begin
id b
≈↑⟨ idL ⟩
id b o id b
∎
distr1  {t0} {t0} {t1} { id-t0 } { arrow-f } = let open  ≈-Reasoning A in begin
fmap (T [ arrow-f  o id-t0 ] )
≈⟨⟩
fmap arrow-f
≈↑⟨ idR ⟩
fmap arrow-f o id a
∎
distr1  {t0} {t0} {t1}  { id-t0 } { arrow-g } = let open  ≈-Reasoning A in begin
fmap (T [ arrow-g  o id-t0 ] )
≈⟨⟩
fmap arrow-g
≈↑⟨ idR ⟩
fmap arrow-g o id a
∎
distr1  {t0} {t1} {t1}  { arrow-f } { id-t1 } = let open  ≈-Reasoning A in begin
fmap (T [ id-t1  o arrow-f ] )
≈⟨⟩
fmap arrow-f
≈↑⟨ idL ⟩
id b o  fmap arrow-f
∎
distr1  {t0} {t1} {t1} { arrow-g } { id-t1 } = let open  ≈-Reasoning A in begin
fmap (T [ id-t1  o arrow-g ] )
≈⟨⟩
fmap arrow-g
≈↑⟨ idL ⟩
id b o  fmap arrow-g
∎

--- Nat for Limit
--
--     Nat : K → IndexFunctor
--

open Functor

IndexNat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
→  {a b : Obj A}      (f g : Hom A  a b )
(d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   →
NTrans TwoCat  A (K TwoCat A d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)
IndexNat {c₁} {c₂} {ℓ} A {a} {b} f g d h fh=gh = record {
TMap = λ x → nmap x d h ;
isNTrans = record {
commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh
}
} where
I = TwoCat  {c₁} {c₂}
Γ : Functor I A
Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g
nmap :  (x : Obj I ) ( d : Obj (A)  ) (h : Hom A d a ) → Hom A (FObj (K I A d) x) (FObj Γ x)
nmap t0 d h = h
nmap t1 d h = A [ f o  h ]
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 ] ]
→ A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K I A d) f' ] ]
commute1  {t0} {t1} {arrow-f}  d h fh=gh =  let open  ≈-Reasoning A in begin
f o h
≈↑⟨ idR ⟩
(f o h ) o id d
∎
commute1  {t0} {t1} {arrow-g}  d h fh=gh =  let open  ≈-Reasoning A in begin
g o h
≈↑⟨ fh=gh ⟩
f o h
≈↑⟨ idR ⟩
(f o h ) o id d
∎
commute1  {t0} {t0} {id-t0}  d h fh=gh =   let open  ≈-Reasoning A in begin
id a o h
≈⟨ idL ⟩
h
≈↑⟨ idR ⟩
h o id d
∎
commute1  {t1} {t1} {id-t1}  d h fh=gh =   let open  ≈-Reasoning A in begin
id b o  ( f o  h  )
≈⟨ idL ⟩
f o  h
≈↑⟨ idR ⟩
( f o  h ) o id d
∎

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) ) →
Hom A (a0 lim) a
equlimit A {a} {b} f g lim = TMap (Limit.t0 lim) discrete.t0

lim-to-equ :  {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) )
→ IsEqualizer A (equlimit A f g lim) f g
lim-to-equ {c₁} {c₂} {ℓ} A {a} {b} f g lim =  record {
fe=ge =  fe=ge0
; k = λ {d} h fh=gh → k {d} h fh=gh
; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
} where
I : Category  c₁ c₂ c₂
I = TwoCat
Γ : Functor I A
Γ = IndexFunctor A a b f g
e : Hom A (a0 lim) a
e = equlimit A f g lim
c : Obj A
c = a0 lim
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) Γ
inat = IndexNat A f g
fe=ge0 : A [ A [ f o (equlimit A f g lim ) ] ≈ A [ g o (equlimit A f g lim ) ] ]
fe=ge0 = let open  ≈-Reasoning A in  begin
f o (equlimit A f g lim )
≈⟨⟩
FMap  Γ arrow-f o TMap (Limit.t0 lim) discrete.t0
≈⟨  IsNTrans.commute ( isNTrans (Limit.t0 lim)) {discrete.t0} {discrete.t1} {arrow-f} ⟩
TMap (Limit.t0 lim) discrete.t1 o FMap (K (TwoCat {c₁} {c₂} ) A (a0 lim)) id-t0
≈↑⟨ IsNTrans.commute ( isNTrans (Limit.t0 lim)) {discrete.t0} {discrete.t1} {arrow-g} ⟩
FMap  Γ arrow-g o TMap (Limit.t0 lim) discrete.t0
≈⟨⟩
g o (equlimit A f g lim )
∎
k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
k {d} h fh=gh  =  limit (isLimit lim) d (inat d h fh=gh )
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 ]
ek=h d h fh=gh = let open  ≈-Reasoning A in  begin
e o k h fh=gh
≈⟨⟩
TMap (Limit.t0 lim) discrete.t0  o k h fh=gh
≈⟨ t0f=t (isLimit lim) {d} {inat d h fh=gh } {discrete.t0}  ⟩
TMap (inat d h fh=gh) discrete.t0
≈⟨⟩
h
∎
uniq-nat :  {i : Obj I} →  (d : Obj A )  (h : Hom A d a ) ( k' : Hom A d c )
( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ]) → A [ A [ e o k' ] ≈ h ] →
A [ A [ TMap (Limit.t0 lim) i o k' ] ≈ TMap (inat d h fh=gh) i ]
uniq-nat {t0} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
TMap (Limit.t0 lim) discrete.t0 o k'
≈⟨⟩
e o k'
≈⟨ ek'=h ⟩
h
≈⟨⟩
TMap (inat d h fh=gh) discrete.t0
∎
uniq-nat {t1} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
TMap (Limit.t0 lim) t1 o k'
≈↑⟨ car (idR) ⟩
( TMap (Limit.t0 lim) t1  o  id c ) o k'
≈⟨⟩
( TMap (Limit.t0 lim) t1  o  FMap (K I A c) arrow-f ) o k'
≈↑⟨ car ( nat1 (Limit.t0 lim) arrow-f ) ⟩
( FMap Γ  arrow-f  o TMap (Limit.t0 lim) discrete.t0 ) o k'
≈⟨⟩
(f o e ) o k'
≈↑⟨ assoc ⟩
f o ( e o k' )
≈⟨ cdr  ek'=h ⟩
f o h
≈⟨⟩
TMap (inat d h fh=gh) t1
∎
uniquness :  (d : Obj A ) (h : Hom A d a ) →  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  →
( k' : Hom A d c )
→ A [ A [ e o k' ] ≈ h ] → A [ k h  fh=gh   ≈ k' ]
uniquness d h fh=gh k' ek'=h =  let open  ≈-Reasoning A in  begin
k h fh=gh
≈⟨ limit-uniqueness (isLimit lim) ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
k'
∎

---  Product  from Limit ( given Discrete→A functor Γ and  pnat :  K →　Γ)

open DiscreteHom

plimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set  c₁)
→  ( Γ : Functor (DiscreteCat  S ) A ) → (lim : Limit ( DiscreteCat  S ) A Γ )  → Obj A
plimit A S Γ lim = a0 lim

discrete-identity : { c₁ : Level} { S : Set c₁} { a : S } → (f : DiscreteHom a a ) →  (DiscreteCat S)  [ f  ≈  id1 (DiscreteCat S) a ]
discrete-identity  f =   refl

pnat :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  (S : Set  c₁)
→ (Γ : Functor (DiscreteCat S) A )
→  {q : Obj A }  ( qi : (i : Obj ( DiscreteCat  S)) → Hom A q (FObj Γ i) )
→ NTrans (DiscreteCat S )A (K (DiscreteCat S) A q) Γ
pnat  A S Γ {q} qi  = record {
TMap = qi ;
isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
} where
commute :  {a b : Obj (DiscreteCat  S) } {f : Hom (DiscreteCat S)  a b} →
A [ A [ FMap Γ f o qi a ] ≈ A [ qi  b o FMap (K (DiscreteCat  S) A q) f ] ]
commute {a} {b} {f} with discrete f
commute {a} {.a} {f} | refl =  let open  ≈-Reasoning A in  begin
FMap Γ f o qi a
≈⟨ car ( fcong Γ (discrete-identity f )) ⟩
FMap Γ (id1 (DiscreteCat S) a ) o qi a
≈⟨ car ( IsFunctor.identity (isFunctor Γ) ) ⟩
id1 A (FObj Γ a)  o qi a
≈⟨ idL ⟩
qi  a
≈↑⟨ idR ⟩
qi  a o id q
≈⟨⟩
qi  a o FMap (K (DiscreteCat S) A q) f
∎

lim-to-product :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( S : Set  c₁ )
→  ( Γ : Functor (DiscreteCat S) A )     -- could be constructed from S → Obj A
→ (lim : Limit (DiscreteCat S) A Γ )
→ IProduct  (Obj (DiscreteCat S))  A (FObj Γ)
lim-to-product A S Γ lim = record {
iprod = plimit A S Γ lim
; pi =  λ  i →   TMap (Limit.t0 lim) i
; isIProduct =  record {
iproduct = λ {q} qi → iproduct {q} qi ;
pif=q =  λ {q} {qi} {i} → pif=q {q} qi {i}  ;
ip-uniqueness  = λ  {q } { h } → ip-uniqueness {q} {h} ;
ip-cong  =  λ {q } { qi }  { qi' } qi=qi' → ip-cong  {q} {qi} {qi'} qi=qi'
}
} where
D = DiscreteCat S
I = Obj ( DiscreteCat S )
ai = λ i → FObj Γ i
p = a0 lim
pi =  λ i → TMap (Limit.t0 lim) i
iproduct : {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
iproduct {q} qi = limit (isLimit lim) q (pnat A S Γ qi )
pif=q :   {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i )  o ( iproduct qi ) ] ≈  (qi i) ]
pif=q {q} qi {i} = t0f=t (isLimit lim)  {q} {pnat A S Γ qi } {i}
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 ] ]
ipu {i} q h = let open  ≈-Reasoning A in  refl-hom
ip-uniqueness :  {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) →  A [ (pi i)  o h ] )  ≈  h ]
ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i  o h ]  )} (ipu q h)
ipc : {q : Obj A}   → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
→ (i : I ) →  A [ qi i ≈ qi' i ]  →
A [ A [ TMap (Limit.t0 lim) i o iproduct qi' ] ≈ TMap (pnat A S Γ qi) i ]
ipc {q} {qi} {qi'} i qi=qi' = let open  ≈-Reasoning A in begin
TMap (Limit.t0 lim) i o iproduct qi'
≈⟨⟩
TMap (Limit.t0 lim) i o limit (isLimit lim) q (pnat A S Γ qi' )
≈⟨ t0f=t (isLimit lim) {q} {pnat A S Γ qi'} {i} ⟩
TMap (pnat A S Γ qi') i
≈⟨⟩
qi' i
≈↑⟨ qi=qi' ⟩
qi i
≈⟨⟩
TMap (pnat A S Γ qi) i
∎
ip-cong : {q : Obj A}   → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
→ ( ∀ (i : I ) →  A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ]
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))
```