Mercurial > hg > Members > kono > Proof > category
view SetsCompleteness.agda @ 600:3e2ef72d8d2f
Set Completeness unfinished
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 03 Jun 2017 09:46:59 +0900 |
| parents | d3b669722d77 |
| children | 2e7b5a777984 |
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) → f ≡ g → ( λ 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 ≈-to-≡ : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} → Sets [ f ≈ g ] → (x : a ) → f x ≡ g x ≈-to-≡ 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} → CreateProduct ( Sets { c₂} ) SetsProduct { c₂ } = record { product = λ a b → Σ a b ; π1 = λ a b → λ ab → (proj₁ ab) ; π2 = λ a b → λ ab → (proj₂ ab) ; isProduct = λ a b → 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 sproduct {a} (I : Set a) ( Product : I → Set a ) : Set a where field proj : ( i : I ) → Product i open sproduct iproduct1 : { c₂ : Level} → (I : Obj (Sets { c₂}) ) (fi : I → Obj Sets ) {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (sproduct I fi) iproduct1 I fi {q} qi x = record { proj = λ i → (qi i) x } ipcx : { c₂ : Level} → (I : Obj (Sets { c₂})) (fi : I → Obj Sets ) {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 I fi qi x ≡ iproduct1 I fi qi' x ipcx I fi {q} {qi} {qi'} qi=qi x = begin record { proj = λ i → (qi i) x } ≡⟨ ≡cong ( λ qi → record { proj = qi } ) ( extensionality Sets (λ i → ≈-to-≡ (qi=qi i) x )) ⟩ record { proj = λ i → (qi' i) x } ∎ where open import Relation.Binary.PropositionalEquality open ≡-Reasoning ip-cong : { c₂ : Level} → (I : Obj (Sets { c₂}) ) (fi : I → Obj Sets ) {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 I fi qi ≈ iproduct1 I fi qi' ] ip-cong I fi {q} {qi} {qi'} qi=qi = extensionality Sets ( ipcx I fi qi=qi ) SetsIProduct : { c₂ : Level} → (I : Obj Sets) (fi : I → Obj Sets ) → IProduct ( Sets { c₂} ) I SetsIProduct I fi = record { ai = fi ; iprod = sproduct I fi ; pi = λ i prod → proj prod i ; isIProduct = record { iproduct = iproduct1 I fi ; pif=q = pif=q ; ip-uniqueness = ip-uniqueness ; ip-cong = ip-cong I fi } } where pif=q : {q : Obj Sets} (qi : (i : I) → Hom Sets q (fi i)) {i : I} → Sets [ Sets [ (λ prod → proj prod i) o iproduct1 I fi qi ] ≈ qi i ] pif=q {q} qi {i} = refl ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (sproduct I fi)} → Sets [ iproduct1 I fi (λ i → Sets [ (λ prod → proj prod i) o h ]) ≈ h ] ip-uniqueness = refl -- -- e f -- c -------→ a ---------→ b -- ^ . ---------→ -- | . g -- |k . -- | . h -- 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 elm-cong : { c₂ : Level} → {a b : Obj (Sets {c₂}) } {f g : Hom (Sets {c₂}) a b} → (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' ) fe=ge : { c₂ : Level} → {a b : Obj (Sets {c₂}) } {f g : Hom (Sets {c₂}) a b} → Sets [ Sets [ f o (λ e → equ {_} {a} {b} {f} {g} e ) ] ≈ Sets [ g o (λ e → equ e ) ] ] fe=ge = extensionality Sets (fe=ge0 ) k : { c₂ : Level} → {a b : Obj (Sets {c₂}) } {f g : Hom (Sets {c₂}) a b} → {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) ( ≈-to-≡ eq x ) ek=h : { c₂ : Level} → {a b : Obj (Sets {c₂}) } {f g : Hom (Sets {c₂}) a b} → {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ {_} {a} {b} {f} {g} e ) o k h eq ] ≈ h ] ek=h {_} {_} {_} {_} {_} {d} {h} {eq} = 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 { c₂ } {a} {b} {f} {g} ; k = λ {d} h eq → k { c₂ } {a} {b} {f} {g} {d} h eq ; ek=h = λ {d} {h} {eq} → ek=h {c₂} {a} {b} {f} {g} {d} {h} {eq} ; uniqueness = uniqueness } where 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 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 {_} {a} {b} {f} {g} (k h fh=gh x) ≡ equ (k' x) lemma5 refl x = refl -- somehow this is not equal to ≈-to-≡ 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 → I hom← : {i j : Obj C } → ( f : I → I ) → Hom C i j hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } → (x≈y : C [ x ≈ y ] ) → x ≡ y 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 → I ) → ΓObj s Γ i → ΓObj s Γ j ΓMap s Γ {i} {j} f = FMap Γ ( hom← s f ) slid : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) → (x : Obj C) → I → I slid C I s x = hom→ s ( id1 C x ) record slim { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I ) → sobj i → sobj j ) : Set c₂ where field slequ : { i j : OC } → ( f : I → I ) → sequ (sproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) ( λ x → proj x j ) slobj : OC → Set c₂ slobj i = sobj i slmap : {i j : OC } → (f : I → I ) → sobj i → sobj j slmap f = smap f ipp : {i j : OC } → (f : I → I ) → sproduct OC sobj ipp {i} {j} f = equ ( slequ {i} {j} f ) open slim smap-id : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) ( se : slim (ΓObj s Γ) (ΓMap s Γ) ) → (i : Obj C ) → (x : FObj Γ i ) → slmap se (slid C I s i) x ≡ x smap-id C I s Γ se i x = begin slmap se (slid C I s i) x ≡⟨⟩ slmap se ( hom→ s (id1 C i)) x ≡⟨⟩ FMap Γ (hom← s (hom→ s (id1 C i))) x ≡⟨ ≡cong ( λ ii → FMap Γ ii x ) (hom-iso s) ⟩ FMap Γ (id1 C i) x ≡⟨ ≡cong ( λ f → f x ) (IsFunctor.identity ( isFunctor Γ) ) ⟩ x ∎ where open import Relation.Binary.PropositionalEquality open ≡-Reasoning product-to : { c₂ : Level } { I OC : Set c₂ } { sobj : OC → Set c₂ } → Hom Sets (sproduct OC sobj) (sproduct OC sobj) product-to x = record { proj = proj x } lemma-equ : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) {i j i' j' : Obj C } → { f f' : I → I } → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) → proj (ipp se {i} {j} f) i ≡ proj (ipp se {i'} {j'} f' ) i lemma-equ C I s Γ {i} {j} {i'} {j'} {f} {f'} se = ≡cong ( λ p → proj p i ) ( begin ipp se {i} {j} f ≡⟨⟩ record { proj = λ x → proj (equ (slequ se f)) x } ≡⟨ ≡cong ( λ p → record { proj = proj p i }) ( ≡cong ( λ QIX → record { proj = QIX } ) ( extensionality Sets ( λ x → ≡cong ( λ qi → qi x ) refl ) )) ⟩ record { proj = λ x → proj (equ (slequ se f')) x } ≡⟨⟩ ipp se {i'} {j'} f' ∎ ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning 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 Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) Γ Cone C I s Γ = record { TMap = λ i → λ se → proj ( ipp se {i} {i} (slid C I s i) ) i ; isNTrans = record { commute = commute1 } } where commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj ( ipp se (slid C I s a) ) a) ] ≈ Sets [ (λ se → proj ( ipp se (slid C I s b) ) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ] commute1 {a} {b} {f} = extensionality Sets ( λ se → begin (Sets [ FMap Γ f o (λ se₁ → proj ( ipp se (slid C I s a) ) a) ]) se ≡⟨⟩ FMap Γ f (proj ( ipp se {a} {a} (slid C I s a) ) a) ≡⟨ ≡cong ( λ g → FMap Γ g (proj ( ipp se {a} {a} (slid C I s a) ) a)) (sym ( hom-iso s ) ) ⟩ FMap Γ (hom← s ( hom→ s f)) (proj ( ipp se {a} {a} (slid C I s a) ) a) ≡⟨ ≡cong ( λ g → FMap Γ (hom← s ( hom→ s f)) g ) ( lemma-equ C I s Γ se ) ⟩ FMap Γ (hom← s ( hom→ s f)) (proj ( ipp se {a} {b} (hom→ s f) ) a) ≡⟨ fe=ge0 ( slequ se (hom→ s f ) ) ⟩ proj (ipp se {a} {b} ( hom→ s f )) b ≡⟨ sym ( lemma-equ C I s Γ se ) ⟩ proj (ipp se {b} {b} (slid C I s b)) b ≡⟨⟩ (Sets [ (λ se₁ → proj (ipp se₁ (slid C I s b)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se ∎ ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) → Limit Sets C Γ SetsLimit { c₂} C I s Γ = record { a0 = slim (ΓObj s Γ) (ΓMap s Γ) ; t0 = Cone C I s Γ ; isLimit = record { limit = limit1 ; t0f=t = λ {a t i } → refl ; limit-uniqueness = λ {a} {t} {f} → uniquness1 {a} {t} {f} } } where limit2 : (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → {i j : Obj C } → ( f : I → I ) → ( x : a ) → ΓMap s Γ f (TMap t i x) ≡ TMap t j x limit2 a t f x = ≡cong ( λ g → g x ) ( IsNTrans.commute ( isNTrans t ) ) limit1 : (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ) ) limit1 a t x = record { slequ = λ {i} {j} f → elem ( record { proj = λ i → TMap t i x } ) ( limit2 a t f x ) } uniquness2 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ) )} → ( i j : Obj C ) → ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → (f' : I → I ) → (x : a ) → record { proj = λ i₁ → TMap t i₁ x } ≡ equ (slequ (f x) f') uniquness2 {a} {t} {f} i j cif=t f' x = begin record { proj = λ i → TMap t i x } ≡⟨ ≡cong ( λ g → record { proj = λ i → g i } ) ( extensionality Sets ( λ i → sym ( ≡cong ( λ e → e x ) cif=t ) ) ) ⟩ record { proj = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x } ≡⟨⟩ record { proj = λ i → proj (ipp (f x) {i} {i} (slid C I s i) ) i } ≡⟨ ≡cong ( λ g → record { proj = λ i' → g i' } ) ( extensionality Sets ( λ i'' → lemma-equ C I s Γ (f x))) ⟩ record { proj = λ i → proj (ipp (f x) f') i } ∎ where open import Relation.Binary.PropositionalEquality open ≡-Reasoning uniquness1 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (slim (Γ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 ] uniquness1 {a} {t} {f} cif=t = extensionality Sets ( λ x → begin limit1 a t x ≡⟨⟩ record { slequ = λ {i} {j} f' → elem ( record { proj = λ i → TMap t i x } ) ( limit2 a t f' x ) } ≡⟨ ≡cong ( λ e → record { slequ = λ {i} {j} f' → e i j f' x } ) ( extensionality Sets ( λ i → extensionality Sets ( λ j → extensionality Sets ( λ f' → extensionality Sets ( λ x → elm-cong ( elem ( record { proj = λ i → TMap t i x } ) ( limit2 a t f' x )) (slequ (f x) f' ) (uniquness2 {a} {t} {f} i j cif=t f' x ) ) ))) ) ⟩ record { slequ = λ {i} {j} f' → slequ (f x ) f' } ≡⟨⟩ f x ∎ ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning