Large dependent pair types

{-# OPTIONS --safe #-}
module foundation.large-dependent-pair-types where

open import foundation-core.universe-levels

Idea

When B is a family of large types over A, then we can form the large type of pairs pairω a b consisting of an element a : A and an element b : B a. Such pairs are called dependent pairs, since the type of the second component depends on the first component.

Definition

record Σω (A : UUω) (B : A → UUω) : UUω where
  constructor pairω
  field
    prω1 : A
    prω2 : B prω1

open Σω public

infixr  _,ω_
pattern _,ω_ a b = pairω a b

Families on dependent pair types

module _
  {l : Level} {A : UUω} {B : A → UUω}
  where

  fam-Σω : ((x : A) → B x → UU l) → Σω A B → UU l
  fam-Σω C (pairω x y) = C x y