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

annotate freyd2.agda @ 658:9242298cffa8

adjoint functor theorem done

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Thu, 06 Jul 2017 13:50:45 +0900
parents	0d029674eb59
children	372205f40ab0

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
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	20 -- 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	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
497 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
624 9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	27
497 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 --
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	30 -- 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	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
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	40 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	41 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	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
611 b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	51 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	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
611 b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	54 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	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 ]
611 b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	62 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	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
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	68 -- Representable U ≈　Hom(A,-)
502 01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	69
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	70 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	71 field
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	72 -- FObj U x : A → Set
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	73 -- FMap U f = Set → Set (locally small)
502 01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	74 -- λ b → Hom (a,b) : A → Set
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	75 -- λ f → Hom (a,-) = λ b → Hom a b
01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	76
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	77 repr→ : NTrans A (Sets {c₂}) U (Yoneda A a )
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	78 repr← : NTrans A (Sets {c₂}) (Yoneda A a) U
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	79 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	80 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	81
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	82 open Representable
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	83 open import freyd
502 01a0dda67a8b on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 499 diff changeset	84
624 9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	85 _↓_ : { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	86 → ( F G : Functor A B )
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	87 → Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	88 _↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} { A } { B } F G = CommaCategory
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	89 where open import Comma1 F G
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	90
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	91 open SmallFullSubcategory
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	92 open Complete
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	93 open PreInitial
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	94 open HasInitialObject
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	95 open import Comma1
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	96 open CommaObj
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	97 open LimitPreserve
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	98
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	99 -- 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	100 --
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	101 -- 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	102 -- : Functor Sets A
610 3fb4d834c349 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	103
635 f7cc0ec00e05 introduce U preserving Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 634 diff changeset	104 YonedaFpreserveLimit0 : {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	105 (b : Obj A )
610 3fb4d834c349 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	106 (Γ : Functor I A) (limita : Limit A I Γ) →
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	107 IsLimit Sets I (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (Yoneda A b))
635 f7cc0ec00e05 introduce U preserving Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 634 diff changeset	108 YonedaFpreserveLimit0 {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	109 limit = λ a t → ψ a t
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	110 ; 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	111 ; 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	112 } where
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	113 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	114 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	115 haa0 : Obj Sets
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	116 haa0 = FObj (Yoneda A b) (a0 lim)
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	117 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	118 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	119 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	120 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	121 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	122 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	123 ≈⟨⟩
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	124 ( ( 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	125 ≈⟨ ≡-≈ ( 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	126 ( 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	127 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	128 ( 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	129 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	130 TMap t b₁ x
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	131 ≈↑⟨ idR ⟩
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	132 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	133 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	134 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	135 ∎
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	136 ψ : (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	137 → Hom Sets X (FObj (Yoneda A b) (a0 lim))
7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	138 ψ 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	139 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	140 → 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	141 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	142 ( 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	143 ≈⟨⟩
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	144 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	145 ≈⟨⟩ -- 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	146 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	147 ≈⟨ cdr idR ⟩
afddfebea797 t0f=t0 done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 612 diff changeset	148 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	149 ≈⟨ t0f=t (isLimit lim) ⟩
afddfebea797 t0f=t0 done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 612 diff changeset	150 TMap (ta a x t) i
afddfebea797 t0f=t0 done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 612 diff changeset	151 ≈⟨⟩
612 f924056bf08a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 611 diff changeset	152 TMap t i x
f924056bf08a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 611 diff changeset	153 ∎ ))
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	154 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	155 ({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	156 Sets [ ψ a t ≈ f ]
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	157 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	158 ψ a t x
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	159 ≈⟨⟩
616 7011165c118e on going .. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 615 diff changeset	160 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	161 ≈⟨⟩
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	162 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	163 ≈⟨ idR ⟩
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	164 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	165 ≈⟨ 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	166 f x
e6be03d94284 Representational Functor preserve limit done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 613 diff changeset	167 ∎ ))
610 3fb4d834c349 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	168
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	169
635 f7cc0ec00e05 introduce U preserving Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 634 diff changeset	170 YonedaFpreserveLimit : {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	171 (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b)
635 f7cc0ec00e05 introduce U preserving Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 634 diff changeset	172 YonedaFpreserveLimit A I b = record {
f7cc0ec00e05 introduce U preserving Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 634 diff changeset	173 preserve = λ Γ lim → YonedaFpreserveLimit0 A I b Γ lim
610 3fb4d834c349 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	174 }
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	175
624 9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	176
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	177 -- 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	178 -- 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	179
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	180 open CommaHom
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	181
627 efa1f2103a83 fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 626 diff changeset	182 data * {c : Level} : Set c where
efa1f2103a83 fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 626 diff changeset	183 OneObj : *
efa1f2103a83 fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 626 diff changeset	184
609 d686d7ae38e0 on goging Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 608 diff changeset	185 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
608 7194ba55df56 freyd2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 502 diff changeset	186 (a : Obj A )
628 b99660fa14e1 remove arrow's yellow Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 627 diff changeset	187 → HasInitialObject ( K (Sets) A * ↓ (Yoneda A a) ) ( record { obj = a ; hom = λ x → id1 A a } )
621 19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	188 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	189 initial = λ b → initial0 b
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	190 ; uniqueness = λ f → unique f
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	191 } where
621 19f31d22e790 add desciptive lemma Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 620 diff changeset	192 commaCat : Category (c₂ ⊔ c₁) c₂ ℓ
624 9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	193 commaCat = K Sets A * ↓ Yoneda A a
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	194 initObj : Obj (K Sets A * ↓ Yoneda A a)
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	195 initObj = record { obj = a ; hom = λ x → id1 A a }
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	196 comm2 : (b : Obj commaCat) ( x : * ) → ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) x ≡ hom b x
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	197 comm2 b OneObj = let open ≈-Reasoning A in ≈-≡ A ( begin
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	198 ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) OneObj
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	199 ≈⟨⟩
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	200 FMap (Yoneda A a) (hom b OneObj) (id1 A a)
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	201 ≈⟨⟩
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	202 hom b OneObj o id1 A a
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	203 ≈⟨ idR ⟩
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	204 hom b OneObj
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	205 ∎ )
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	206 comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K Sets A *) (hom b OneObj) ] ]
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	207 comm1 b = let open ≈-Reasoning Sets in begin
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	208 FMap (Yoneda A a) (hom b OneObj) o ( λ x → id1 A a )
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	209 ≈⟨ extensionality A ( λ x → comm2 b x ) ⟩
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	210 hom b
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	211 ≈⟨⟩
624 9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	212 hom b o FMap (K Sets A *) (hom b OneObj)
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	213 ∎
624 9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	214 initial0 : (b : Obj commaCat) →
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	215 Hom commaCat initObj b
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	216 initial0 b = record {
624 9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	217 arrow = hom b OneObj
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	218 ; comm = comm1 b }
625 d73fbed639a9 initialObject done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 624 diff changeset	219 -- what is comm f ?
d73fbed639a9 initialObject done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 624 diff changeset	220 comm-f : (b : Obj (K Sets A * ↓ (Yoneda A a))) (f : Hom (K Sets A * ↓ Yoneda A a) initObj b)
d73fbed639a9 initialObject done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 624 diff changeset	221 → Sets [ Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ]
d73fbed639a9 initialObject done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 624 diff changeset	222 ≈ Sets [ hom b o FMap (K Sets A *) (arrow f) ] ]
d73fbed639a9 initialObject done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 624 diff changeset	223 comm-f b f = comm f
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	224 unique : {b : Obj (K Sets A * ↓ Yoneda A a)} (f : Hom (K Sets A * ↓ Yoneda A a) initObj b)
624 9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	225 → (K Sets A * ↓ Yoneda A a) [ f ≈ initial0 b ]
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	226 unique {b} f = let open ≈-Reasoning A in begin
624 9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	227 arrow f
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	228 ≈↑⟨ idR ⟩
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	229 arrow f o id1 A a
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	230 ≈⟨⟩
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	231 ( Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ] ) (id1 A a)
625 d73fbed639a9 initialObject done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 624 diff changeset	232 ≈⟨⟩
d73fbed639a9 initialObject done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 624 diff changeset	233 ( Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj
d73fbed639a9 initialObject done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 624 diff changeset	234 ≈⟨ ≡-≈ ( cong (λ k → k OneObj ) (comm f )) ⟩
624 9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	235 ( Sets [ hom b o FMap (K Sets A *) (arrow f) ] ) OneObj
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	236 ≈⟨⟩
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	237 hom b OneObj
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	238 ∎
9b9bc1e076f3 introduce one element set Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 623 diff changeset	239
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	240
a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	241
644 8e35703ef116 representability theorem done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 643 diff changeset	242 -- A is complete and K{*}↓U has preinitial full subcategory and U preserve limit then U is representable
615 a45c32ceca97 initial Object's arrow found Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 614 diff changeset	243
617 34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	244 open SmallFullSubcategory
34540494fdcf initital obj uniquness done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 616 diff changeset	245 open PreInitial
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	246
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	247 -- if U preserve limit, K{*}↓U has initial object from freyd.agda
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	248
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	249 ≡-cong = Relation.Binary.PropositionalEquality.cong
c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	250
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	251
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	252 ub : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b )
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	253 → Hom Sets (FObj (K Sets A *) b) (FObj U b)
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	254 ub A U b x OneObj = x
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	255 ob : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b )
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	256 → Obj ( K Sets A * ↓ U)
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	257 ob A U b x = record { obj = b ; hom = ub A U b x}
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	258 fArrow : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) {a b : Obj A} (f : Hom A a b) (x : FObj U a )
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	259 → Hom ( K Sets A * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) )
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	260 fArrow A U {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x }
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	261 where
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	262 fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub A U a x y ) ≡ ub A U b (FMap U f x) y
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	263 fArrowComm1 a b f x OneObj = refl
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	264 fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) →
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	265 Sets [ Sets [ FMap U f o hom (ob A U a x) ] ≈ Sets [ hom (ob A U b (FMap U f x)) o FMap (K Sets A *) f ] ]
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	266 fArrowComm a b f x = extensionality Sets ( λ y → begin
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	267 ( Sets [ FMap U f o hom (ob A U a x) ] ) y
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	268 ≡⟨⟩
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	269 FMap U f ( hom (ob A U a x) y )
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	270 ≡⟨⟩
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	271 FMap U f ( ub A U a x y )
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	272 ≡⟨ fArrowComm1 a b f x y ⟩
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	273 ub A U b (FMap U f x) y
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	274 ≡⟨⟩
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	275 hom (ob A U b (FMap U f x)) y
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	276 ∎ ) where
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	277 open import Relation.Binary.PropositionalEquality
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	278 open ≡-Reasoning
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	279
635 f7cc0ec00e05 introduce U preserving Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 634 diff changeset	280
f7cc0ec00e05 introduce U preserving Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 634 diff changeset	281 -- if K{*}↓U has initial Obj, U is representable
f7cc0ec00e05 introduce U preserving Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 634 diff changeset	282
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	283 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	284 (U : Functor A (Sets {c₂}) )
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	285 ( i : Obj ( K (Sets) A * ↓ U) )
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	286 (In : HasInitialObject ( K (Sets) A * ↓ U) i )
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	287 → Representable A U (obj i)
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	288 UisRepresentable A U i In = record {
627 efa1f2103a83 fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 626 diff changeset	289 repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	290 ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	291 ; reprId→ = iso→
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	292 ; reprId← = iso←
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	293 } where
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	294 comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	295 ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	296 ≡ (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	297 comm11 a b f y = begin
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	298 ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y
631 7be3eb96310c introduce fArrow Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 630 diff changeset	299 ≡⟨⟩
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	300 A [ f o arrow (initial In (ob A U a y)) ]
631 7be3eb96310c introduce fArrow Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 630 diff changeset	301 ≡⟨⟩
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	302 A [ arrow ( fArrow A U f y ) o arrow (initial In (ob A U a y)) ]
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	303 ≡⟨ ≈-≡ A ( uniqueness In {ob A U b (FMap U f y) } (( K Sets A * ↓ U) [ fArrow A U f y o initial In (ob A U a y)] ) ) ⟩
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	304 arrow (initial In (ob A U b (FMap U f y) ))
629 693020c766d2 fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 628 diff changeset	305 ≡⟨⟩
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	306 (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y
629 693020c766d2 fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 628 diff changeset	307 ∎ where
693020c766d2 fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 628 diff changeset	308 open import Relation.Binary.PropositionalEquality
693020c766d2 fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 628 diff changeset	309 open ≡-Reasoning
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	310 tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj i)) b)
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	311 tmap1 b x = arrow ( initial In (ob A U b x ) )
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	312 comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj i)) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ]
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	313 comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	314 FMap (Yoneda A (obj i)) f o tmap1 a
629 693020c766d2 fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 628 diff changeset	315 ≈⟨⟩
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	316 FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In ( ob A U a x )))
629 693020c766d2 fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 628 diff changeset	317 ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	318 ( λ x → arrow (initial In (ob A U b x))) o FMap U f
629 693020c766d2 fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 628 diff changeset	319 ≈⟨⟩
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	320 tmap1 b o FMap U f
c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	321 ∎
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	322 comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj i) a ) →
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	323 (Sets [ FMap U f o (λ x → FMap U x (hom i OneObj))] ) y ≡
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	324 (Sets [ ( λ x → (FMap U x ) (hom i OneObj)) o (λ x → A [ f o x ] ) ] ) y
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	325 comm21 a b f y = begin
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	326 FMap U f ( FMap U y (hom i OneObj))
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	327 ≡⟨ ≡-cong ( λ k → k (hom i OneObj)) ( sym ( IsFunctor.distr (isFunctor U ) ) ) ⟩
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	328 (FMap U (A [ f o y ] ) ) (hom i OneObj)
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	329 ∎ where
c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	330 open import Relation.Binary.PropositionalEquality
c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	331 open ≡-Reasoning
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	332 tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (obj i)) b) (FObj U b)
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	333 tmap2 b x = ( FMap U x ) ( hom i OneObj )
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	334 comm2 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	335 Sets [ tmap2 b o FMap (Yoneda A (obj i)) f ] ]
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	336 comm2 {a} {b} {f} = let open ≈-Reasoning Sets in begin
c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	337 FMap U f o tmap2 a
c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	338 ≈⟨⟩
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	339 FMap U f o ( λ x → ( FMap U x ) ( hom i OneObj ) )
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	340 ≈⟨ extensionality Sets ( λ y → comm21 a b f y ) ⟩
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	341 ( λ x → ( FMap U x ) ( hom i OneObj ) ) o ( λ x → A [ f o x ] )
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	342 ≈⟨⟩
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	343 ( λ x → ( FMap U x ) ( hom i OneObj ) ) o FMap (Yoneda A (obj i)) f
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	344 ≈⟨⟩
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	345 tmap2 b o FMap (Yoneda A (obj i)) f
637 946ea019a2e7 if K{}↓U has initial Obj, U is representable done. Shinji KONO <kono@ie.u-ryukyu.ac.jp>* parents: 636 diff changeset	346 ∎
946ea019a2e7 if K{}↓U has initial Obj, U is representable done. Shinji KONO <kono@ie.u-ryukyu.ac.jp>* parents: 636 diff changeset	347 iso0 : ( x : Obj A) ( y : Hom A (obj i ) x ) ( z : * )
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	348 → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K Sets A *) y ] ) z
637 946ea019a2e7 if K{}↓U has initial Obj, U is representable done. Shinji KONO <kono@ie.u-ryukyu.ac.jp>* parents: 636 diff changeset	349 iso0 x y OneObj = refl
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	350 iso→ : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ]
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	351 iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≈-≡ A ( begin
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	352 ( Sets [ tmap1 x o tmap2 x ] ) y
626 c5abbd39e6eb on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 625 diff changeset	353 ≈⟨⟩
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	354 arrow ( initial In (ob A U x (( FMap U y ) ( hom i OneObj ) )))
637 946ea019a2e7 if K{}↓U has initial Obj, U is representable done. Shinji KONO <kono@ie.u-ryukyu.ac.jp>* parents: 636 diff changeset	355 ≈↑⟨ uniqueness In (record { arrow = y ; comm = extensionality Sets ( λ (z : * ) → iso0 x y z ) } ) ⟩
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	356 y
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	357 ∎ ))
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	358 iso← : {x : Obj A} → Sets [ Sets [ tmap2 x o tmap1 x ] ≈ id1 Sets (FObj U x) ]
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	359 iso← {x} = extensionality Sets ( λ (y : FObj U x ) → ( begin
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	360 ( Sets [ tmap2 x o tmap1 x ] ) y
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	361 ≡⟨⟩
638 a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	362 ( FMap U ( arrow ( initial In (ob A U x y ) )) ) ( hom i OneObj )
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	363 ≡⟨ ≡-cong (λ k → k OneObj) ( comm ( initial In (ob A U x y ) )) ⟩
a07b95e92933 creating nat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 637 diff changeset	364 hom (ob A U x y) OneObj
637 946ea019a2e7 if K{}↓U has initial Obj, U is representable done. Shinji KONO <kono@ie.u-ryukyu.ac.jp>* parents: 636 diff changeset	365 ≡⟨⟩
636 3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	366 y
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	367 ∎ ) ) where
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	368 open import Relation.Binary.PropositionalEquality
3e663c7f88c4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 635 diff changeset	369 open ≡-Reasoning
645 5f26af3f1c00 start adjoint Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 644 diff changeset	370
647 4d261d04b176 functorF and η Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 646 diff changeset	371 -------------
4d261d04b176 functorF and η Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 646 diff changeset	372 -- Adjoint Functor Theorem
4d261d04b176 functorF and η Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 646 diff changeset	373 --
4d261d04b176 functorF and η Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 646 diff changeset	374
648 10f2057c8bff use module Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 647 diff changeset	375 module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
10f2057c8bff use module Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 647 diff changeset	376 (U : Functor A B )
10f2057c8bff use module Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 647 diff changeset	377 (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) )
650 449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	378 (PI : (b : Obj B) → PreInitial (K B A b ↓ U) (SFSF (SFS b)))
449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	379 ( i : (b : Obj B) → Obj ( K B A b ↓ U) )
449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	380 (In : (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) )
648 10f2057c8bff use module Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 647 diff changeset	381 (LP : LimitPreserve A I B U ) where
10f2057c8bff use module Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 647 diff changeset	382
649 4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	383 tmap-η : (y : Obj B) → Hom B y (FObj U (obj (i y)))
4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	384 tmap-η y = hom (i y)
648 10f2057c8bff use module Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 647 diff changeset	385
652 236e916760e6 rewritw solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 651 diff changeset	386 sobj : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaObj (K B A a) U
236e916760e6 rewritw solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 651 diff changeset	387 sobj {a} {b} f = record {obj = b; hom = f }
236e916760e6 rewritw solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 651 diff changeset	388 solution : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaHom (K B A a) U (i a) (sobj f)
236e916760e6 rewritw solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 651 diff changeset	389 solution {a} {b} f = initial (In a) (sobj f)
647 4d261d04b176 functorF and η Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 646 diff changeset	390
654 2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	391 ηf : (a b : Obj B) → ( f : Hom B a b ) → Obj ( K B A a ↓ U)
2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	392 ηf a b f = sobj ( B [ tmap-η b o f ] )
2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	393
653 893ae9a95ee1 solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 652 diff changeset	394 univ : {a : Obj B} {b : Obj A} → (f : Hom B a (FObj U b))
652 236e916760e6 rewritw solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 651 diff changeset	395 → B [ B [ FMap U (arrow (solution f)) o tmap-η a ] ≈ f ]
653 893ae9a95ee1 solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 652 diff changeset	396 univ {a} {b} f = let open ≈-Reasoning B in begin
893ae9a95ee1 solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 652 diff changeset	397 FMap U (arrow (solution f)) o tmap-η a
893ae9a95ee1 solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 652 diff changeset	398 ≈⟨ comm (initial (In a) (sobj f)) ⟩
893ae9a95ee1 solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 652 diff changeset	399 hom (sobj f) o FMap (K B A a) (arrow (initial (In a) (sobj f)))
893ae9a95ee1 solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 652 diff changeset	400 ≈⟨ idR ⟩
893ae9a95ee1 solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 652 diff changeset	401 f
893ae9a95ee1 solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 652 diff changeset	402 ∎
652 236e916760e6 rewritw solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 651 diff changeset	403
654 2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	404 unique : {a : Obj B} { b : Obj A } → { f : Hom B a (FObj U b) } → { g : Hom A (obj (i a)) b} →
2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	405 B [ B [ FMap U g o tmap-η a ] ≈ f ] → A [ arrow (solution f) ≈ g ]
2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	406 unique {a} {b} {f} {g} ugη=f = let open ≈-Reasoning A in begin
2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	407 arrow (solution f)
2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	408 ≈↑⟨ ≡-≈ ( cong (λ k → arrow (solution k)) ( ≈-≡ B ugη=f )) ⟩
2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	409 arrow (solution (B [ FMap U g o tmap-η a ] ))
2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	410 ≈↑⟨ uniqueness (In a) (record { arrow = g ; comm = comm1 }) ⟩
2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	411 g
2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	412 ∎ where
2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	413 comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K B A a) g ] ]
2872af3b32cc uniquness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 653 diff changeset	414 comm1 = let open ≈-Reasoning B in sym idR
645 5f26af3f1c00 start adjoint Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 644 diff changeset	415
655 26a28b1cee6f universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 654 diff changeset	416 UM : UniversalMapping B A U (λ b → obj (i b)) (tmap-η)
26a28b1cee6f universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 654 diff changeset	417 UM = record {
26a28b1cee6f universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 654 diff changeset	418 _* = λ f → arrow (solution f) ;
26a28b1cee6f universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 654 diff changeset	419 isUniversalMapping = record {
26a28b1cee6f universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 654 diff changeset	420 universalMapping = λ {a} {b} {f} → univ f ;
26a28b1cee6f universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 654 diff changeset	421 uniquness = unique
26a28b1cee6f universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 654 diff changeset	422 }}
26a28b1cee6f universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 654 diff changeset	423
649 4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	424 F : Functor B A
4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	425 F = record {
647 4d261d04b176 functorF and η Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 646 diff changeset	426 FObj = λ b → obj (i b)
652 236e916760e6 rewritw solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 651 diff changeset	427 ; FMap = λ {x} {y} (f : Hom B x y ) → arrow (solution ( B [ tmap-η y o f ] ))
649 4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	428 ; isFunctor = record {
650 449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	429 identity = identity1
449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	430 ; distr = distr1
449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	431 ; ≈-cong = cong1
646 4e0f0105a85d add adjunction Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 645 diff changeset	432 }
649 4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	433 } where
651 1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	434 id1comm : {a : Obj B} → B [ B [ FMap U (arrow (initial (In a) (ηf a a (id1 B a)))) o hom (i a) ]
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	435 ≈ B [ hom (i a) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a)))) ] ]
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	436 id1comm {a} = let open ≈-Reasoning B in begin
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	437 FMap U (arrow (initial (In a) (ηf a a (id1 B a)))) o hom (i a)
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	438 ≈⟨ comm (initial (In a) (ηf a a (id1 B a))) ⟩
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	439 hom (ηf a a (id1 B a)) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a))))
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	440 ≈⟨ idR ⟩
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	441 hom (ηf a a (id1 B a))
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	442 ≈⟨⟩
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	443 hom (i a) o id1 B a
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	444 ≈⟨ idR ⟩
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	445 hom (i a)
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	446 ≈↑⟨ idR ⟩
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	447 hom (i a) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a))))
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	448 ∎
650 449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	449 identity1 : {a : Obj B} → A [ arrow (initial (In a) (ηf a a (id1 B a))) ≈ id1 A (obj (i a)) ]
651 1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	450 identity1 {a} = let open ≈-Reasoning A in begin
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	451 arrow (initial (In a) (ηf a a (id1 B a)))
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	452 ≈⟨ uniqueness (In a) (record { arrow = arrow (initial (In a) (ηf a a (id1 B a))); comm = id1comm }) ⟩
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	453 arrow (initial (In a) (i a))
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	454 ≈↑⟨ uniqueness (In a) (id1 ( K B A a ↓ U) (i a) ) ⟩
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	455 id1 A (obj (i a))
1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	456 ∎
648 10f2057c8bff use module Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 647 diff changeset	457 distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} →
650 449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	458 A [ arrow (initial (In a) (ηf a c (B [ g o f ]))) ≈
449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	459 A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ]
656 18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	460 distr1 {a} {b} {c} {f} {g} = unique (
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	461 let open ≈-Reasoning B in begin
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	462 FMap U (A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ) o tmap-η a
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	463 ≈⟨ car (IsFunctor.distr (isFunctor U )) ⟩
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	464 ( FMap U (arrow (initial (In b) (ηf b c g))) o FMap U (arrow (initial (In a) (ηf a b f))) )
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	465 o tmap-η a
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	466 ≈↑⟨ assoc ⟩
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	467 FMap U (arrow (initial (In b) (ηf b c g))) o
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	468 (FMap U (arrow (initial (In a) (ηf a b f))) o tmap-η a )
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	469 ≈⟨ cdr (univ ( tmap-η b o f )) ⟩
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	470 FMap U (arrow (initial (In b) (ηf b c g))) o ( tmap-η b o f )
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	471 ≈⟨ assoc ⟩
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	472 (FMap U (arrow (initial (In b) (ηf b c g))) o tmap-η b ) o f
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	473 ≈⟨ car ( univ (tmap-η c o g )) ⟩
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	474 (tmap-η c o g ) o f
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	475 ≈↑⟨ assoc ⟩
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	476 tmap-η c o ( g o f )
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	477 ∎
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	478 )
648 10f2057c8bff use module Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 647 diff changeset	479 cong1 : {a : Obj B} {b : Obj B} {f g : Hom B a b} →
650 449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	480 B [ f ≈ g ] → A [ arrow (initial (In a) (ηf a b f)) ≈ arrow (initial (In a) (ηf a b g)) ]
656 18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	481 cong1 {a} {b} {f} {g} f≈g = unique (
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	482 let open ≈-Reasoning B in begin
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	483 FMap U (arrow (initial (In a) (ηf a b g))) o tmap-η a
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	484 ≈⟨ univ ( tmap-η b o g ) ⟩
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	485 tmap-η b o g
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	486 ≈↑⟨ cdr f≈g ⟩
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	487 tmap-η b o f
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	488 ∎
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	489 )
645 5f26af3f1c00 start adjoint Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 644 diff changeset	490
656 18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	491 nat-ε : NTrans A A (F ○ U) identityFunctor
649 4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	492 nat-ε = record {
652 236e916760e6 rewritw solution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 651 diff changeset	493 TMap = λ x → arrow ( solution (id1 B (FObj U x)))
650 449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	494 ; isNTrans = record { commute = comm1 } } where
657 0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	495 lemma-nat1 : {a b : Obj A} {f : Hom A a b} →
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	496 B [ B [ FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a))
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	497 (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a) ]
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	498 ≈ B [ FMap U f o id1 B (FObj U a) ] ]
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	499 lemma-nat1 {a} {b} {f} = let open ≈-Reasoning B in begin
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	500 FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a))
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	501 (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a)
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	502 ≈⟨ car (distr U) ⟩
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	503 ( FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o FMap U (arrow (initial (In (FObj U a))
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	504 (record { obj = a ; hom = id1 B (FObj U a) })))) o (tmap-η (FObj U a))
658 9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	505 ≈↑⟨ assoc ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	506 FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o (FMap U (arrow (initial (In (FObj U a))
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	507 (record { obj = a ; hom = id1 B (FObj U a) }))) o tmap-η (FObj U a) )
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	508 ≈⟨ cdr ( univ (id1 B (FObj U a))) ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	509 FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o id1 B (FObj U a)
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	510 ≈⟨⟩
657 0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	511 FMap U f o id1 B (FObj U a)
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	512 ∎
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	513 lemma-nat2 : {a b : Obj A} {f : Hom A a b} →
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	514 B [ B [ FMap U (A [ arrow (initial (In (FObj U b))
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	515 (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a) ]
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	516 ≈ B [ FMap U f o id1 B (FObj U a) ] ]
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	517 lemma-nat2 {a} {b} {f} = let open ≈-Reasoning B in begin
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	518 FMap U (A [ arrow (initial (In (FObj U b))
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	519 (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a)
658 9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	520 ≈⟨ car (distr U) ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	521 ( FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })))
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	522 o FMap U ( FMap (F ○ U) f )) o tmap-η (FObj U a)
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	523 ≈↑⟨ assoc ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	524 FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })))
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	525 o ( FMap U ( FMap (F ○ U) f ) o tmap-η (FObj U a) )
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	526 ≈⟨ cdr ( univ ( tmap-η (FObj U b) o FMap U f ) ) ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	527 FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })))
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	528 o ( tmap-η (FObj U b) o FMap U f )
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	529 ≈⟨ assoc ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	530 ( FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })))
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	531 o tmap-η (FObj U b) ) o FMap U f
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	532 ≈⟨ car (univ (id1 B (FObj U b))) ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	533 id1 B (FObj U b) o FMap U f
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	534 ≈⟨ idL ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	535 FMap U f
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	536 ≈↑⟨ idR ⟩
657 0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	537 FMap U f o id1 B (FObj U a)
0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	538 ∎
648 10f2057c8bff use module Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 647 diff changeset	539 comm1 : {a b : Obj A} {f : Hom A a b} →
649 4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	540 A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o
648 10f2057c8bff use module Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 647 diff changeset	541 arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ]
650 449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	542 ≈ A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ]
656 18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	543 comm1 {a} {b} {f} = let open ≈-Reasoning A in begin
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	544 FMap (identityFunctor {_} {_} {_} {A}) f o
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	545 arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) }))
657 0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	546 ≈↑⟨ unique lemma-nat1 ⟩
656 18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	547 arrow (initial (In (FObj U a)) (record { obj = b ; hom = B [ FMap U f o id1 B (FObj U a) ] }))
657 0d029674eb59 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 656 diff changeset	548 ≈⟨ unique lemma-nat2 ⟩
656 18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	549 arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f
18431b63893b fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 655 diff changeset	550 ∎
645 5f26af3f1c00 start adjoint Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 644 diff changeset	551
649 4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	552 nat-η : NTrans B B identityFunctor (U ○ F)
4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	553 nat-η = record { TMap = λ y → tmap-η y ; isNTrans = record { commute = comm1 } } where
651 1503af5d7440 id of Functor F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 650 diff changeset	554 comm1 : {a b : Obj B} {f : Hom B a b} → B [ B [ FMap (U ○ F) f o tmap-η a ] ≈ B [ tmap-η b o f ] ]
647 4d261d04b176 functorF and η Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 646 diff changeset	555 comm1 {a} {b} {f} = let open ≈-Reasoning B in begin
649 4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	556 FMap (U ○ F) f o tmap-η a
647 4d261d04b176 functorF and η Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 646 diff changeset	557 ≈⟨⟩
650 449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	558 FMap U ( arrow ( initial (In a) (ηf a b f ))) o hom ( i a )
449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	559 ≈⟨ comm ( initial (In a) (ηf a b f)) ⟩
449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	560 ( tmap-η b o f ) o FMap (K B A a) (arrow (initial (In a) (ηf a b f)))
647 4d261d04b176 functorF and η Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 646 diff changeset	561 ≈⟨ idR ⟩
4d261d04b176 functorF and η Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 646 diff changeset	562 hom (i b ) o f
4d261d04b176 functorF and η Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 646 diff changeset	563 ≈⟨⟩
649 4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	564 tmap-η b o f
647 4d261d04b176 functorF and η Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 646 diff changeset	565 ∎
645 5f26af3f1c00 start adjoint Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 644 diff changeset	566
649 4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	567 FisLeftAdjoint : Adjunction B A U F nat-η nat-ε
4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	568 FisLeftAdjoint = record { isAdjunction = record {
650 449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	569 adjoint1 = adjoint1
449025d1327f fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 649 diff changeset	570 ; adjoint2 = adjoint2
646 4e0f0105a85d add adjunction Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 645 diff changeset	571 } } where
649 4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	572 adjoint1 : {b : Obj A} → B [ B [ FMap U (TMap nat-ε b) o TMap nat-η (FObj U b) ] ≈ id1 B (FObj U b) ]
658 9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	573 adjoint1 {b} = let open ≈-Reasoning B in begin
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	574 FMap U (TMap nat-ε b) o TMap nat-η (FObj U b)
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	575 ≈⟨ univ (id1 B (FObj U b)) ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	576 id1 B (FObj U b)
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	577 ∎
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	578 adj2comm1 : {a : Obj B} → B [ B [ FMap U (A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ]) o
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	579 tmap-η (FObj (identityFunctor {_} {_} {_} {B}) a) ] ≈ tmap-η a ]
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	580 adj2comm1 {a} = let open ≈-Reasoning B in begin
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	581 FMap U (A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ]) o tmap-η a
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	582 ≈⟨ car (distr U) ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	583 (FMap U (TMap nat-ε (FObj F a)) o FMap U (FMap F (TMap nat-η a) )) o tmap-η a
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	584 ≈↑⟨ assoc ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	585 FMap U (TMap nat-ε (FObj F a)) o (FMap U (FMap F (TMap nat-η a) ) o tmap-η a )
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	586 ≈⟨ cdr ( univ (tmap-η (FObj U (obj (i a))) o tmap-η a )) ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	587 FMap U (TMap nat-ε (FObj F a)) o (tmap-η (FObj U (obj (i a))) o tmap-η a )
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	588 ≈⟨ assoc ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	589 ( FMap U (TMap nat-ε (FObj F a)) o tmap-η (FObj U (obj (i a)))) o tmap-η a
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	590 ≈⟨ car (univ (id1 B (FObj U (FObj F a)))) ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	591 id1 B (FObj U (FObj F a)) o tmap-η a
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	592 ≈⟨ idL ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	593 tmap-η a
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	594 ∎
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	595 adj2comm2 : {a : Obj B} → B [ B [ FMap U (id1 A (FObj F a)) o tmap-η a ] ≈ tmap-η a ]
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	596 adj2comm2 {a} = let open ≈-Reasoning B in begin
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	597 FMap U (id1 A (FObj F a)) o tmap-η a
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	598 ≈⟨ car (IsFunctor.identity (isFunctor U)) ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	599 id1 B (FObj U (obj (i a))) o tmap-η a
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	600 ≈⟨ idL ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	601 tmap-η a
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	602 ∎
649 4d742e13fb7c module introdued Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 648 diff changeset	603 adjoint2 : {a : Obj B} → A [ A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ] ≈ id1 A (FObj F a) ]
658 9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	604 adjoint2 {a} = let open ≈-Reasoning A in begin
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	605 TMap nat-ε (FObj F a) o FMap F (TMap nat-η a)
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	606 ≈↑⟨ unique adj2comm1 ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	607 arrow (solution ( tmap-η a ) )
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	608 ≈⟨ unique adj2comm2 ⟩
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	609 id1 A (FObj F a)
9242298cffa8 adjoint functor theorem done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 657 diff changeset	610 ∎

Mercurial > hg > Members > kono > Proof > category

annotate freyd2.agda @ 658:9242298cffa8