Mercurial > hg > Members > kono > Proof > category
changeset 598:2e3459a9a69f
try two field again
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 02 Jun 2017 15:45:15 +0900 |
| parents | b281e8352158 |
| children | d3b669722d77 |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 217 insertions(+), 193 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Thu May 25 08:27:03 2017 +0900 +++ b/SetsCompleteness.agda Fri Jun 02 15:45:15 2017 +0900 @@ -1,4 +1,4 @@ -open import Category -- https://github.com/konn/category-agda +open import Category -- https://github.com/konn/category-agda open import Level open import Category.Sets renaming ( _o_ to _*_ ) @@ -11,28 +11,28 @@ -- 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 +≡cong = Relation.Binary.PropositionalEquality.cong -≈-to-≡ : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} → +lemma1 : { 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 +lemma1 refl x = refl record Σ {a} (A : Set a) (B : Set a) : Set a where constructor _,_ field proj₁ : A - proj₂ : B + proj₂ : B open Σ public SetsProduct : { c₂ : Level} → CreateProduct ( Sets { c₂} ) -SetsProduct { c₂ } = record { +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 ) + _×_ = λ f g x → record { proj₁ = f x ; proj₂ = g x } -- ( f x , g x ) ; π1fxg=f = refl ; π2fxg=g = refl ; uniqueness = refl @@ -45,53 +45,52 @@ 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 +record iproduct {a} (I : Set a) ( pi0 : I → Set a ) : Set a where field - proj : ( i : I ) → Product i - -open sproduct + pi1 : ( i : I ) → pi0 i -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 ) +open iproduct -SetsIProduct : { c₂ : Level} → (I : Obj Sets) (fi : I → Obj Sets ) +SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) → IProduct ( Sets { c₂} ) I SetsIProduct I fi = record { ai = fi - ; iprod = sproduct I fi - ; pi = λ i prod → proj prod i + ; iprod = iproduct I fi + ; pi = λ i prod → pi1 prod i ; isIProduct = record { - iproduct = iproduct1 I fi + iproduct = iproduct1 ; pif=q = pif=q ; ip-uniqueness = ip-uniqueness - ; ip-cong = ip-cong I fi + ; ip-cong = ip-cong } } 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 ] + 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 (sproduct I fi)} → Sets [ iproduct1 I fi (λ i → Sets [ (λ prod → proj prod i) o h ]) ≈ h ] + 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 - -- ^ . ---------→ + -- c -------→ a ---------→ b f ( f' + -- ^ . ---------→ -- | . g -- |k . -- | . h - -- d + --y : d -- cf. https://github.com/danr/Agda-projects/blob/master/Category-Theory/Equalizer.agda @@ -99,44 +98,40 @@ 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 +equ (elem x eq) = x -fe=ge0 : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → +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} +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 {_} {a} {b} {f} {g} (k h fh=gh x) ≡ equ (k' x) - lemma5 refl x = refl -- somehow this is not equal to ≈-to-≡ + 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 @@ -156,168 +151,197 @@ 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 + 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 +open Small -ΓObj : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) +Γ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 ) +Γ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 ) + +record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) + ( smap : { i j : OC } → (f : I → I )→ sobj i → sobj j ) : Set c₂ where + field + snmap : ( i : OC ) → sobj i + sncommute : { i j : OC } → ( f : I → I ) → smap f ( snmap i ) ≡ snmap j + +open snat + +snmeq : { c₂ : Level } { I OC : Set c₂ } { SO : OC → Set c₂ } { SM : { i j : OC } → (f : I → I )→ SO i → SO j } + ( s t : snat SO SM ) → ( i : OC ) → + { snmapsi snmapti : SO i } → snmapsi ≡ snmapti → SO i +snmeq s t i {pi} {.pi} refl = pi -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 ) +snmc : { c₂ : Level } { I OC : Set c₂ } { SO : OC → Set c₂ } { SM : { i j : OC } → (f : I → I )→ SO i → SO j } + ( s t : snat SO SM ) → { i j : OC } → { f : I → I } → + { snmapsi snmapti : SO i } → (eqi : snmapsi ≡ snmapti ) → + { snmapsj snmaptj : SO j } → (eqj : snmapsj ≡ snmaptj ) + → ( SM f ( snmapsi ) ≡ snmapsj ) + → ( SM f ( snmapti ) ≡ snmaptj ) + → SM f (snmeq s t i (eqi)) ≡ snmeq s t j (eqj) +snmc s t refl refl refl refl = refl + +snat1 : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I → I )→ SO i → SO j ) + → ( s t : snat SO SM ) + → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) + → ( eq2 : ( i j : OC ) ( f : I → I ) → SM {i} {j} f ( snmap s i ) ≡ snmap s j ) + → ( eq3 : ( i j : OC ) ( f : I → I ) → SM {i} {j} f ( snmap t i ) ≡ snmap t j ) + → snat SO SM +snat1 SO SM s t eq1 eq2 eq3 = record { + snmap = λ i → snmeq s t i (eq1 i ) ; + sncommute = λ {i} {j} f → snmc s t (eq1 i) (eq1 j) (eq2 i j f ) (eq3 i j f ) + } + +≡cong2 : { c c' : Level } { A B : Set c } { C : Set c' } { a a' : A } { b b' : B } ( f : A → B → C ) + → a ≡ a' + → b ≡ b' + → f a b ≡ f a' b' +≡cong2 _ refl refl = refl + +subst2 : { c c' : Level } { A B : Set c } { C : Set c' } { a a' : A } { b b' : B } ( f : A → C ) ( g : B → C ) + → f a ≡ g b + → a ≡ a' + → b ≡ b' + → f a' ≡ g b' +subst2 {_} {_} {A} {B} {C} { a} {.a} {b} {.b} f g f=g refl refl = f=g -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 ) +snmeqeqs : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I → I )→ SO i → SO j ) + ( s t : snat SO SM ) → ( i : OC ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) → + snmap s i ≡ snmeq s t i (eq1 i ) +snmeqeqs SO SM s t i eq1 = lemma (eq1 i) refl where + lemma : { snmapsi snmapti sm : SO i } → ( eq1 : snmapsi ≡ snmapti ) → ( snmapsi ≡ sm ) → + sm ≡ snmeq s t i eq1 + lemma refl refl = refl -open slim +snmeqeqt : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I → I )→ SO i → SO j ) + ( s t : snat SO SM ) → ( i : OC ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) → + snmap t i ≡ snmeq s t i (eq1 i ) +snmeqeqt SO SM s t i eq1 = lemma (eq1 i) refl where + lemma : { snmapsi snmapti sm : SO i } → ( eq1 : snmapsi ≡ snmapti ) → ( snmapti ≡ sm ) → + sm ≡ snmeq s t i eq1 + lemma refl refl = refl + +scomm2 : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I → I )→ SO i → SO j ) + ( s t : snat SO SM ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) + → ( i j : OC ) → ( f : I → I ) + → SM f ( snmap s i ) ≡ snmap s j + → {x : ( i : OC ) → SO i } → (x ≡ λ i → snmeq s t i (eq1 i ) ) + → SM f (x i) ≡ x j +scomm2 SO SM s t eq1 i j f eq2 refl = lemma eq2 (snmeqeqs SO SM s t i eq1) (snmeqeqs SO SM s t j eq1) where + lemma : { si sni : SO i} { sj snj : SO j } → ( SM f si ≡ sj ) → (si ≡ sni ) → (sj ≡ snj ) → ( SM f sni ≡ snj ) + lemma eq1 eq2 eq3 = subst2 (λ x → SM f x) (λ y → y ) eq1 eq2 eq3 -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 +tcomm2 : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I → I )→ SO i → SO j ) + ( s t : snat SO SM ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) + → ( i j : OC ) → ( f : I → I ) + → SM f ( snmap t i ) ≡ snmap t j + → SM f (snmeq s t i (eq1 i)) ≡ snmeq s t j (eq1 j) +tcomm2 SO SM s t eq1 i j f eq2 = lemma eq2 (snmeqeqt SO SM s t i eq1) (snmeqeqt SO SM s t j eq1) where + lemma : { si sni : SO i} { sj snj : SO j } → ( SM f si ≡ sj ) → (si ≡ sni ) → (sj ≡ snj ) → ( SM f sni ≡ snj ) + lemma eq1 eq2 eq3 = subst2 (λ x → SM f x) (λ y → y ) eq1 eq2 eq3 + + +snat-cong : { c : Level } { I OC : Set c } ( SObj : OC → Set c ) ( SMap : { i j : OC } → (f : I → I )→ SObj i → SObj j) + { s t : snat SObj SMap } + → (( i : OC ) → snmap s i ≡ snmap t i ) + → ( ( i j : OC ) ( f : I → I ) → SMap {i} {j} f ( snmap s i ) ≡ snmap s j ) + → ( ( i j : OC ) ( f : I → I ) → SMap {i} {j} f ( snmap t i ) ≡ snmap t j ) + → s ≡ t +snat-cong {_} {I} {OC} SO SM {s} {t} eq1 eq2 eq3 = begin + record { snmap = λ i → snmap s i ; sncommute = λ {i} {j} f → sncommute s f } + ≡⟨ + ≡cong2 ( λ x y → + record { snmap = λ i → x i ; sncommute = λ {i} {j} f → y x i j f } ) ( extensionality Sets ( λ i → (eq1 i) ) ) + ( extensionality Sets ( λ x → + ( extensionality Sets ( λ i → + ( extensionality Sets ( λ j → + ( extensionality Sets ( λ f → irr {!!} {!!} + )))))))) + ⟩ + record { snmap = λ i → snmap t i ; sncommute = λ {i} {j} f → sncommute t f } + ∎ 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 : Obj C } → { f : I → I } - → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) - → proj (ipp se {i} {j} f) i ≡ proj (ipp se {i} {i} (slid C I s i) ) i -lemma-equ' C I s Γ {i} {j} {f} se = - fe=ge0 {!!} +open import HomReasoning +open NTrans -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 +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 (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 Sets C (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 ( hom-iso s )) ⟩ + FMap Γ ( hom← s ( hom→ s f)) (snmap sn a ) ≡⟨⟩ - 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' + ΓMap s Γ (hom→ s f) (snmap sn a ) + ≡⟨ sncommute sn (hom→ s f) ⟩ + snmap sn b ∎ ) 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 +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 = 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 + a0 : Obj Sets + a0 = snat (ΓObj s Γ) (ΓMap s Γ) + comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) + → ΓMap s Γ f (TMap t i x) ≡ TMap t j x + comm2 {a} {x} t f = ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ) + limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) + limit1 a t = λ x → record { snmap = λ i → ( TMap t i ) x ; + sncommute = λ f → comm2 t f } + t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C 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 + -- ≡⟨⟩ + -- snmap ( record { snmap = λ i → ( TMap t i ) x ; sncommute = λ {i j} f → comm2 {a} {x} {i} {j} t f } ) i ≡⟨⟩ - 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 + TMap t i x ∎ ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning - - + limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C 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 = λ f → comm2 t f } + ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) (eq1 x) (eq2 x ) (eq3 x ) ⟩ + record { snmap = λ i → snmap (f x ) i ; sncommute = sncommute (f x ) } + ≡⟨⟩ + 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) (f : I → I ) → ΓMap s Γ f (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 → I ) → ΓMap s Γ k (snmap (f x) i) ≡ snmap (f x) j + eq3 x i j k = sncommute (f x ) k -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 -