Mercurial > hg > Members > kono > Proof > category
changeset 573:cc67ef472636
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 25 Apr 2017 11:24:27 +0900 |
| parents | 46e417754601 |
| children | dbb5da4ab08f |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 48 insertions(+), 52 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Mon Apr 24 22:26:59 2017 +0900 +++ b/SetsCompleteness.agda Tue Apr 25 11:24:27 2017 +0900 @@ -15,9 +15,9 @@ ≡cong = Relation.Binary.PropositionalEquality.cong -lemma1 : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} → +≈-to-≡ : { 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 +≈-to-≡ refl x = refl record Σ {a} (A : Set a) (B : Set a) : Set a where constructor _,_ @@ -47,9 +47,9 @@ 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 +record iproduct {a} (I : Set a) ( Product : I → Set a ) : Set a where field - pi1 : ( i : I ) → pi0 i + proj : ( i : I ) → Product i open iproduct @@ -58,7 +58,7 @@ SetsIProduct I fi = record { ai = fi ; iprod = iproduct I fi - ; pi = λ i prod → pi1 prod i + ; pi = λ i prod → proj prod i ; isIProduct = record { iproduct = iproduct1 ; pif=q = pif=q @@ -67,17 +67,17 @@ } } 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 ] + iproduct1 {q} qi x = record { proj = λ i → (qi i) x } + pif=q : {q : Obj Sets} (qi : (i : I) → Hom Sets q (fi i)) {i : I} → Sets [ Sets [ (λ prod → proj 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 : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → proj 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 } + 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 @@ -117,7 +117,7 @@ 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) ( ≡cong ( λ y → y x ) eq ) +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 @@ -137,7 +137,7 @@ 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 lemma1 + 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 @@ -178,19 +178,15 @@ {i j : Obj C } → ( f : I → I ) → ΓObj s Γ i → ΓObj s Γ j ΓMap s Γ {i} {j} f = FMap Γ ( hom← s f ) -record snproj { 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 - -open snproj 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 (snproj sobj smap ) (sobj j) ( λ x → smap f ( snmap x i ) ) ( λ x → snmap x j ) - slobj : OC → Set c₂ - slobj i = sobj i + slequ : { i j : OC } → ( f : I → I ) → sequ (iproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) ( λ x → proj x j ) + snmap : OC → Set c₂ + snmap i = sobj i + ipp : ( ( i : OC ) → sobj i ) → iproduct OC sobj + ipp qi = record { proj = qi } open slim @@ -199,39 +195,39 @@ lemma-equ : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) {a b : Obj C } { f : I → I } { se : slim (ΓObj s Γ) (ΓMap s Γ) } - → snmap (equ (slequ se {a} {a} (λ x → x))) a ≡ snmap (equ (slequ se {a} {b} f )) a -lemma-equ C I s Γ {a} {b} {f} {se} = begin - snmap (equ (slequ se {a} {a} (λ x → x))) a - ≡⟨ ≡cong ( λ p → snmap p a ) ( ≡cong ( λ QIX → record { snmap = QIX } ) ( + → proj (equ (slequ se {a} {a} (λ x → x))) a ≡ proj (equ (slequ se {a} {b} f )) a +lemma-equ C I s Γ {a} {b} {f} {se} = begin + proj (equ (slequ se {a} {a} (λ x → x))) a + ≡⟨ ≡cong ( λ p → proj p a ) ( ≡cong ( λ QIX → record { proj = QIX } ) ( extensionality Sets ( λ x → ≡cong ( λ qi → qi x ) refl ) )) ⟩ - snmap (equ (slequ se {a} {b} f )) a + proj (equ (slequ se {a} {b} f )) a ∎ where open import Relation.Binary.PropositionalEquality open ≡-Reasoning 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 Γ) )) Γ + → NTrans C Sets (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) Γ Cone C I s Γ = record { - TMap = λ i → λ se → snmap (equ (slequ se {i} {i} (λ x → x )) ) i + TMap = λ i → λ se → proj (equ (slequ se {i} {i} (λ x → x )) ) i ; isNTrans = record { commute = commute1 } } where - commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → snmap (equ (slequ se {a} {a} (λ x → x))) a) ] ≈ - Sets [ (λ se → snmap (equ (slequ se {b} {b} (λ x → x))) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] ] + commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (equ (slequ se {a} {a} (λ x → x))) a) ] ≈ + Sets [ (λ se → proj (equ (slequ se {b} {b} (λ x → x))) 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₁ → snmap (equ (slequ se₁ (λ x → x))) a) ]) se + (Sets [ FMap Γ f o (λ se₁ → proj (equ (slequ se₁ (λ x → x))) a) ]) se ≡⟨⟩ - FMap Γ f (snmap (equ (slequ se (λ x → x))) a) - ≡⟨ ≡cong ( λ g → FMap Γ g (snmap (equ (slequ se (λ x → x))) a)) (sym ( hom-iso s ) ) ⟩ - FMap Γ (hom← s ( hom→ s f)) (snmap (equ (slequ se {a} {a} (λ x → x))) a) + FMap Γ f (proj (equ (slequ se (λ x → x))) a) + ≡⟨ ≡cong ( λ g → FMap Γ g (proj (equ (slequ se (λ x → x))) a)) (sym ( hom-iso s ) ) ⟩ + FMap Γ (hom← s ( hom→ s f)) (proj (equ (slequ se {a} {a} (λ x → x))) a) ≡⟨ ≡cong ( λ g → FMap Γ (hom← s ( hom→ s f)) g ) ( lemma-equ C I s Γ ) ⟩ - FMap Γ (hom← s ( hom→ s f)) (snmap (equ (slequ se (hom→ s f ))) a) + FMap Γ (hom← s ( hom→ s f)) (proj (equ (slequ se (hom→ s f ))) a) ≡⟨ fe=ge0 ( slequ se (hom→ s f ) ) ⟩ - snmap (equ (slequ se ( hom→ s f ) )) b + proj (equ (slequ se ( hom→ s f ) )) b ≡⟨ sym ( lemma-equ C I s Γ ) ⟩ - snmap (equ (slequ se (λ x → x))) b + proj (equ (slequ se (λ x → x))) b ≡⟨⟩ - (Sets [ (λ se₁ → snmap (equ (slequ se₁ (λ x → x))) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ]) se + (Sets [ (λ se₁ → proj (equ (slequ se₁ (λ x → x))) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se ∎ ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning @@ -252,37 +248,37 @@ 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 : 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 { snmap = λ i → TMap t i x } ) ( limit2 a t f x ) + 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 Γ) )} + 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 { snmap = λ i₁ → TMap t i₁ x } ≡ equ (slequ (f x) f') + → record { proj = λ i₁ → TMap t i₁ x } ≡ equ (slequ (f x) f') uniquness2 {a} {t} {f} i j cif=t f' x = begin - record { snmap = λ i → TMap t i x } - ≡⟨ ≡cong ( λ g → record { snmap = λ i → g i } ) ( extensionality Sets ( λ i → sym ( ≡cong ( λ e → e x ) cif=t ) ) ) ⟩ - record { snmap = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x } + 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 { snmap = λ i → snmap (equ (slequ (f x) {i} {i} (λ x → x )) ) i } - ≡⟨ ≡cong ( λ g → record { snmap = λ i → g i } ) ( extensionality Sets ( λ i → lemma-equ C I s Γ )) ⟩ - record { snmap = λ i → snmap (equ (slequ (f x) f')) i } + record { proj = λ i → proj (equ (slequ (f x) {i} {i} (λ x → x )) ) i } + ≡⟨ ≡cong ( λ g → record { proj = λ i → g i } ) ( extensionality Sets ( λ i → lemma-equ C I s Γ )) ⟩ + record { proj = λ i → proj (equ (slequ (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 Γ) )} → + 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 { snmap = λ i → TMap t i x } ) ( limit2 a t f' 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 { snmap = λ i → TMap t i x } ) ( limit2 a t f' x )) (slequ (f x) f' ) (uniquness2 {a} {t} {f} i j cif=t f' 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' }