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

annotate freyd2.agda @ 621:19f31d22e790

add desciptive lemma

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Thu, 22 Jun 2017 08:56:32 +0900
parents	c95add5b7cbe
children	bd890a43ef5b

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
611 b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	3 open import Category.Sets renaming ( _o_ to _*_ )
497 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
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	20 ----
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	21 -- C is locally small i.e. Hom C i j is a set c₁
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	22 --
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	23 record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ )
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	24 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	25 field
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	26 hom→ : {i j : Obj C } → Hom C i j → I
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	27 hom← : {i j : Obj C } → ( f : I ) → Hom C i j
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	28 hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	29
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	30 open Small
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	31
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	32 -- maybe this is a part of local smallness
611 b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	33 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
497 e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	34
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	35 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	36 -- 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	37 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	38
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 ----
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	41 --
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	42 -- Hom ( a, - ) is Object mapping in Yoneda Functor
497 e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	43 --
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	44 ----
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	45
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	46 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	47 open Functor
498 c981a2f0642f UpreseveLimit detailing Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 497 diff changeset	48 open Limit
c981a2f0642f UpreseveLimit detailing Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 497 diff changeset	49 open IsLimit
c981a2f0642f UpreseveLimit detailing Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 497 diff changeset	50 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	51
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	52 Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	53 Yoneda {c₁} {c₂} {ℓ} A a = record {
497 e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	54 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	55 ; 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	56 ; 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	57 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	58 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	59 ≈-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	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 } where
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-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x
611 b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	63 lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≈-≡ A idL
497 e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	64 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	65 A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
611 b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	66 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≈-≡ A ( begin
497 e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	67 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	68 ≈↑⟨ assoc ⟩
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	69 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	70 ≈⟨⟩
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	71 ( λ 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	72 ∎ )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	73 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 ]
611 b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	74 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≈-≡ A ( begin
497 e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	75 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	76 ≈⟨ 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	77 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	78 ∎ )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	79
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	80 -- Representable U ≈　Hom(A,-)
502 01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	81
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	82 record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where
502 01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	83 field
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	84 -- FObj U x : A → Set
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	85 -- FMap U f = Set → Set (locally small)
502 01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	86 -- λ b → Hom (a,b) : A → Set
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	87 -- λ f → Hom (a,-) = λ b → Hom a b
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	88
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	89 repr→ : NTrans A (Sets {c₂}) U (Yoneda A a )
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	90 repr← : NTrans A (Sets {c₂}) (Yoneda A a) U
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	91 reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )]
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	92 reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	93
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	94 open Representable
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	95 open import freyd
502 01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	96
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	97 _↓_ : { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	98 → ( F G : Functor A B )
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	99 → Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	100 _↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} { A } { B } F G = CommaCategory
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	101 where open import Comma1 F G
498 c981a2f0642f UpreseveLimit detailing Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 497 diff changeset	102
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	103 open import freyd
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	104 open SmallFullSubcategory
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	105 open Complete
7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	106 open PreInitial
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	107 open HasInitialObject
d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	108 open import Comma1
d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	109 open CommaObj
d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	110 open LimitPreserve
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	111
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	112 -- Representable Functor U preserve limit , so K{*}↓U is complete
610 3fb4d834c349 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	113 --
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	114 -- Yoneda A b = λ a → Hom A a b : Functor A Sets
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	115 -- : Functor Sets A
610 3fb4d834c349 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	116
3fb4d834c349 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	117 UpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
612 f924056bf08a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 611 diff changeset	118 (b : Obj A )
610 3fb4d834c349 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	119 (Γ : Functor I A) (limita : Limit A I Γ) →
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	120 IsLimit Sets I (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (Yoneda A b))
612 f924056bf08a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 611 diff changeset	121 UpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record {
611 b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	122 limit = λ a t → ψ a t
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	123 ; t0f=t = λ {a t i} → t0f=t0 a t i
614 e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	124 ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t
610 3fb4d834c349 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	125 } where
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	126 hat0 : NTrans I Sets (K Sets I (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ)
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	127 hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)
611 b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	128 haa0 : Obj Sets
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	129 haa0 = FObj (Yoneda A b) (a0 lim)
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	130 ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) → NTrans I A (K A I b ) Γ
611 b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	131 ta a x t = record { TMap = λ i → (TMap t i ) x ; isNTrans = record { commute = commute1 } } where
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	132 commute1 : {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} →
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	133 A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K A I b) f ] ]
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	134 commute1 {a₁} {b₁} {f} = let open ≈-Reasoning A in begin
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	135 FMap Γ f o TMap t a₁ x
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	136 ≈⟨⟩
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	137 ( ( FMap (Yoneda A b ○ Γ ) f ) * TMap t a₁ ) x
611 b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	138 ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	139 ( TMap t b₁ * ( FMap (K Sets I a) f ) ) x
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	140 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	141 ( TMap t b₁ * id1 Sets a ) x
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	142 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	143 TMap t b₁ x
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	144 ≈↑⟨ idR ⟩
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	145 TMap t b₁ x o id1 A b
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	146 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	147 TMap t b₁ x o FMap (K A I b) f
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	148 ∎
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	149 ψ : (X : Obj Sets) ( t : NTrans I Sets (K Sets I X) (Yoneda A b ○ Γ))
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	150 → Hom Sets X (FObj (Yoneda A b) (a0 lim))
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	151 ψ X t x = FMap (Yoneda A b) (limit (isLimit lim) b (ta X x t )) (id1 A b )
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	152 t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) (i : Obj I)
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	153 → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ]
612 f924056bf08a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 611 diff changeset	154 t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	155 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ) x
612 f924056bf08a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 611 diff changeset	156 ≈⟨⟩
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	157 FMap (Yoneda A b) ( TMap (t0 lim) i) (FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ))
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	158 ≈⟨⟩ -- FMap (Hom A b ) f g = A [ f o g ]
613 afddfebea797 t0f=t0 done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 612 diff changeset	159 TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b )
afddfebea797 t0f=t0 done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 612 diff changeset	160 ≈⟨ cdr idR ⟩
afddfebea797 t0f=t0 done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 612 diff changeset	161 TMap (t0 lim) i o limit (isLimit lim) b (ta a x t )
afddfebea797 t0f=t0 done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 612 diff changeset	162 ≈⟨ t0f=t (isLimit lim) ⟩
afddfebea797 t0f=t0 done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 612 diff changeset	163 TMap (ta a x t) i
afddfebea797 t0f=t0 done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 612 diff changeset	164 ≈⟨⟩
612 f924056bf08a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 611 diff changeset	165 TMap t i x
f924056bf08a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 611 diff changeset	166 ∎ ))
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	167 limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} →
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	168 ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o f ] ≈ TMap t i ]) →
614 e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	169 Sets [ ψ a t ≈ f ]
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	170 limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	171 ψ a t x
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	172 ≈⟨⟩
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	173 FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )
614 e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	174 ≈⟨⟩
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	175 limit (isLimit lim) b (ta a x t ) o id1 A b
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	176 ≈⟨ idR ⟩
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	177 limit (isLimit lim) b (ta a x t )
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	178 ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≡-≈ ( cong ( λ g → g x )( t0f=t {i} ))) ⟩
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	179 f x
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	180 ∎ ))
610 3fb4d834c349 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	181
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	182
d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	183 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	184 (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b)
612 f924056bf08a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 611 diff changeset	185 UpreserveLimit A I b = record {
f924056bf08a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 611 diff changeset	186 preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim
610 3fb4d834c349 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	187 }
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	188
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	189 -- K{*}↓U has preinitial full subcategory if U is representable
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	190 -- if U is representable, K{*}↓U has initial Object ( so it has preinitial full subcategory )
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	191
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	192 open CommaHom
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	193
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	194 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	195 (a : Obj A )
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	196 → HasInitialObject {c₁} {c₂} {ℓ} ( K (Sets) A (FObj (Yoneda A a) a) ↓ (Yoneda A a) ) ( record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) } )
621 19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	197 KUhasInitialObj {c₁} {c₂} {ℓ} A a = record {
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	198 initial = λ b → initial0 b
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	199 ; uniqueness = λ b f → unique b f
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	200 } where
621 19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	201 commaCat : Category (c₂ ⊔ c₁) c₂ ℓ
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	202 commaCat = K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	203 initObj : Obj (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a)
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	204 initObj = record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }
619 325ee3bef15c on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 618 diff changeset	205 hom1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) →
325ee3bef15c on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 618 diff changeset	206 Hom Sets (FObj (K Sets A (FObj (Yoneda A a) a)) (obj b)) (FObj (Yoneda A a) (obj b))
621 19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	207 hom1 b = λ (x : Hom A a a ) → hom b x
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	208 hom2 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → Hom A a a → Hom A a (obj b )
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	209 hom2 b x = hom b x
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	210 comm1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) (x : FObj (Yoneda A a ) a )
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	211 → A [ ( Sets [ FMap (Yoneda A a) (id1 A (obj b) ) o hom b ] ) x ≈ hom b x ]
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	212 comm1 b x = let open ≈-Reasoning A in ≡-≈ ( cong ( λ k -> k x ) ( comm ( id1 (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a)) b ) ) )
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	213 -- hom b is Hom A a a → Hom A a (obj b)
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	214 -- hom b is Hom A a a → Hom A a (obj b)
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	215 -- hom b x is ( x : Hom A a a ) → Hom A a (obj b)
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	216 -- hom b (id1 A a) is ( id1 A a : Hom A a a ) → Hom A a (obj b)
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	217 -- hom b (id1 A a) o x is ( x : Hom A a a ) → Hom A a (obj b)
618 23ff2464f7ad fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 617 diff changeset	218 initial0comm1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → (x : FObj (Yoneda A a) a )
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	219 → FMap (Yoneda A a) (hom b (id1 A a)) x ≡ hom b x
618 23ff2464f7ad fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 617 diff changeset	220 initial0comm1 b x = let open ≈-Reasoning A in ≈-≡ A ( begin
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	221 FMap (Yoneda A a) (hom b (id1 A a)) x
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	222 ≈⟨⟩
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	223 hom b (id1 A a ) o x
620 c95add5b7cbe on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 619 diff changeset	224 ≈⟨ {!!} ⟩
621 19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	225 ( Sets [ FMap (Yoneda A a) (id1 A (obj b) ) o hom b ] ) x
19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	226 ≈⟨ comm1 b x ⟩
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	227 hom b x
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	228 ∎ )
618 23ff2464f7ad fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 617 diff changeset	229 initial0comm : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) →
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	230 Sets [ Sets [ FMap (Yoneda A a) (hom b (id1 A a)) o id1 Sets (FObj (Yoneda A a) a) ] ≈
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	231 Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (hom b (id1 A a)) ] ]
618 23ff2464f7ad fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 617 diff changeset	232 initial0comm b = let open ≈-Reasoning Sets in begin
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	233 FMap (Yoneda A a) (hom b (id1 A a)) o id1 Sets (FObj (Yoneda A a) a)
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	234 ≈⟨⟩
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	235 FMap (Yoneda A a) (hom b (id1 A a))
618 23ff2464f7ad fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 617 diff changeset	236 ≈⟨ extensionality A ( λ x → initial0comm1 b x ) ⟩
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	237 hom b
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	238 ≈⟨⟩
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	239 hom b o id1 Sets (FObj (K Sets A (FObj (Yoneda A a) a)) (obj b))
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	240 ≈⟨⟩
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	241 hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (hom b (id1 A a))
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	242 ∎
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	243 initial0 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) →
621 19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	244 Hom ((K Sets A (FObj (Yoneda A a) a)) ↓ (Yoneda A a)) initObj b
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	245 initial0 b = record {
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	246 arrow = hom b (id1 A a)
618 23ff2464f7ad fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 617 diff changeset	247 ; comm = initial0comm b }
23ff2464f7ad fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 617 diff changeset	248 -- what is comm f ?
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	249 comm-f : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a)))
621 19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	250 (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) initObj b)
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	251 → Sets [ Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ]
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	252 ≈ Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (arrow f) ] ]
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	253 comm-f b f = comm f
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	254 unique : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a))
621 19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	255 (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) initObj b)
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	256 → (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) [ f ≈ initial0 b ]
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	257 unique b f = let open ≈-Reasoning A in begin
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	258 arrow f
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	259 ≈↑⟨ idR ⟩
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	260 arrow f o id1 A a
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	261 ≈⟨⟩
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	262 ( Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ] ) (id1 A a)
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	263 ≈⟨ ≡-≈ ( cong (λ k → k (id1 A a)) (comm f ) ) ⟩
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	264 ( Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (arrow f) ] ) (id1 A a)
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	265 ≈⟨⟩
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	266 hom b (id1 A a)
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	267 ∎
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	268
a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	269
a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	270 -- K{*}↓U has preinitial full subcategory then U is representable
a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	271
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	272 open SmallFullSubcategory
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	273 open PreInitial
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	274
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	275 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	276 (U : Functor A (Sets {c₂}) )
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	277 (a : Obj (Sets {c₂}))
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	278 (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A a ↓ U) )
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	279 (PI : PreInitial {c₁} {c₂} {ℓ} ( K (Sets) A a ↓ U) (SFSF SFS ))
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	280 → Representable A U (obj (preinitialObj PI ))
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	281 UisRepresentable A U a SFS PI = record {
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	282 repr→ = record { TMap = {!!} ; isNTrans = record { commute = {!!} } }
a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	283 ; repr← = record { TMap = {!!} ; isNTrans = record { commute = {!!} } }
a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	284 ; reprId→ = λ {y} →　?
a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	285 ; reprId← = λ {y} →　?
a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	286 }
a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	287

Mercurial > hg > Members > kono > Proof > category

annotate freyd2.agda @ 621:19f31d22e790