open import Category -- https://github.com/konn/category-agda open import Level open import Category.Sets renaming ( _o_ to _*_ ) module freyd2 where open import HomReasoning open import cat-utility open import Relation.Binary.Core open import Function ---------- -- -- a : Obj A -- U : A → Sets -- U ⋍ Hom (a,-) -- -- maybe this is a part of local smallness 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 import Relation.Binary.PropositionalEquality -- 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 ) postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ ---- -- -- Hom ( a, - ) is Object mapping in Yoneda Functor -- ---- open NTrans open Functor open Limit open IsLimit open import Category.Cat Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) Yoneda {c₁} {c₂} {ℓ} A a = record { FObj = λ b → Hom A a b ; 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) ; isFunctor = record { identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) } } where lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≈-≡ A idL lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≈-≡ A ( begin A [ A [ g o f ] o x ] ≈↑⟨ assoc ⟩ A [ g o A [ f o x ] ] ≈⟨⟩ ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) ∎ ) 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 ] lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≈-≡ A ( begin A [ f o x ] ≈⟨ resp refl-hom eq ⟩ A [ g o x ] ∎ ) -- Representable U ≈　Hom(A,-) record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where field -- FObj U x : A → Set -- FMap U f = Set → Set (locally small) -- λ b → Hom (a,b) : A → Set -- λ f → Hom (a,-) = λ b → Hom a b repr→ : NTrans A (Sets {c₂}) U (Yoneda A a ) repr← : NTrans A (Sets {c₂}) (Yoneda A a) U reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )] reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] open Representable open import freyd _↓_ : { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' } → ( F G : Functor A B ) → Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ _↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} { A } { B } F G = CommaCategory where open import Comma1 F G open SmallFullSubcategory open Complete open PreInitial open HasInitialObject open import Comma1 open CommaObj open LimitPreserve -- Representable Functor U preserve limit , so K{*}↓U is complete -- -- Yoneda A b = λ a → Hom A a b : Functor A Sets -- : Functor Sets A YonedaFpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) (b : Obj A ) (Γ : Functor I A) (limita : Limit A I Γ) → IsLimit Sets I (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (Yoneda A b)) YonedaFpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record { limit = λ a t → ψ a t ; t0f=t = λ {a t i} → t0f=t0 a t i ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t } where hat0 : NTrans I Sets (K Sets I (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ) hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b) haa0 : Obj Sets haa0 = FObj (Yoneda A b) (a0 lim) ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) → NTrans I A (K A I b ) Γ ta a x t = record { TMap = λ i → (TMap t i ) x ; isNTrans = record { commute = commute1 } } where commute1 : {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} → A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K A I b) f ] ] commute1 {a₁} {b₁} {f} = let open ≈-Reasoning A in begin FMap Γ f o TMap t a₁ x ≈⟨⟩ ( ( FMap (Yoneda A b ○ Γ ) f ) * TMap t a₁ ) x ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩ ( TMap t b₁ * ( FMap (K Sets I a) f ) ) x ≈⟨⟩ ( TMap t b₁ * id1 Sets a ) x ≈⟨⟩ TMap t b₁ x ≈↑⟨ idR ⟩ TMap t b₁ x o id1 A b ≈⟨⟩ TMap t b₁ x o FMap (K A I b) f ∎ ψ : (X : Obj Sets) ( t : NTrans I Sets (K Sets I X) (Yoneda A b ○ Γ)) → Hom Sets X (FObj (Yoneda A b) (a0 lim)) ψ X t x = FMap (Yoneda A b) (limit (isLimit lim) b (ta X x t )) (id1 A b ) t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) (i : Obj I) → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ] t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ) x ≈⟨⟩ FMap (Yoneda A b) ( TMap (t0 lim) i) (FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )) ≈⟨⟩ -- FMap (Hom A b ) f g = A [ f o g ] TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b ) ≈⟨ cdr idR ⟩ TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) ≈⟨ t0f=t (isLimit lim) ⟩ TMap (ta a x t) i ≈⟨⟩ TMap t i x ∎ )) limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} → ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o f ] ≈ TMap t i ]) → Sets [ ψ a t ≈ f ] limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin ψ a t x ≈⟨⟩ FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ) ≈⟨⟩ limit (isLimit lim) b (ta a x t ) o id1 A b ≈⟨ idR ⟩ limit (isLimit lim) b (ta a x t ) ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≡-≈ ( cong ( λ g → g x )( t0f=t {i} ))) ⟩ f x ∎ )) YonedaFpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b) YonedaFpreserveLimit A I b = record { preserve = λ Γ lim → YonedaFpreserveLimit0 A I b Γ lim } -- K{*}↓U has preinitial full subcategory if U is representable -- if U is representable, K{*}↓U has initial Object ( so it has preinitial full subcategory ) open CommaHom data * {c : Level} : Set c where OneObj : * KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → HasInitialObject ( K (Sets) A * ↓ (Yoneda A a) ) ( record { obj = a ; hom = λ x → id1 A a } ) KUhasInitialObj {c₁} {c₂} {ℓ} A a = record { initial = λ b → initial0 b ; uniqueness = λ f → unique f } where commaCat : Category (c₂ ⊔ c₁) c₂ ℓ commaCat = K Sets A * ↓ Yoneda A a initObj : Obj (K Sets A * ↓ Yoneda A a) initObj = record { obj = a ; hom = λ x → id1 A a } comm2 : (b : Obj commaCat) ( x : * ) → ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) x ≡ hom b x comm2 b OneObj = let open ≈-Reasoning A in ≈-≡ A ( begin ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) OneObj ≈⟨⟩ FMap (Yoneda A a) (hom b OneObj) (id1 A a) ≈⟨⟩ hom b OneObj o id1 A a ≈⟨ idR ⟩ hom b OneObj ∎ ) comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K Sets A *) (hom b OneObj) ] ] comm1 b = let open ≈-Reasoning Sets in begin FMap (Yoneda A a) (hom b OneObj) o ( λ x → id1 A a ) ≈⟨ extensionality A ( λ x → comm2 b x ) ⟩ hom b ≈⟨⟩ hom b o FMap (K Sets A *) (hom b OneObj) ∎ initial0 : (b : Obj commaCat) → Hom commaCat initObj b initial0 b = record { arrow = hom b OneObj ; comm = comm1 b } -- what is comm f ? comm-f : (b : Obj (K Sets A * ↓ (Yoneda A a))) (f : Hom (K Sets A * ↓ Yoneda A a) initObj b) → Sets [ Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ≈ Sets [ hom b o FMap (K Sets A *) (arrow f) ] ] comm-f b f = comm f unique : {b : Obj (K Sets A * ↓ Yoneda A a)} (f : Hom (K Sets A * ↓ Yoneda A a) initObj b) → (K Sets A * ↓ Yoneda A a) [ f ≈ initial0 b ] unique {b} f = let open ≈-Reasoning A in begin arrow f ≈↑⟨ idR ⟩ arrow f o id1 A a ≈⟨⟩ ( Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ] ) (id1 A a) ≈⟨⟩ ( Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj ≈⟨ ≡-≈ ( cong (λ k → k OneObj ) (comm f )) ⟩ ( Sets [ hom b o FMap (K Sets A *) (arrow f) ] ) OneObj ≈⟨⟩ hom b OneObj ∎ -- A is complete and K{*}↓U has preinitial full subcategory and U preserve limit then U is representable open SmallFullSubcategory open PreInitial -- if U preserve limit, K{*}↓U has initial object from freyd.agda ≡-cong = Relation.Binary.PropositionalEquality.cong ub : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b) ub A U b x OneObj = x ob : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b ) → Obj ( K Sets A * ↓ U) ob A U b x = record { obj = b ; hom = ub A U b x} fArrow : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) {a b : Obj A} (f : Hom A a b) (x : FObj U a ) → Hom ( K Sets A * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) ) fArrow A U {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x } where fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub A U a x y ) ≡ ub A U b (FMap U f x) y fArrowComm1 a b f x OneObj = refl fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → Sets [ Sets [ FMap U f o hom (ob A U a x) ] ≈ Sets [ hom (ob A U b (FMap U f x)) o FMap (K Sets A *) f ] ] fArrowComm a b f x = extensionality Sets ( λ y → begin ( Sets [ FMap U f o hom (ob A U a x) ] ) y ≡⟨⟩ FMap U f ( hom (ob A U a x) y ) ≡⟨⟩ FMap U f ( ub A U a x y ) ≡⟨ fArrowComm1 a b f x y ⟩ ub A U b (FMap U f x) y ≡⟨⟩ hom (ob A U b (FMap U f x)) y ∎ ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning -- if K{*}↓U has initial Obj, U is representable UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) ( i : Obj ( K (Sets) A * ↓ U) ) (In : HasInitialObject ( K (Sets) A * ↓ U) i ) → Representable A U (obj i) UisRepresentable A U i In = record { repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } } ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } } ; reprId→ = iso→ ; reprId← = iso← } where comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) → ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y ≡ (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y comm11 a b f y = begin ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y ≡⟨⟩ A [ f o arrow (initial In (ob A U a y)) ] ≡⟨⟩ A [ arrow ( fArrow A U f y ) o arrow (initial In (ob A U a y)) ] ≡⟨ ≈-≡ A ( uniqueness In {ob A U b (FMap U f y) } (( K Sets A * ↓ U) [ fArrow A U f y o initial In (ob A U a y)] ) ) ⟩ arrow (initial In (ob A U b (FMap U f y) )) ≡⟨⟩ (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y ∎ where open import Relation.Binary.PropositionalEquality open ≡-Reasoning tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj i)) b) tmap1 b x = arrow ( initial In (ob A U b x ) ) comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj i)) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ] comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin FMap (Yoneda A (obj i)) f o tmap1 a ≈⟨⟩ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In ( ob A U a x ))) ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ≈⟨⟩ tmap1 b o FMap U f ∎ comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj i) a ) → (Sets [ FMap U f o (λ x → FMap U x (hom i OneObj))] ) y ≡ (Sets [ ( λ x → (FMap U x ) (hom i OneObj)) o (λ x → A [ f o x ] ) ] ) y comm21 a b f y = begin FMap U f ( FMap U y (hom i OneObj)) ≡⟨ ≡-cong ( λ k → k (hom i OneObj)) ( sym ( IsFunctor.distr (isFunctor U ) ) ) ⟩ (FMap U (A [ f o y ] ) ) (hom i OneObj) ∎ where open import Relation.Binary.PropositionalEquality open ≡-Reasoning tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (obj i)) b) (FObj U b) tmap2 b x = ( FMap U x ) ( hom i OneObj ) comm2 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈ Sets [ tmap2 b o FMap (Yoneda A (obj i)) f ] ] comm2 {a} {b} {f} = let open ≈-Reasoning Sets in begin FMap U f o tmap2 a ≈⟨⟩ FMap U f o ( λ x → ( FMap U x ) ( hom i OneObj ) ) ≈⟨ extensionality Sets ( λ y → comm21 a b f y ) ⟩ ( λ x → ( FMap U x ) ( hom i OneObj ) ) o ( λ x → A [ f o x ] ) ≈⟨⟩ ( λ x → ( FMap U x ) ( hom i OneObj ) ) o FMap (Yoneda A (obj i)) f ≈⟨⟩ tmap2 b o FMap (Yoneda A (obj i)) f ∎ iso0 : ( x : Obj A) ( y : Hom A (obj i ) x ) ( z : * ) → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K Sets A *) y ] ) z iso0 x y OneObj = refl iso→ : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ] iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≈-≡ A ( begin ( Sets [ tmap1 x o tmap2 x ] ) y ≈⟨⟩ arrow ( initial In (ob A U x (( FMap U y ) ( hom i OneObj ) ))) ≈↑⟨ uniqueness In (record { arrow = y ; comm = extensionality Sets ( λ (z : * ) → iso0 x y z ) } ) ⟩ y ∎ )) iso← : {x : Obj A} → Sets [ Sets [ tmap2 x o tmap1 x ] ≈ id1 Sets (FObj U x) ] iso← {x} = extensionality Sets ( λ (y : FObj U x ) → ( begin ( Sets [ tmap2 x o tmap1 x ] ) y ≡⟨⟩ ( FMap U ( arrow ( initial In (ob A U x y ) )) ) ( hom i OneObj ) ≡⟨ ≡-cong (λ k → k OneObj) ( comm ( initial In (ob A U x y ) )) ⟩ hom (ob A U x y) OneObj ≡⟨⟩ y ∎ ) ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning ------------- -- Adjoint Functor Theorem -- module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I ) (U : Functor A B ) (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) ) (PI : (b : Obj B) → PreInitial (K B A b ↓ U) (SFSF (SFS b))) ( i : (b : Obj B) → Obj ( K B A b ↓ U) ) (In : (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) (LP : LimitPreserve A I B U ) where tmap-η : (y : Obj B) → Hom B y (FObj U (obj (i y))) tmap-η y = hom (i y) sobj : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaObj (K B A a) U sobj {a} {b} f = record {obj = b; hom = f } solution : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaHom (K B A a) U (i a) (sobj f) solution {a} {b} f = initial (In a) (sobj f) ηf : (a b : Obj B) → ( f : Hom B a b ) → Obj ( K B A a ↓ U) ηf a b f = sobj ( B [ tmap-η b o f ] ) univ : {a : Obj B} {b : Obj A} → (f : Hom B a (FObj U b)) → B [ B [ FMap U (arrow (solution f)) o tmap-η a ] ≈ f ] univ {a} {b} f = let open ≈-Reasoning B in begin FMap U (arrow (solution f)) o tmap-η a ≈⟨ comm (initial (In a) (sobj f)) ⟩ hom (sobj f) o FMap (K B A a) (arrow (initial (In a) (sobj f))) ≈⟨ idR ⟩ f ∎ unique : {a : Obj B} { b : Obj A } → { f : Hom B a (FObj U b) } → { g : Hom A (obj (i a)) b} → B [ B [ FMap U g o tmap-η a ] ≈ f ] → A [ arrow (solution f) ≈ g ] unique {a} {b} {f} {g} ugη=f = let open ≈-Reasoning A in begin arrow (solution f) ≈↑⟨ ≡-≈ ( cong (λ k → arrow (solution k)) ( ≈-≡ B ugη=f )) ⟩ arrow (solution (B [ FMap U g o tmap-η a ] )) ≈↑⟨ uniqueness (In a) (record { arrow = g ; comm = comm1 }) ⟩ g ∎ where comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K B A a) g ] ] comm1 = let open ≈-Reasoning B in sym idR UM : UniversalMapping B A U (λ b → obj (i b)) (tmap-η) UM = record { _* = λ f → arrow (solution f) ; isUniversalMapping = record { universalMapping = λ {a} {b} {f} → univ f ; uniquness = unique }} F : Functor B A F = record { FObj = λ b → obj (i b) ; FMap = λ {x} {y} (f : Hom B x y ) → arrow (solution ( B [ tmap-η y o f ] )) ; isFunctor = record { identity = identity1 ; distr = distr1 ; ≈-cong = cong1 } } where id1comm : {a : Obj B} → B [ B [ FMap U (arrow (initial (In a) (ηf a a (id1 B a)))) o hom (i a) ] ≈ B [ hom (i a) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a)))) ] ] id1comm {a} = let open ≈-Reasoning B in begin FMap U (arrow (initial (In a) (ηf a a (id1 B a)))) o hom (i a) ≈⟨ comm (initial (In a) (ηf a a (id1 B a))) ⟩ hom (ηf a a (id1 B a)) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a)))) ≈⟨ idR ⟩ hom (ηf a a (id1 B a)) ≈⟨⟩ hom (i a) o id1 B a ≈⟨ idR ⟩ hom (i a) ≈↑⟨ idR ⟩ hom (i a) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a)))) ∎ identity1 : {a : Obj B} → A [ arrow (initial (In a) (ηf a a (id1 B a))) ≈ id1 A (obj (i a)) ] identity1 {a} = let open ≈-Reasoning A in begin arrow (initial (In a) (ηf a a (id1 B a))) ≈⟨ uniqueness (In a) (record { arrow = arrow (initial (In a) (ηf a a (id1 B a))); comm = id1comm }) ⟩ arrow (initial (In a) (i a)) ≈↑⟨ uniqueness (In a) (id1 ( K B A a ↓ U) (i a) ) ⟩ id1 A (obj (i a)) ∎ distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} → A [ arrow (initial (In a) (ηf a c (B [ g o f ]))) ≈ A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ] distr1 {a} {b} {c} {f} {g} = unique ( let open ≈-Reasoning B in begin FMap U (A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ) o tmap-η a ≈⟨ car (IsFunctor.distr (isFunctor U )) ⟩ ( FMap U (arrow (initial (In b) (ηf b c g))) o FMap U (arrow (initial (In a) (ηf a b f))) ) o tmap-η a ≈↑⟨ assoc ⟩ FMap U (arrow (initial (In b) (ηf b c g))) o (FMap U (arrow (initial (In a) (ηf a b f))) o tmap-η a ) ≈⟨ cdr (univ ( tmap-η b o f )) ⟩ FMap U (arrow (initial (In b) (ηf b c g))) o ( tmap-η b o f ) ≈⟨ assoc ⟩ (FMap U (arrow (initial (In b) (ηf b c g))) o tmap-η b ) o f ≈⟨ car ( univ (tmap-η c o g )) ⟩ (tmap-η c o g ) o f ≈↑⟨ assoc ⟩ tmap-η c o ( g o f ) ∎ ) cong1 : {a : Obj B} {b : Obj B} {f g : Hom B a b} → B [ f ≈ g ] → A [ arrow (initial (In a) (ηf a b f)) ≈ arrow (initial (In a) (ηf a b g)) ] cong1 {a} {b} {f} {g} f≈g = unique ( let open ≈-Reasoning B in begin FMap U (arrow (initial (In a) (ηf a b g))) o tmap-η a ≈⟨ univ ( tmap-η b o g ) ⟩ tmap-η b o g ≈↑⟨ cdr f≈g ⟩ tmap-η b o f ∎ ) nat-ε : NTrans A A (F ○ U) identityFunctor nat-ε = record { TMap = λ x → arrow ( solution (id1 B (FObj U x))) ; isNTrans = record { commute = comm1 } } where lemma-nat1 : {a b : Obj A} {f : Hom A a b} → B [ B [ FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a) ] ≈ B [ FMap U f o id1 B (FObj U a) ] ] lemma-nat1 {a} {b} {f} = let open ≈-Reasoning B in begin FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a) ≈⟨ car (distr U) ⟩ ( FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o FMap U (arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })))) o (tmap-η (FObj U a)) ≈↑⟨ assoc ⟩ FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o (FMap U (arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) }))) o tmap-η (FObj U a) ) ≈⟨ cdr ( univ (id1 B (FObj U a))) ⟩ FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o id1 B (FObj U a) ≈⟨⟩ FMap U f o id1 B (FObj U a) ∎ lemma-nat2 : {a b : Obj A} {f : Hom A a b} → B [ B [ FMap U (A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a) ] ≈ B [ FMap U f o id1 B (FObj U a) ] ] lemma-nat2 {a} {b} {f} = let open ≈-Reasoning B in begin FMap U (A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a) ≈⟨ car (distr U) ⟩ ( FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) }))) o FMap U ( FMap (F ○ U) f )) o tmap-η (FObj U a) ≈↑⟨ assoc ⟩ FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) }))) o ( FMap U ( FMap (F ○ U) f ) o tmap-η (FObj U a) ) ≈⟨ cdr ( univ ( tmap-η (FObj U b) o FMap U f ) ) ⟩ FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) }))) o ( tmap-η (FObj U b) o FMap U f ) ≈⟨ assoc ⟩ ( FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) }))) o tmap-η (FObj U b) ) o FMap U f ≈⟨ car (univ (id1 B (FObj U b))) ⟩ id1 B (FObj U b) o FMap U f ≈⟨ idL ⟩ FMap U f ≈↑⟨ idR ⟩ FMap U f o id1 B (FObj U a) ∎ comm1 : {a b : Obj A} {f : Hom A a b} → A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ] ≈ A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ] comm1 {a} {b} {f} = let open ≈-Reasoning A in begin FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ≈↑⟨ unique lemma-nat1 ⟩ arrow (initial (In (FObj U a)) (record { obj = b ; hom = B [ FMap U f o id1 B (FObj U a) ] })) ≈⟨ unique lemma-nat2 ⟩ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ∎ nat-η : NTrans B B identityFunctor (U ○ F) nat-η = record { TMap = λ y → tmap-η y ; isNTrans = record { commute = comm1 } } where comm1 : {a b : Obj B} {f : Hom B a b} → B [ B [ FMap (U ○ F) f o tmap-η a ] ≈ B [ tmap-η b o f ] ] comm1 {a} {b} {f} = let open ≈-Reasoning B in begin FMap (U ○ F) f o tmap-η a ≈⟨⟩ FMap U ( arrow ( initial (In a) (ηf a b f ))) o hom ( i a ) ≈⟨ comm ( initial (In a) (ηf a b f)) ⟩ ( tmap-η b o f ) o FMap (K B A a) (arrow (initial (In a) (ηf a b f))) ≈⟨ idR ⟩ hom (i b ) o f ≈⟨⟩ tmap-η b o f ∎ FisLeftAdjoint : Adjunction B A U F nat-η nat-ε FisLeftAdjoint = record { isAdjunction = record { adjoint1 = adjoint1 ; adjoint2 = adjoint2 } } where adjoint1 : {b : Obj A} → B [ B [ FMap U (TMap nat-ε b) o TMap nat-η (FObj U b) ] ≈ id1 B (FObj U b) ] adjoint1 {b} = let open ≈-Reasoning B in begin FMap U (TMap nat-ε b) o TMap nat-η (FObj U b) ≈⟨ univ (id1 B (FObj U b)) ⟩ id1 B (FObj U b) ∎ adj2comm1 : {a : Obj B} → B [ B [ FMap U (A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ]) o tmap-η (FObj (identityFunctor {_} {_} {_} {B}) a) ] ≈ tmap-η a ] adj2comm1 {a} = let open ≈-Reasoning B in begin FMap U (A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ]) o tmap-η a ≈⟨ car (distr U) ⟩ (FMap U (TMap nat-ε (FObj F a)) o FMap U (FMap F (TMap nat-η a) )) o tmap-η a ≈↑⟨ assoc ⟩ FMap U (TMap nat-ε (FObj F a)) o (FMap U (FMap F (TMap nat-η a) ) o tmap-η a ) ≈⟨ cdr ( univ (tmap-η (FObj U (obj (i a))) o tmap-η a )) ⟩ FMap U (TMap nat-ε (FObj F a)) o (tmap-η (FObj U (obj (i a))) o tmap-η a ) ≈⟨ assoc ⟩ ( FMap U (TMap nat-ε (FObj F a)) o tmap-η (FObj U (obj (i a)))) o tmap-η a ≈⟨ car (univ (id1 B (FObj U (FObj F a)))) ⟩ id1 B (FObj U (FObj F a)) o tmap-η a ≈⟨ idL ⟩ tmap-η a ∎ adj2comm2 : {a : Obj B} → B [ B [ FMap U (id1 A (FObj F a)) o tmap-η a ] ≈ tmap-η a ] adj2comm2 {a} = let open ≈-Reasoning B in begin FMap U (id1 A (FObj F a)) o tmap-η a ≈⟨ car (IsFunctor.identity (isFunctor U)) ⟩ id1 B (FObj U (obj (i a))) o tmap-η a ≈⟨ idL ⟩ tmap-η a ∎ adjoint2 : {a : Obj B} → A [ A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ] ≈ id1 A (FObj F a) ] adjoint2 {a} = let open ≈-Reasoning A in begin TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ≈↑⟨ unique adj2comm1 ⟩ arrow (solution ( tmap-η a ) ) ≈⟨ unique adj2comm2 ⟩ id1 A (FObj F a) ∎