Home

積型

module foundations.product-type where
Imports
open import foundations.universe
import foundations.sigma-type as S
open S using (Σ)
open S using (_,_; fst; snd) public
private variable  ℓ′ : Level

_×_ : Type   Type ℓ′  Type (  ℓ′)
A × B = Σ A  _  B)