Categories.Category.Closed.Instance.Sets.agda

open import Level

module Categories.Category.Closed.Instance.Sets (o : Level) where

open import Categories.Category
open import Categories.Category.Instance.Sets
open import Categories.Category.Closed (Sets o)

open import Axiom.Extensionality.Propositional
open import Data.Product
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality hiding (Extensionality)

closed : Extensionality _ _ → Closed
closed extensionality = record
  { [-,-] = record
    { F₀ = λ {(A , B) → A → B}
    ; F₁ = λ {(f , g) h → g ∘ h ∘ f}
    ; identity = refl
    ; homomorphism = refl
    ; F-resp-≈ = λ {_} {_} {f} {g} pq {h} → extensionality λ _ → begin
               proj₂ f ∘ h ∘ proj₁ f
                 ≈⟨ proj₂ pq ⟩
               proj₂ g ∘ h ∘ proj₁ f
                 ≈⟨ cong (proj₂ g ∘ h) (proj₁ pq) ⟩
               proj₂ g ∘ h ∘ proj₁ g
                 ∎
    }
  ; unit = Lift _ ⊤
  ; identity = record
    { F⇒G = record
      { η = λ _ x _ → x
      ; commute = λ _ → refl
      ; sym-commute = λ _ → refl
      }
    ; F⇐G = record
      { η = λ _ f → f (lift tt)
      ; commute = λ _ → refl
      ; sym-commute = λ _ → refl
      }
    ; iso = λ X → record
      { isoˡ = refl
      ; isoʳ = refl
      }
    }
  ; diagonal = record
    { α = λ _ _ x → x
    ; commute = λ _ → refl
    ; op-commute = λ _ → refl
    }
  ; L = λ _ _ _ f g x → f (g x)
  ; L-natural-comm = refl
  ; L-dinatural-comm = refl
  ; Lj≈j = refl
  ; jL≈i = refl
  ; iL≈i = refl
  ; pentagon = refl
  ; γ⁻¹ = record
    { _⟨$⟩_ = λ f → f (lift tt)
    ; cong = λ p → cong-app p _
    }
  ; γ-inverseOf-γ⁻¹ = record
    { left-inverse-of = λ _ → refl
    ; right-inverse-of = λ _ → refl 
    }
  }
  where
    open Category.HomReasoning (Sets _) hiding (refl)