module ThinSemiCategory where
open import Axioms public
open import InitialAlgebra public
open import Prelude public
record Thin (κ : Set) : Set₁ where
infix 4 _<_
field
_<_ : κ → κ → Prop
<< : ∀{x y z} → y < z → x < y → x < z
open Thin{{...}} public
{-# DISPLAY Thin._<_ _ i j = i < j #-}
infix 4 _<ᵇ_
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))
∏ᵇ :
{κ : 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
infix 6 _↓_
_↓_ :
{κ : Set}
{{_ : Thin κ}}
{l : Level}
{B : κ → Set l}
(f : (i : κ) → B i)
(i : κ)
→
∏ᵇ j < i , B j
(f ↓ _) j = f j
∀ᵇ :
{κ : 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}}
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
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
infix 6 _↓ᵇ_
_↓ᵇ_ :
{κ : 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