Free Locally Cartesian Closed Categories

lccc.agda

{-# OPTIONS --cubical -Wignore #-}
module lccc where
open import Cubical.Foundations.Prelude

data Obj : Type
data Hom : Obj → Obj → Type

variable
  A B C D X Y : Obj
  f g h u v e : Hom A B

infixl 5 _∘_

data Obj where
  ⋆ : isSet Obj
  𝟙 : Obj
  _⋈_ : Hom A X → Hom B X → Obj
  Π : Hom B X → Hom A B → Obj

data Hom where
  ⋆ : isSet (Hom A B)

  id : Hom A A
  _∘_ : Hom B C → Hom A B → Hom A C
  idₗ : id ∘ f ≡ f
  idᵣ : f ∘ id ≡ f
  assoc : f ∘ (g ∘ h) ≡ f ∘ g ∘ h

  𝟙 : Hom A 𝟙
  η𝟙 : f ≡ 𝟙

  π₁ : (f : Hom A X) (g : Hom B X) → Hom (f ⋈ g) A
  π₂ : (f : Hom A X) (g : Hom B X) → Hom (f ⋈ g) B
  β⋈ : f ∘ π₁ f g ≡ g ∘ π₂ f g

  ⟨_,_⟩[_] : (u : Hom Y A) (v : Hom Y B)
    → f ∘ u ≡ g ∘ v
    → Hom Y (f ⋈ g)
  η⋈₁ : ∀ {p} → π₁ f g ∘ ⟨ u , v ⟩[ p ] ≡ u
  η⋈₂ : ∀ {p} → π₂ f g ∘ ⟨ u , v ⟩[ p ] ≡ v

  υ : (f : Hom B X) (g : Hom A B) → Hom (Π f g) X
  ε : (f : Hom B X) (g : Hom A B) → Hom (υ f g ⋈ f) A
  βΠ : g ∘ ε f g ≡ π₂ (υ f g) f

  ƛ : {f : Hom B X} {g : Hom A B}
    → (u : Hom Y X) (e : Hom (u ⋈ f) A)
    → g ∘ e ≡ π₂ u f
    → Hom Y (Π f g)
  ηΠυ : ∀ {p} → υ f g ∘ ƛ u e p ≡ u
  ηΠε : {f : Hom B X} {g : Hom A B} {u : Hom Y X} {e : Hom (u ⋈ f) A}
    → (p : g ∘ e ≡ π₂ u f)
    → ε f g ∘
      ⟨ ƛ u e p ∘ π₁ u f , π₂ u f ⟩[ assoc ∙∙ cong (_∘ π₁ u f) ηΠυ ∙∙ β⋈ ]
      ≡ e