Mercurial > hg > Members > kono > Proof > category

annotate freyd2.agda @ 608:7194ba55df56

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
freyd2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 12 Jun 2017 10:50:02 +0900
parents 01a0dda67a8b
children d686d7ae38e0
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
497
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Category -- https://github.com/konn/category-agda
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Category.Sets
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 module freyd2
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 where
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import HomReasoning
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import cat-utility
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Binary.Core
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Function
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 ----------
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 --
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 -- a : Obj A
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 -- U : A → Sets
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 -- U ⋍ Hom (a,-)
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 --
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 -- A is Locally small
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
21
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
22 ----
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
23 -- C is locally small i.e. Hom C i j is a set c₁
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
24 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
25 record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
26 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
27 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
28 hom→ : {i j : Obj C } → Hom C i j → I
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
29 hom← : {i j : Obj C } → ( f : I ) → Hom C i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
30 hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
31
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
32 open Small
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
33
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
34
497
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 postulate ≈-≡ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 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
38 -- 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
39 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
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
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 ----
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 -- Hom ( a, - ) is Object mapping in co Yoneda Functor
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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 ----
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 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
49 open Functor
498
c981a2f0642f UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 497
diff changeset
50 open Limit
c981a2f0642f UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 497
diff changeset
51 open IsLimit
c981a2f0642f UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 497
diff changeset
52 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
53
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 HomA : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 HomA {c₁} {c₂} {ℓ} A a = record {
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 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
57 ; 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
58 ; 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
59 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
60 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
61 ≈-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
62 }
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 } where
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-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≈-≡ {_} {_} {_} {A} idL
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 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
67 A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≈-≡ {_} {_} {_} {A} ( begin
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 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
70 ≈↑⟨ assoc ⟩
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 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
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 ( λ 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
74 ∎ )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ]
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≈-≡ {_} {_} {_} {A} ( begin
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 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
78 ≈⟨ 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
79 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
80 ∎ )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
502
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
83
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
84 record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (b : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
85 field
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
86 -- FObj U x : A → Set
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
87 -- FMap U f = Set → Set
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
88 -- λ b → Hom (a,b) : A → Set
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
89 -- λ f → Hom (a,-) = λ b → Hom a b
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
90
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
91 repr→ : NTrans A (Sets {c₂}) U (HomA A b )
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
92 repr← : NTrans A (Sets {c₂}) (HomA A b) U
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
93 reprId : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
94 reprId : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
95
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
96 open import freyd
502
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
97
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
98 _↓_ : { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
99 → ( F G : Functor A B )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
100 → Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
101 _↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} { A } { B } F G = CommaCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
102 where open import Comma1 F G
498
c981a2f0642f UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 497
diff changeset
103
499
511fd37d90ec prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 498
diff changeset
104
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
105 open import freyd
499
511fd37d90ec prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 498
diff changeset
106
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
107 -- K{*}↓U has preinitial full subcategory then U is representable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
108
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
109 open SmallFullSubcategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
110 open Complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
111 open PreInitial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
112
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
113 data OneObject : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
114 * : OneObject
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
115
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
116 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
117 (comp : Complete A A)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
118 (U : Functor A (Sets) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
119 (SFS : SmallFullSubcategory ( K (Sets) {!!} {!!} ↓ U )) →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
120 (PI : PreInitial {!!} (SFSF SFS )) → Representable A U {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
121 UisRepresentable = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
122
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
123 -- K{*}↓U has preinitial full subcategory if U is representable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
124
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
125 KUhasSFS : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
126 (comp : Complete A A)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
127 (U : Functor A (Sets) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
128 (a : Obj A )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
129 (R : Representable A U a ) →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
130 SmallFullSubcategory {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
131 KUhasSFS = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
132
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
133 KUhasPreinitial : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
134 (comp : Complete A A)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
135 (U : Functor A (Sets) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
136 (a : Obj A )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
137 (R : Representable A U a ) →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
138 PreInitial {!!} (SFSF (KUhasSFS A comp U a R ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
139 KUhasPreinitial = {!!}