module CatDef where

{-
This file contains the category theoretic definitions.
-}
 
open import Basics

Mor :  (A : Set₁) → Set₁
Mor A = A → A → Set

record Cat : Set₂ where
 field
  Obj : Set₁
  _⇒_ : Obj → Obj → Set
  _≈_ : ∀ {M N} → Rel (M ⇒ N)
  isEq : ∀ {M N} →  isEquivalence (M ⇒ N) _≈_ 
  id : ∀ {N} → N ⇒ N
  _⊚_ : ∀ {M N O} → M ⇒ N → N ⇒ O → M ⇒ O
  id1 : ∀ {M N} → (f : M ⇒ N) → (id ⊚ f) ≈ f
  id2 : ∀ {M N} →  (g : M ⇒ N)  → (g ⊚ id) ≈ g 
  asso : ∀ {M N O P} → (f : M ⇒ N) → (g : N ⇒ O) → (h : O ⇒ P) → ((f ⊚ g) ⊚ h) ≈ (f ⊚ (g ⊚ h))  
  resp :  ∀ {M N O} → (_⊚_ {M}{N}{O}) Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_      


open Cat public

record Terminal (ℂ : Cat) : Set₁ where
   field
     Ter : Obj ℂ
     A→T : (A : Obj ℂ) → (_⇒_ ℂ) A Ter
     uni : (A : Obj ℂ) → (f : (_⇒_ ℂ) A Ter) → (_≈_ ℂ) (A→T A) f

record Initial (ℂ : Cat) : Set₁ where
   field
     Ini : Obj ℂ
     I→A : (A : Obj ℂ) → (_⇒_ ℂ) Ini A
     uni : (A : Obj ℂ) → (f : (_⇒_ ℂ) Ini A) → (_≈_ ℂ) (I→A A) f


record Product {ℂ : Cat}(X Y : Obj ℂ) : Set₁ where
  field
    X×Y : Obj ℂ
    π₁ : (_⇒_ ℂ) X×Y X
    π₂ : (_⇒_ ℂ) X×Y Y
    〈_,_〉 : ∀ {Z} → (_⇒_ ℂ) Z X → (_⇒_ ℂ) Z Y → (_⇒_ ℂ) Z X×Y

    c₁ : ∀ {Z}{f : (_⇒_ ℂ) Z X}{g : (_⇒_ ℂ) Z Y} → (_≈_ ℂ)((_⊚_ ℂ) 〈 f , g 〉 π₁) f
    c₂ : ∀ {Z}{f : (_⇒_ ℂ) Z X}{g : (_⇒_ ℂ) Z Y} → (_≈_ ℂ)((_⊚_ ℂ) 〈 f , g 〉 π₂) g  
    uni : ∀ {Z}{f : (_⇒_ ℂ) Z X}{g : (_⇒_ ℂ) Z Y}{h : (_⇒_ ℂ) Z X×Y} → (_≈_ ℂ)((_⊚_ ℂ) h π₁) f → (_≈_ ℂ) ((_⊚_ ℂ) h π₂) g → (_≈_ ℂ) 〈 f , g 〉 h

open Product public


record CarCat : Set₂ where
 field
  Ucat : Cat
  UTer : Terminal Ucat
  UProd : (X Y : Obj Ucat) → Product {Ucat} X Y

open CarCat public

record Coproduct {ℂ : Cat}(X Y : Obj ℂ) : Set₁ where
  field
    X+Y : Obj ℂ
    i₁ : (_⇒_ ℂ) X X+Y
    i₂ : (_⇒_ ℂ) Y X+Y
    [[_,_]] : ∀ {Z} → (_⇒_ ℂ) X Z → (_⇒_ ℂ) Y Z → (_⇒_ ℂ) X+Y Z

    c₁' : ∀ {Z}{f : (_⇒_ ℂ) X Z}{g : (_⇒_ ℂ) Y Z} → (_≈_ ℂ)((_⊚_ ℂ) i₁ [[ f , g ]]) f
    c₂' : ∀ {Z}{f : (_⇒_ ℂ) X Z}{g : (_⇒_ ℂ) Y Z} → (_≈_ ℂ)((_⊚_ ℂ) i₂ [[ f , g ]]) g  
    uni' : ∀ {Z}{f : (_⇒_ ℂ) X Z}{g : (_⇒_ ℂ) Y Z}{h : (_⇒_ ℂ) X+Y Z} → (_≈_ ℂ)((_⊚_ ℂ) i₁ h) f → (_≈_ ℂ) ((_⊚_ ℂ) i₂ h) g → (_≈_ ℂ) [[ f , g ]] h

