open import Level using (Level)
-- open import Category.Core
-- open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-- open import Data.Product using (_×_; Σ-syntax; _,_)
-- open Category
-- open Functor

module Category.Instances.Cat {ℓ₁ ℓ₂ ℓ₃ : Level} where

-- Cat : Category
-- Cat .Obj = Category {ℓ₁} {ℓ₂} {ℓ₃}
-- Cat .Hom 𝐂 𝐃 = Functor 𝐂 𝐃
-- -- Cat ._≈_ {𝐂} {𝐃} 𝐅₁ 𝐅₂ = (∀ a → F₀ 𝐅₁ a ≡ F₀ 𝐅₂ a) × (∀ f → (_≈_ 𝐃) (F₁ 𝐅₁ f) {!!})
-- Cat ._≈_ {𝐂} {𝐃} 𝐅₁ 𝐅₂ = Σ[ h ∈ (∀ a → F₀ 𝐅₁ a ≡ F₀ 𝐅₂ a) ]
--     ∀ {a b : Obj 𝐂} → ∀ (f : Hom 𝐂 a b) → {!!}
--     where
--         transport : (a b : Obj 𝐂)
--                   → (F₀ 𝐅₁ a ≡ F₀ 𝐅₂ a)
--                   → (F₀ 𝐅₁ b ≡ F₀ 𝐅₂ b)
--                   → (Hom 𝐃 (F₀ 𝐅₁ a) (F₀ 𝐅₁ b))
--                   → (Hom 𝐃 (F₀ 𝐅₂ a) (F₀ 𝐅₂ b))
--         transport a b h₁ h₂ H = {!!}
-- Cat ._∘_ = {!!}
-- Cat .𝟙 = {!!}
-- Cat .assoc = {!!}
-- Cat .identity-ˡ = {!!}
-- Cat .identity-ʳ = {!!}
-- Cat .equiv = {!!}
-- Cat .≈-resp-∘ = {!!}