55 lines
1.8 KiB
Agda
55 lines
1.8 KiB
Agda
{-# OPTIONS --allow-unsolved-metas #-}
|
||
module Cat.Categories.Fam where
|
||
|
||
open import Agda.Primitive
|
||
open import Data.Product
|
||
open import Cubical
|
||
import Function
|
||
|
||
open import Cat.Category
|
||
open import Cat.Equality
|
||
|
||
open Equality.Data.Product
|
||
|
||
module _ (ℓa ℓb : Level) where
|
||
private
|
||
Obj' = Σ[ A ∈ Set ℓa ] (A → Set ℓb)
|
||
Arr : Obj' → Obj' → Set (ℓa ⊔ ℓb)
|
||
Arr (A , B) (A' , B') = Σ[ f ∈ (A → A') ] ({x : A} → B x → B' (f x))
|
||
one : {o : Obj'} → Arr o o
|
||
proj₁ one = λ x → x
|
||
proj₂ one = λ b → b
|
||
_∘_ : {a b c : Obj'} → Arr b c → Arr a b → Arr a c
|
||
(g , g') ∘ (f , f') = g Function.∘ f , g' Function.∘ f'
|
||
_⟨_∘_⟩ : {a b : Obj'} → (c : Obj') → Arr b c → Arr a b → Arr a c
|
||
c ⟨ g ∘ f ⟩ = _∘_ {c = c} g f
|
||
|
||
module _ {A B C D : Obj'} {f : Arr A B} {g : Arr B C} {h : Arr C D} where
|
||
isAssociative : (D ⟨ h ∘ C ⟨ g ∘ f ⟩ ⟩) ≡ D ⟨ D ⟨ h ∘ g ⟩ ∘ f ⟩
|
||
isAssociative = Σ≡ refl refl
|
||
|
||
module _ {A B : Obj'} {f : Arr A B} where
|
||
isIdentity : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f
|
||
isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
|
||
|
||
|
||
RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
|
||
RawFam = record
|
||
{ Object = Obj'
|
||
; Arrow = Arr
|
||
; 𝟙 = one
|
||
; _∘_ = λ {a b c} → _∘_ {a} {b} {c}
|
||
}
|
||
|
||
instance
|
||
isCategory : IsCategory RawFam
|
||
isCategory = record
|
||
{ isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {D = D} {f} {g} {h}
|
||
; isIdentity = λ {A} {B} {f} → isIdentity {A} {B} {f = f}
|
||
; arrowsAreSets = {!!}
|
||
; univalent = {!!}
|
||
}
|
||
|
||
Fam : Category (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
|
||
Category.raw Fam = RawFam
|