record CoCarCat : Set₂ where
 field
  UCcat : Cat
  UIni : Initial UCcat
  UCoProd : (X Y : Obj UCcat) → Coproduct {UCcat} X Y

open CoCarCat public

Pair⇒ : {ℂ : CarCat} → (X Y Z W : Obj (Ucat ℂ)) → (XZ : ((_⇒_ (Ucat ℂ)) X Z)) → (YW : ((_⇒_ (Ucat ℂ)) Y W)) → (_⇒_ (Ucat ℂ)) (X×Y (UProd ℂ X Y)) (X×Y (UProd ℂ Z W))
Pair⇒ {ℂ} X Y Z W XZ YW = (〈_,_〉 (UProd ℂ Z W)) ((_⊚_ (Ucat ℂ)) (π₁ (UProd ℂ X Y)) XZ) ((_⊚_ (Ucat ℂ)) (π₂ (UProd ℂ X Y)) YW)   

record Exp {ℂ : CarCat}(X Y : Obj (Ucat ℂ)) : Set₁ where
  field
   Yˣ : Obj (Ucat ℂ)
   app : (_⇒_ (Ucat ℂ)) (X×Y (UProd ℂ Yˣ X)) Y
   curr : (Z : Obj (Ucat ℂ)) → (f : (_⇒_ (Ucat ℂ)) (X×Y (UProd ℂ Z X)) Y) → ((_⇒_ (Ucat ℂ)) Z Yˣ)
   comm : (Z : Obj (Ucat ℂ)) → (f : (_⇒_ (Ucat ℂ)) (X×Y (UProd ℂ Z X)) Y) → (_≈_ (Ucat ℂ))((_⊚_ (Ucat ℂ)) (Pair⇒ {ℂ} Z X Yˣ X (curr Z f) ((id (Ucat ℂ)) {X})) app) f
   univ : (Z : Obj (Ucat ℂ)) → (f : (_⇒_ (Ucat ℂ)) (X×Y (UProd ℂ Z X)) Y) → (h : (_⇒_ (Ucat ℂ)) Z Yˣ) → (_≈_ (Ucat ℂ))((_⊚_ (Ucat ℂ)) (Pair⇒ {ℂ} Z X Yˣ X h ((id (Ucat ℂ)) {X})) app) f → (_≈_ (Ucat ℂ)) (curr Z f) h

open Exp public


record CCC : Set₂ where
 field
  CarC : CarCat
  exp : (X Y : Obj (Ucat CarC)) → Exp {CarC} X Y

record Functor (C : Cat) (D : Cat) : Set₁ where
  field
   onObj : (Obj C) → (Obj D)
   onMor : (X Y : Obj C) → (f : (_⇒_ C) X Y) → (_⇒_ D) (onObj X)(onObj Y)
   res≈ : (X Y : Obj C) → (f g : (_⇒_ C) X Y) → (_≈_ C) f g → (_≈_ D) (onMor X Y f) (onMor X Y g)
   onId : (X : Obj C) → (_≈_ D) (onMor X X ((id C) {X})) ((id D) {onObj X})
   onComp : (X Y Z : Obj C) → (f : (_⇒_ C) X Y) → (g : (_⇒_ C) Y Z) → (_≈_ D) ((_⊚_ D) (onMor X Y f) (onMor Y Z g)) (onMor X Z ((_⊚_ C) f g))  

open Functor public


