Mercurial > hg > Members > kono > Proof > category

comparison src/freyd2.agda @ 1115:5620d4a85069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
1114:ce23d2b47c5e 1115:5620d4a85069
322 322
323 ------------- 323 -------------
324 -- Adjoint Functor Theorem 324 -- Adjoint Functor Theorem
325 -- 325 --
326 326
327 module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I ) 327 module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete {c₁} {c₂} {ℓ} A )
328 (U : Functor A B ) 328 (U : Functor A B )
329 (i : (b : Obj B) → Obj ( K A B b ↓ U) ) 329 (i : (b : Obj B) → Obj ( K A B b ↓ U) )
330 (In : (b : Obj B) → HasInitialObject ( K A B b ↓ U) (i b) ) 330 (In : (b : Obj B) → HasInitialObject ( K A B b ↓ U) (i b) )
331 where 331 where
332 332