Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 645:5f26af3f1c00

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
start adjoint
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jul 2017 16:40:34 +0900
parents 8e35703ef116
children 4e0f0105a85d
comparison
equal deleted inserted replaced
644:8e35703ef116 645:5f26af3f1c00
372 ≡⟨⟩ 372 ≡⟨⟩
373 y 373 y
374 ∎ ) ) where 374 ∎ ) ) where
375 open import Relation.Binary.PropositionalEquality 375 open import Relation.Binary.PropositionalEquality
376 open ≡-Reasoning 376 open ≡-Reasoning
377
378
379 FunctorF : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
380 (U : Functor A B )
381 (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) )
382 (PI : (b : Obj B) → PreInitial (K B A b ↓ U) (SFSF (SFS b)))
383 (LP : LimitPreserve A I B U )
384 → Functor B A
385 FunctorF = {!!}
386
387 nat-ε : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
388 (U : Functor A B )
389 (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) )
390 (PI : (b : Obj B) → PreInitial (K B A b ↓ U) (SFSF (SFS b)))
391 (LP : LimitPreserve A I B U )
392 → NTrans A A ( (FunctorF A B I comp U SFS PI LP) ○ U ) identityFunctor
393 nat-ε = {!!}
394
395 nat-η : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
396 (U : Functor A B )
397 (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) )
398 (PI : (b : Obj B) → PreInitial (K B A b ↓ U) (SFSF (SFS b)))
399 (LP : LimitPreserve A I B U )
400 → NTrans B B identityFunctor (U ○ (FunctorF A B I comp U SFS PI LP) )
401 nat-η = {!!}
402
403 IsLeftAdjoint : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
404 (U : Functor A B )
405 (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) )
406 (PI : (b : Obj B) → PreInitial (K B A b ↓ U) (SFSF (SFS b)))
407 (LP : LimitPreserve A I B U )
408 → Adjunction B A U (FunctorF A B I comp U SFS PI LP)
409 (nat-η A B I comp U SFS PI LP) (nat-ε A B I comp U SFS PI LP)
410 IsLeftAdjoint = {!!}