Π-types in precategories with families

Content created by Daniel Gratzer, Egbert Rijke and Elisabeth Stenholm.

Created on 2023-11-27.
Last modified on 2023-11-27.

module type-theories.pi-types-precategories-with-families where
Imports
open import foundation.equivalences
open import foundation.identity-types
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import type-theories.precategories-with-families

Idea

A precategory with families 𝒯 is said to have Π-types if it comes equipped with the following structure:

  • An operation Π : (A : Ty Γ) → Ty (ext Γ A) → Ty Γ for every context Γ,
  • A family of equivalences Tm Γ (Π A B) ≃ Tm (ext Γ A) B,

that are compatible with the substitution structure on 𝒯.

Definitions

The structure of Π-types on a precategory with families

record
  Π-structure-Precategory-With-Families
    (l1 l2 l3 l4 : Level) (cwf : Precategory-With-Families l1 l2 l3 l4) :
    UU (l1  l2  l3  l4)
  where

  open Precategory-With-Families cwf

  field
    Π : {Γ : Ctx} (A : Ty Γ) (B : Ty (ext Γ A))  Ty Γ
    iso-Π :
      {Γ : Ctx} (A : Ty Γ) (B : Ty (ext Γ A))  Tm Γ (Π A B)  Tm (ext Γ A) B

  app : {Γ : Ctx} (A : Ty Γ) (B : Ty (ext Γ A))  Tm Γ (Π A B)  Tm (ext Γ A) B
  app A B = map-equiv (iso-Π A B)

  lam : {Γ : Ctx} (A : Ty Γ) (B : Ty (ext Γ A))  Tm (ext Γ A) B  Tm Γ (Π A B)
  lam A B = map-inv-equiv (iso-Π A B)

  field
    substitution-law-Π :
      {Γ Δ : Ctx} (A : Ty Δ) (B : Ty (ext Δ A)) (σ : Sub Γ Δ) 
      (Π A B) · σ  Π (A · σ) (B ·  σ , A )
    substitution-law-iso-Π :
      {Γ Δ : Ctx} (A : Ty Δ) (B : Ty (ext Δ A)) (σ : Sub Γ Δ) 
      (t : Tm Δ (Π A B)) 
      app
        ( A · σ)
        ( B ·  σ , A )
        ( tr (Tm Γ) (substitution-law-Π A B σ) (t [ σ ])) 
      app A B t [  σ , A  ]

Recent changes