### view SetsCompleteness.agda @ 790:1e7319868d77

Sets is CCC
author Shinji KONO Fri, 19 Apr 2019 23:42:19 +0900 340708e8d54f
line wrap: on
line source
```
open import Category -- https://github.com/konn/category-agda
open import Level
open import Category.Sets renaming ( _o_ to _*_ )

module SetsCompleteness where

open import cat-utility
open import Relation.Binary.Core
open import Function
import Relation.Binary.PropositionalEquality
-- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → ( λ x → f x ≡ λ x → g x )
postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂

≡cong = Relation.Binary.PropositionalEquality.cong

open import Relation.Binary.PropositionalEquality hiding ( [_] )

lemma1 :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} {f g : Hom Sets a b} →
Sets [ f ≈ g ] → (x : a ) → f x  ≡ g x
lemma1 refl  x  = refl

record Σ {a} (A : Set a) (B : Set a) : Set a where
constructor _,_
field
proj₁ : A
proj₂ : B

open Σ public

SetsProduct :  {  c₂ : Level} → ( a b : Obj (Sets  {c₂})) → Product ( Sets  {  c₂} ) a b
SetsProduct { c₂ } a b = record {
product =  Σ a b
; π1 = λ ab → (proj₁ ab)
; π2 = λ ab → (proj₂ ab)
; isProduct = record {
_×_  = λ f g  x →   record { proj₁ = f  x ;  proj₂ =  g  x }     -- ( f x ,  g x )
; π1fxg=f = refl
; π2fxg=g  = refl
; uniqueness = refl
; ×-cong   =  λ {c} {f} {f'} {g} {g'} f=f g=g →  prod-cong a b f=f g=g
}
} where
prod-cong : ( a b : Obj (Sets {c₂}) ) {c : Obj (Sets {c₂}) } {f f' : Hom Sets c a } {g g' : Hom Sets c b }
→ Sets [ f ≈ f' ] → Sets [ g ≈ g' ]
→ Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ]
prod-cong a b {c} {f} {.f} {g} {.g} refl refl = refl

record iproduct {a} (I : Set a)  ( pi0 : I → Set a ) : Set a where
field
pi1 : ( i : I ) → pi0 i

open iproduct

SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets )
→ IProduct I ( Sets  {  c₂} ) ai
SetsIProduct I fi = record {
iprod = iproduct I fi
; pi  = λ i prod  → pi1 prod i
; isIProduct = record {
iproduct = iproduct1
; pif=q = λ {q} {qi} {i} → pif=q {q} {qi} {i}
; ip-uniqueness = ip-uniqueness
; ip-cong  = ip-cong
}
} where
iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi)
iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x  }
pif=q : {q : Obj Sets} {qi : (i : I) → Hom Sets q (fi i)} → {i : I} → Sets [ Sets [ (λ prod → pi1 prod i) o iproduct1 qi ] ≈ qi i ]
pif=q {q} {qi} {i} = refl
ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ]
ip-uniqueness = refl
ipcx : {q :  Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 qi x ≡ iproduct1 qi' x
ipcx {q} {qi} {qi'} qi=qi x  =
begin
record { pi1 = λ i → (qi i) x  }
≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡cong ( λ f → f x )  (qi=qi i)  )) ⟩
record { pi1 = λ i → (qi' i) x  }
∎  where
open  import  Relation.Binary.PropositionalEquality
open ≡-Reasoning
ip-cong  : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 qi ≈ iproduct1  qi' ]
ip-cong {q} {qi} {qi'} qi=qi  = extensionality Sets ( ipcx qi=qi )

--
--         e             f
--    c  -------→ a ---------→ b        f ( f'
--    ^        .     ---------→
--    |      .            g
--    |k   .
--    |  . h
--y : d

-- cf. https://github.com/danr/Agda-projects/blob/master/Category-Theory/Equalizer.agda

data sequ {c : Level} (A B : Set c) ( f g : A → B ) :  Set c where
elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g

equ  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → ( sequ a b  f g ) →  a
equ  (elem x eq)  = x

fe=ge0  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } →
(x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x
fe=ge0 (elem x eq )  =  eq

irr : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
irr refl refl = refl

open sequ

--           equalizer-c = sequ a b f g
--          ; equalizer = λ e → equ e

SetsIsEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e) f g
SetsIsEqualizer {c₂} a b f g = record {
fe=ge  = fe=ge
; k = k
; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq}
; uniqueness  = uniqueness
} where
fe=ge  :  Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
fe=ge  =  extensionality Sets (fe=ge0 )
k :  {d : Obj Sets} (h : Hom Sets d a) → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g)
k {d} h eq = λ x → elem  (h x) ( ≡cong ( λ y → y x ) eq )
ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e )  o k h eq ] ≈ h ]
ek=h {d} {h} {eq} = refl
injection :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} (f  : Hom Sets a b) → Set c₂
injection f =  ∀ x y  → f x ≡ f y →  x  ≡ y
elm-cong :   (x y : sequ a b f g) → equ x ≡ equ y →  x  ≡ y
elm-cong ( elem x eq  ) (elem .x eq' ) refl   =  ≡cong ( λ ee → elem x ee ) ( irr eq eq' )
lemma5 :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x)
lemma5 refl  x  = refl   -- somehow this is not equal to lemma1
uniqueness :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh  ≈ k' ]
uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  extensionality Sets  ( λ ( x : d ) →  begin
k h fh=gh x
≡⟨ elm-cong ( k h fh=gh x) (  k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x )  ⟩
k' x
∎  ) where
open  import  Relation.Binary.PropositionalEquality
open ≡-Reasoning

open Functor

----
-- C is locally small i.e. Hom C i j is a set c₁
--
record Small  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )
: Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
field
hom→ : {i j : Obj C } →    Hom C i j →  I
hom← : {i j : Obj C } →  ( f : I ) →  Hom C i j
hom-iso : {i j : Obj C } →  { f : Hom C i j } →   C [ hom← ( hom→ f )  ≈ f ]
hom-rev : {i j : Obj C } →  { f : I } →   hom→ ( hom← {i} {j} f )  ≡ f
≡←≈ : {i j : Obj C } →  { f g : Hom C i j } →  C [ f ≈ g ] →   f ≡ g

open Small

ΓObj :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
(i : Obj C ) →　 Set c₁
ΓObj s  Γ i = FObj Γ i

ΓMap :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
{i j : Obj C } →　 ( f : I ) →  ΓObj s Γ i → ΓObj  s Γ j
ΓMap  s Γ {i} {j} f = FMap Γ ( hom← s f )

record snat   { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ )
( smap : { i j :  OC  }  → (f : I ) →  sobj i → sobj j ) : Set  c₂ where
field
snmap : ( i : OC ) → sobj i
sncommute : ( i j : OC ) → ( f :  I ) →  smap f ( snmap i )  ≡ snmap j

open snat

open import Relation.Binary.HeterogeneousEquality as HE renaming ( cong to cong' ; sym to sym' ; subst₂ to subst₂' ; Extensionality to Extensionality' )
using (_≅_;refl; ≡-to-≅)
-- why we cannot use Extensionality' ?
postulate ≅extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) →
{a : Level } {A : Set a} {B B' : A → Set a}
{f : (y : A) → B y} {g : (y : A) → B' y} → (∀ y → f y ≅ g y) → ( ( λ y → f y ) ≅ ( λ y → g y ))

snat-cong : {c : Level}
{I OC : Set c}
{sobj : OC → Set c}
{smap : {i j : OC}  → (f : I) → sobj i → sobj j}
→ (s t : snat sobj smap)
→ (snmap-≡ : snmap s ≡ snmap t)
→ (sncommute-≅ : sncommute s ≅ sncommute t)
→ s ≡ t
snat-cong _ _ refl refl = refl

open import HomReasoning
open NTrans

Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
→ NTrans C Sets (K C Sets (snat  (ΓObj s Γ) (ΓMap s Γ) ) ) Γ
Cone C I s  Γ  =  record {
TMap = λ i →  λ sn →  snmap sn i
; isNTrans = record { commute = comm1 }
} where
comm1 :  {a b : Obj C} {f : Hom C a b} →
Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈
Sets [ (λ sn →  (snmap sn b)) o FMap (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
comm1 {a} {b} {f} = extensionality Sets  ( λ  sn  →  begin
FMap Γ f  (snmap sn  a )
≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn  a ))) (sym ( ≡←≈ s ( hom-iso s ))) ⟩
FMap Γ ( hom← s ( hom→ s f))  (snmap sn  a )
≡⟨⟩
ΓMap s Γ (hom→ s f) (snmap sn a )
≡⟨ sncommute sn a b  (hom→ s  f) ⟩
snmap sn b
∎  ) where
open  import  Relation.Binary.PropositionalEquality
open ≡-Reasoning

SetsLimit : {  c₁ c₂ ℓ : Level} ( I :  Set  c₁ ) ( C : Category c₁ c₂ ℓ )  ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) )
→ Limit C Sets Γ
SetsLimit {c₁} I C s Γ = record {
a0 =  snat  (ΓObj s Γ) (ΓMap s Γ)
; t0 = Cone C I s Γ
; isLimit = record {
limit  = limit1
; t0f=t = λ {a t i } → t0f=t {a} {t} {i}
; limit-uniqueness  =  λ {a t i }  → limit-uniqueness   {a} {t} {i}
}
}  where
comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K C Sets a) Γ) (f : I)
→ ΓMap s Γ f (TMap t i x) ≡ TMap t j x
comm2 {a} {x} t f =  ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) )
limit1 : (a : Obj Sets) → NTrans C Sets (K C Sets a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))
limit1 a t = λ x →  record { snmap = λ i →  ( TMap t i ) x ;
sncommute = λ i j f → comm2 t f }
t0f=t : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o limit1 a t ] ≈ TMap t i ]
t0f=t {a} {t} {i} =  extensionality Sets  ( λ  x  →  begin
( Sets [ TMap (Cone C I s Γ) i o limit1 a t ]) x
≡⟨⟩
TMap t i x
∎  ) where
open  import  Relation.Binary.PropositionalEquality
open ≡-Reasoning
limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} →
({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
limit-uniqueness {a} {t} {f} cif=t = extensionality Sets  ( λ  x  →  begin
limit1 a t x
≡⟨⟩
record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ i j f → comm2 t f }
≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets  ( λ  i  →  eq1 x i )) (eq5 x ) ⟩
record { snmap = λ i →  snmap  (f x ) i  ; sncommute = λ i j g → sncommute (f x ) i j g  }
≡⟨⟩
f x
∎  ) where
open  import  Relation.Binary.PropositionalEquality
open ≡-Reasoning
eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i
eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t  )
eq2 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (TMap t i x) ≡ TMap t j x
eq2 x i j f =  ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )
eq3 :  (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (snmap (f x) i) ≡ snmap (f x) j
eq3 x i j k =  sncommute (f x ) i j k
irr≅ : { c₂ : Level}  {d e : Set c₂ }  { x1 y1 : d } { x2 y2 : e }
( ee :  x1 ≅ x2 ) ( ee' :  y1  ≅ y2 )  ( eq :  x1  ≡ y1 ) ( eq' :  x2  ≡ y2 ) → eq ≅ eq'
irr≅ refl refl refl refl = refl
eq4 :  ( x : a)  ( i j : Obj C ) ( g : I )
→ ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g }  ) ≅  sncommute (f x) i j g
eq4 x i j g = irr≅ (≡-to-≅ (≡cong ( λ h → ΓMap s Γ g h ) (eq1 x i))) (≡-to-≅ (eq1 x j )) (eq2 x i j g ) (eq3 x i j g )
eq5 :  ( x : a)
→  ( λ i j g → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } ))
≅ ( λ i j g →  sncommute (f x) i j g )
eq5 x = ≅extensionality (Sets {c₁} ) ( λ i →
≅extensionality (Sets {c₁} ) ( λ j →
≅extensionality (Sets {c₁} ) ( λ g → eq4 x i j g ) ) )

open Limit
open IsLimit
open IProduct

SetsCompleteness : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) → Complete (Sets {c₁}) C
SetsCompleteness {c₁} {c₂} C I s  =  record {
climit = λ Γ → SetsLimit {c₁} I C s Γ
;  cequalizer = λ {a} {b} f g → record {  equalizer-c = sequ a b f g ;
equalizer = ( λ e → equ e ) ;
isEqualizer =  SetsIsEqualizer a b f g }
;  cproduct = λ J fi → SetsIProduct J fi
} where
```