{-# OPTIONS --type-in-type #-}

module Playground.Category where

open import Agda.Builtin.Equality public

_∘_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
_∘_ f g x = f (g x)

postulate
  funext : (A : Set)(B : A → Set)(f g : (a : A) → B a) → ((a : A) → f a ≡ g a) → f ≡ g

record Category (Obj : Set) (Hom : Obj → Obj → Set) : Set where
  field
    id : (A : Obj) → Hom A A
    comp : {A B C : Obj} → Hom B C → Hom A B → Hom A C
    left-id : {A B : Obj}(f : Hom A B) → comp (id B) f ≡ f
    right-id : {A B : Obj}(f : Hom A B) → comp f (id A) ≡ f
    comp-assoc : {A B C D : Obj}(f : Hom C D)(g : Hom B C)(h : Hom A B)
               → comp (comp f g) h ≡ comp f (comp g h)

open Category

ArrowCategory : Category Set (\x y → x → y)
id ArrowCategory A = λ x → x
comp ArrowCategory {A} {B} {C} f g = f ∘ g
left-id ArrowCategory {A} {B} f =
  funext A (\a → B) (comp ArrowCategory (id ArrowCategory B) f) f (\a → refl)
right-id ArrowCategory {A} {B} f =
  funext A (\a → B) (comp ArrowCategory f (id ArrowCategory A)) f (\a → refl)
comp-assoc ArrowCategory {A} {B} {C} {D} f g h =
  funext A (\a → D) (comp ArrowCategory (comp ArrowCategory f g) h) (comp ArrowCategory f (comp ArrowCategory g h)) (\a → refl)

data Void : Set where

record Unit : Set where
  constructor top

Unit-singleton : (x : Unit) → x ≡ top
Unit-singleton top = refl

Unit-Terminal : {A : Set} → A → Unit
Unit-Terminal {A} a = top

Void-Initial : {A : Set} → Void → A
Void-Initial {A} ()

VoidHom : Void → Void → Set
VoidHom ()

VoidCat : Category Void VoidHom
id VoidCat ()
comp VoidCat {()}
left-id VoidCat {()}
right-id VoidCat {()}
comp-assoc VoidCat {()}

UnitHom : Unit → Unit → Set
UnitHom top top = Unit

UnitCat : Category Unit UnitHom
id UnitCat A = top
comp UnitCat top top = top
left-id UnitCat top = refl
right-id UnitCat top = refl
comp-assoc UnitCat top top top = refl

record Pair (A : Set) (B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

data Either (A : Set) (B : Set) : Set where
  inl : A → Either A B
  inr : B → Either A B

PairEqlProof : {A B : Set}(p : Pair A B)(q : Pair A B)(a : Pair.fst p ≡ Pair.fst q)(b : Pair.snd p ≡ Pair.snd q) → (p ≡ q)
PairEqlProof {A} {B} (p , q) (.p , .q) refl refl = refl

-- EitherInlInrProof : {A B : Set}(x : Either A B) → Either (a : A , x = Either.inl a) (b : B , x = Either.inr b)

record IsTerminal {Obj : Set}{Hom : Obj -> Obj -> Set}(C : Category Obj Hom)(T : Obj) : Set where
  field
    terminate : (A : Obj) → Hom A T
    unique-terminal : {A : Obj}(a : Hom A T) → a ≡ (terminate A)

open IsTerminal

UnitTerminal : IsTerminal UnitCat top
terminate UnitTerminal top = top
unique-terminal UnitTerminal top = refl

ArrowTerminal : IsTerminal ArrowCategory Unit
terminate ArrowTerminal A x = top
unique-terminal ArrowTerminal a = refl

comm-eql : {A : Set}{x y : A}(a : x ≡ y) → (y ≡ x)
comm-eql refl = refl

OppositeCat : {Obj : Set}{Hom : Obj -> Obj -> Set}(C : Category Obj Hom) → (Category Obj (\x y → Hom y x))
id (OppositeCat c) = id c
comp (OppositeCat c) x y = comp c y x
left-id (OppositeCat c) f = right-id c f
right-id (OppositeCat c) f = left-id c f
comp-assoc (OppositeCat c) f g h = comm-eql (comp-assoc c h g f)

record IsInitial {Obj : Set}{Hom : Obj → Obj → Set}(C : Category Obj Hom)(I : Obj) : Set where
  field
    initiate : (A : Obj) → Hom I A
    unique-initial : {A : Obj}(a : Hom I A) → a ≡ (initiate A)

open IsInitial

UnitInitial : IsInitial UnitCat top
initiate UnitInitial A = top
unique-initial UnitInitial a = refl

ArrowInitial : IsInitial ArrowCategory Void
initiate ArrowInitial A = Void-Initial
unique-initial ArrowInitial a = {!!}