module ThinSemiCategory where

open import Axioms public
open import InitialAlgebra public
open import Prelude public

----------------------------------------------------------------------
-- Small thin semi-categories
----------------------------------------------------------------------
record Thin (κ : Set) : Set₁ where
  infix  _<_
  field
    _<_   : κ → κ → Prop
    << : ∀{x y z} → y < z → x < y → x < z

open Thin{{...}} public

{-# DISPLAY Thin._<_ _ i j = i < j #-}

----------------------------------------------------------------------
-- Use instance search for proofs about <
----------------------------------------------------------------------
infix  _<ᵇ_
record _<ᵇ_  {κ : Set}{{_ : Thin κ}}(i j : κ) : Prop where
  constructor <inst
  field <prf : i < j

open _<ᵇ_ public

instance
  <ᵇ<ᵇ :
    {κ : Set}
    {{_ : Thin κ}}
    {i j k : κ}
    {{q : j <ᵇ k}}
    {{p : i <ᵇ j}}
    → ------------
    i <ᵇ k
  <ᵇ<ᵇ {{q = q}} {{p}} = <inst (<< (<prf q) (<prf p))

-- Bounded dependent function
∏ᵇ :
  {κ : Set}
  {{_ : Thin κ}}
  (i : κ)
  {l : Level}
  (B : (j : κ){{_ : j <ᵇ i}} → Set l)
  → ---------------------------------
  Set l
∏ᵇ {κ} i B = (j : κ){{_ : j <ᵇ i}} → B j

syntax ∏ᵇ i (λ j → B) = ∏ᵇ j < i , B

-- Restricting functions
infix  _↓_
_↓_ :
  {κ : Set}
  {{_ : Thin κ}}
  {l : Level}
  {B : κ → Set l}
  (f : (i : κ) → B i)
  (i : κ)
  → -----------------
  ∏ᵇ j < i , B j
(f ↓ _) j = f j

-- Bounded universal quantification
∀ᵇ :
  {κ : Set}
  {{_ : Thin κ}}
  (i : κ)
  {l : Level}
  (P : (j : κ){{_ : j <ᵇ i}} → Prop l)
  → ----------------------------------
  Prop l
∀ᵇ i P =  ∀ j  → {{_ : j <ᵇ i}} → P j

syntax ∀ᵇ i (λ j → P) = ∀ᵇ j < i , P

funᵇ-ext :
  {κ : Set}
  {{_ : Thin κ}}
  {i : κ}
  {l : Level}
  {B : (j : κ){{_ : j <ᵇ i}} → Set l}
  {f f' : ∏ᵇ i B}
  (_ : ∀ᵇ j < i , (f j ≡ f' j))
  → ---------------------------------
  f ≡ f'
funᵇ-ext e =
  funext λ j →
  instance-funexp λ p → e j {{p}}

-- Bounded dependent product
record ∑ᵇ
  {κ : Set}
  {{_ : Thin κ}}
  (i : κ)
  {l : Level}
  (B : (j : κ){{_ : j <ᵇ i}} → Set l)
  : ---------------------------------
  Set l
  where
  constructor pairᵇ
  field
    fst      : κ
    {{fst<}} : fst <ᵇ i
    snd      : B fst
open ∑ᵇ public

syntax ∑ᵇ i (λ j → B) = ∑ᵇ j < i , B

-- Bounded existential quantification
data ∃ᵇ
  {κ : Set}
  {{_ : Thin κ}}
  (i : κ)
  {l : Level}
  (P : (j : κ){{_ : j <ᵇ i}} → Prop l)
  : ----------------------------------
  Prop l
  where
    ∃ᵇi : (j : κ){{_ : j <ᵇ i}} → P j → ∃ᵇ i P

syntax ∃ᵇ i (λ j → P) = ∃ᵇ j < i , P

-- Restricting bounded functions
infix  _↓ᵇ_
_↓ᵇ_ :
  {κ : Set}
  {{_ : Thin κ}}
  {i : κ}
  {l : Level}
  {B : ∏ᵇ j < i , Set l}
  (f : ∏ᵇ j < i , B j)
  (j : κ)
  {{_ : j <ᵇ i}}
  → --------------------
  ∏ᵇ k < j , B k
(f ↓ᵇ _) k = f k