Mercurial > hg > Members > kono > Proof > category
diff src/freyd2.agda @ 1115:5620d4a85069
safe rewriting nearly finished
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Jul 2024 11:44:58 +0900 |
| parents | 0e750446e463 |
| children |
line wrap: on
line diff
--- a/src/freyd2.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/freyd2.agda Wed Jul 03 11:44:58 2024 +0900 @@ -324,7 +324,7 @@ -- Adjoint Functor Theorem -- -module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I ) +module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete {c₁} {c₂} {ℓ} A ) (U : Functor A B ) (i : (b : Obj B) → Obj ( K A B b ↓ U) ) (In : (b : Obj B) → HasInitialObject ( K A B b ↓ U) (i b) )