{-# OPTIONS --without-K #-}
module function.core where

open import level

-- copied from Agda's standard library

infixr 9 _∘'_
infixr 0 _$_

_∘'_ :  {a b c}
      {A : Set a} {B : A  Set b} {C : {x : A}  B x  Set c} 
      (∀ {x} (y : B x)  C y)  (g : (x : A)  B x) 
      ((x : A)  C (g x))
f ∘' g = λ x  f (g x)

const :  {a b} {A : Set a} {B : Set b}  A  B  A
const x = λ _  x

_$_ :  {a b} {A : Set a} {B : A  Set b} 
      ((x : A)  B x)  ((x : A)  B x)
f $ x = f x

flip :  {a b c} {A : Set a} {B : Set b} {C : A  B  Set c} 
       ((x : A) (y : B)  C x y)  ((y : B) (x : A)  C x y)
flip f = λ y x  f x y

record Composition u₁ u₂ u₃ u₁₂ u₂₃ u₁₃
        : Set (lsuc (u₁  u₂  u₃  u₁₂  u₂₃  u₁₃)) where
  infixl 9 _∘_
  field
    U₁ : Set u₁
    U₂ : Set u₂
    U₃ : Set u₃

    hom₁₂ : U₁  U₂  Set u₁₂
    hom₂₃ : U₂  U₃  Set u₂₃
    hom₁₃ : U₁  U₃  Set u₁₃

    _∘_ : {X₁ : U₁}{X₂ : U₂}{X₃ : U₃}  hom₂₃ X₂ X₃  hom₁₂ X₁ X₂  hom₁₃ X₁ X₃

record Identity u e : Set (lsuc (u  e)) where
  field
    U : Set u
    endo : U  Set e
    id : {X : U}  endo X

func-comp :  {i j k}  Composition _ _ _ _ _ _
func-comp {i}{j}{k} = record
  { U₁ = Set i
  ; U₂ = Set j
  ; U₃ = Set k
  ; hom₁₂ = λ X Y  X  Y
  ; hom₂₃ = λ X Y  X  Y
  ; hom₁₃ = λ X Y  X  Y
  ; _∘_ = λ f g x  f (g x) }

func-id :  {i}  Identity _ _
func-id {i} = record
  { U = Set i
  ; endo = λ X  X  X
  ; id = λ x  x }

module ComposeInterface {u₁ u₂ u₃ u₁₂ u₂₃ u₁₃}
                         comp : Composition u₁ u₂ u₃ u₁₂ u₂₃ u₁₃  where
  open Composition comp public using (_∘_)
open ComposeInterface public

module IdentityInterface {i e}
                          identity : Identity i e  where
  open Identity identity public using (id)
open IdentityInterface public