Members/kono/Proof/category: freyd2.agda annotate

annotate freyd2.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	01a0dda67a8b
children	7194ba55df56

rev	line source
497 e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	1 open import Category -- https://github.com/konn/category-agda
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	2 open import Level
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	3 open import Category.Sets
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	4
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	5 module freyd2
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	6 where
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	7
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	8 open import HomReasoning
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	9 open import cat-utility
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	10 open import Relation.Binary.Core
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	11 open import Function
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	12
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	13 ----------
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	14 --
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	15 -- a : Obj A
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	16 -- U : A → Sets
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	17 -- U ⋍ Hom (a,-)
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	18 --
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	19
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	20 -- A is Locally small
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	21 postulate ≈-≡ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	22
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	23 import Relation.Binary.PropositionalEquality
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	24 -- 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 )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	25 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	26
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	27
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	28 ----
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	29 --
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	30 -- Hom ( a, - ) is Object mapping in co Yoneda Functor
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	31 --
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	32 ----
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	33
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	34 open NTrans
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	35 open Functor
498 c981a2f0642f UpreseveLimit detailing Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 497 diff changeset	36 open Limit
c981a2f0642f UpreseveLimit detailing Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 497 diff changeset	37 open IsLimit
c981a2f0642f UpreseveLimit detailing Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 497 diff changeset	38 open import Category.Cat
497 e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	39
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	40 HomA : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	41 HomA {c₁} {c₂} {ℓ} A a = record {
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	42 FObj = λ b → Hom A a b
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	43 ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y)
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	44 ; isFunctor = record {
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	45 identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ;
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	46 distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ;
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	47 ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	48 }
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	49 } where
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	50 lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	51 lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≈-≡ {_} {_} {_} {A} idL
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	52 lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	53 A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	54 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≈-≡ {_} {_} {_} {A} ( begin
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	55 A [ A [ g o f ] o x ]
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	56 ≈↑⟨ assoc ⟩
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	57 A [ g o A [ f o x ] ]
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	58 ≈⟨⟩
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	59 ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	60 ∎ )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	61 lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ]
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	62 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≈-≡ {_} {_} {_} {A} ( begin
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	63 A [ f o x ]
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	64 ≈⟨ resp refl-hom eq ⟩
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	65 A [ g o x ]
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	66 ∎ )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	67
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	68
502 01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	69 -- {*}↓U has preinitial full subcategory iff U is representable
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	70
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	71 record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (b : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	72 field
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	73 -- FObj U x : A → Set
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	74 -- FMap U f = Set → Set
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	75 -- λ b → Hom (a,b) : A → Set
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	76 -- λ f → Hom (a,-) = λ b → Hom a b
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	77
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	78 repr→ : NTrans A (Sets {c₂}) U (HomA A b )
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	79 repr← : NTrans A (Sets {c₂}) (HomA A b) U
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	80 representable→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )]
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	81 representable← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	82
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	83 -- HpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → (b : Obj A)
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	84 -- { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' )
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	85 -- → LimitPreserve A I (Sets {c₂}) ( HomA A b )
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	86 -- HpreseveLimit {_} { c₂} A b I = record {
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	87 -- preserve = λ Γ limita → record {
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	88 -- limit = λ a t → limitu a Γ t limita
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	89 -- ; t0f=t = λ { a t i } → t0f=tu {a} Γ t limita {i}
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	90 -- ; limit-uniqueness = λ { a t f } t=f → limit-uniquenessu {a} Γ limita t f t=f
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	91 -- }
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	92 -- } where
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	93 -- limitu : ( a : Obj Sets ) → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( limita : Limit A I Γ ) →
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	94 -- Hom Sets a (FObj (HomA A b) (a0 limita))
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	95 -- limitu = {!!}
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	96 -- t0f=tu : { a : Obj Sets } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( limita : Limit A I Γ ) →
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	97 -- ∀ { i : Obj I } → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o limitu a Γ t limita ] ≈ TMap t i ]
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	98 -- t0f=tu = {!!}
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	99 -- limit-uniquenessu : { a : Obj Sets } → (Γ : Functor I A )
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	100 -- → ( limita : Limit A I Γ ) →
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	101 -- ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( f : Hom Sets a (FObj (HomA A b) (a0 limita)) )
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	102 -- → ( ∀ { i : Obj I } → (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o f ] ≡ TMap t i ) )
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	103 -- → Sets [ limitu a Γ t limita ≈ f ]
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	104 -- limit-uniquenessu = {!!}
498 c981a2f0642f UpreseveLimit detailing Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 497 diff changeset	105
499 511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	106
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	107
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	108 --
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	109 --
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	110 -- UpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → ( U : Functor A (Sets {c₂}) ) (b : Obj A)
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	111 -- { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' )
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	112 -- ( rep : Representable A U b ) → LimitPreserve A I (Sets {c₂}) U
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	113 -- UpreseveLimit {_} { c₂} A U b I rep = record {
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	114 -- preserve = λ Γ limita → record {
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	115 -- limit = λ a t → limitu a Γ t limita
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	116 -- ; t0f=t = λ { a t i } → t0f=tu {a} Γ t limita {i}
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	117 -- ; limit-uniqueness = λ { a t f } t=f → limit-uniquenessu {a} Γ limita t f t=f
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	118 -- }
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	119 -- } where
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	120 -- limitu : ( a : Obj (Sets {c₂}) ) → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) → ( limita : Limit A I Γ ) →
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	121 -- Hom Sets a (FObj U (a0 limita))
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	122 -- limitu = {!!}
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	123 -- t0f=tu : { a : Obj (Sets {c₂}) } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) → ( limita : Limit A I Γ ) →
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	124 -- ∀ { i : Obj I } → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o limitu a Γ t limita ] ≈ TMap t i ]
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	125 -- t0f=tu = {!!}
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	126 -- limit-uniquenessu : { a : Obj (Sets {c₂}) } → (Γ : Functor I A )
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	127 -- → ( limita : Limit A I Γ ) →
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	128 -- ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) → ( f : Hom Sets a (FObj U (a0 limita)) )
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	129 -- → ( ∀ { i : Obj I } → (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o f ] ≡ TMap t i ) )
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	130 -- → Sets [ limitu a Γ t limita ≈ f ]
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	131 -- limit-uniquenessu = {!!}
511fd37d90ec prove only limit preserving on co yoneda functor's obj Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 498 diff changeset	132 --

Mercurial > hg > Members > kono > Proof > category

annotate freyd2.agda @ 600:3e2ef72d8d2f