Mercurial > hg > Members > kono > Proof > category

comparison freyd.agda @ 695:7a6ee564e3a8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 Nov 2017 13:31:35 +0900
parents 984518c56e96
children
comparison
equal deleted inserted replaced
694:2043f7fd4273 695:7a6ee564e3a8
46 open IsEqualizer 46 open IsEqualizer
47 47
48 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 48 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
49 (comp : Complete A A) 49 (comp : Complete A A)
50 (SFS : FullSubcategory A ) → 50 (SFS : FullSubcategory A ) →
51 (PI : PreInitial A (FSF SFS )) → IsInitialObject A (limit-c comp (FSF SFS)) 51 (PI : PreInitial A (FSF SFS )) → HasInitialObject A (limit-c comp (FSF SFS))
52 initialFromPreInitialFullSubcategory A comp SFS PI = record { 52 initialFromPreInitialFullSubcategory A comp SFS PI = record {
53 initial = initialArrow ; 53 initial = initialArrow ;
54 uniqueness = λ {a} f → lemma1 a f 54 uniqueness = λ {a} f → lemma1 a f
55 } where 55 } where
56 F : Functor A A 56 F : Functor A A