record Adjoint (C D : Cat) (F : Functor C D)(G : Functor D C) : Set₁ where
  field
   counit : (X : Obj D) → (_⇒_ D) ((onObj F) ((onObj G) X)) X 
   f̂ : (X : Obj D) → (Y : Obj C) → (_⇒_ D) ((onObj F) Y) X → (_⇒_ C) Y ((onObj G) X)
   f̂ε : (X : Obj D) → (Y : Obj C) → (f : ((_⇒_ D) ((onObj F) Y) X)) → (_≈_ D) ((_⊚_ D) ((onMor F) Y ((onObj G) X) (f̂ X Y f)) (counit X)) f
   unif̂ : (X : Obj D) → (Y : Obj C) → (f : ((_⇒_ D) ((onObj F) Y) X)) → (g : (_⇒_ C) Y ((onObj G) X)) → (_≈_ D) ((_⊚_ D) ((onMor F) Y ((onObj G) X) g) (counit X)) f → (_≈_ C) g (f̂ X Y f)

open Adjoint public

record Pullbacks (C : Cat) (X Y Z : Obj C) (f : (_⇒_ C) X Z)(g : (_⇒_ C) Y Z) : Set₁ where
  field
   X⊗Y : Obj C
   X⊗Y→X : (_⇒_ C) X⊗Y  X
   X⊗Y→Y :  (_⇒_ C) X⊗Y  Y
   f∘p₁≡g∘p₂ : (_≈_ C) ((_⊚_ C) X⊗Y→X  f) ((_⊚_ C) X⊗Y→Y  g)
   W→X⊗Y : (W : Obj C) → (f' : (_⇒_ C) W X) → (g' : (_⇒_ C) W Y) → (_≈_ C) ((_⊚_ C) f' f) ((_⊚_ C) g' g) → (_⇒_ C) W  X⊗Y
   WXY₁ :  (W : Obj C) → (f' : (_⇒_ C) W X) → (g' : (_⇒_ C) W Y) → (f'g' : (_≈_ C) ((_⊚_ C) f' f) ((_⊚_ C) g' g)) → (_≈_ C) ((_⊚_ C) (W→X⊗Y W f' g' f'g') X⊗Y→X) f'
   WXY₂ : (W : Obj C) → (f' : (_⇒_ C) W X) → (g' : (_⇒_ C) W Y) → (f'g' : (_≈_ C) ((_⊚_ C) f' f) ((_⊚_ C) g' g)) → (_≈_ C) ((_⊚_ C) (W→X⊗Y W f' g' f'g') X⊗Y→Y) g'
   W↠X⊗Y : (W : Obj C) → (f' : (_⇒_ C) W X) → (g' : (_⇒_ C) W Y) → (f'g' : (_≈_ C) ((_⊚_ C) f' f) ((_⊚_ C) g' g)) → (h : (_⇒_ C) W X⊗Y) → (_≈_ C) ((_⊚_ C) h X⊗Y→X) f' → (_≈_ C) ((_⊚_ C) h X⊗Y→Y) g' 
                                                                                                                                                                                                                                                             → (_≈_ C) (W→X⊗Y W f' g' f'g') h
open Pullbacks public

record CatPull (C : Cat) : Set₁ where
  field
    Pulls : (X Y Z : Obj C) → (f : (_⇒_ C) X Z) → (g : (_⇒_ C) Y Z) → Pullbacks C X Y Z f g

record Iso {C : Cat}(X Y : Obj C) : Set where
 field
  liso : (_⇒_ C) X Y
  riso : (_⇒_ C) Y X
  idisl : (_≈_ C) ((_⊚_ C) liso riso) ((id C) {X})
  idisr : (_≈_ C) ((_⊚_ C) riso liso) ((id C) {Y})

record Nat (C D : Cat) (F G : Functor C D) : Set₁ where
 field
  trf : (X : Obj C) → (_⇒_ D) ((onObj F) X) ((onObj G) X)
  ntsq : (X Y : Obj C) → (f : (_⇒_ C) X Y) → (_≈_ D) ((_⊚_ D) (trf X) ((onMor G) X Y f)) ((_⊚_ D) ((onMor F) X Y f) (trf Y))

-------------------------------------------------------------------------------------------------------------