UniAgda.Core.UniversalProperties

Table of Contents

1 Prelude

2 Products

2.1 Mapping in

into-product :  {i j k} {A : Type i} {B : Type j} {X : Type k}
                  (X  A × B)
                  (X  A) × (X  B)
into-product f = pr₁ o f , pr₂ o f
into-product-is-equiv :  {i j k} {A : Type i} {B : Type j} {X : Type k}
                         isEquiv (into-product {A = A} {B = B} {X = X})
into-product-is-equiv {A = A} {B = B} {X = X} =
  isequiv-adjointify
    ((λ { (f , g) x  (f x) , (g x)}) ,
     { (f , g)  refl}) ,
    λ f  funext λ x  path-equiv-prod (refl , refl))
into-product-dep :  {i j k} {X : Type i} {A : X  Type j} {B : X  Type k}
                      ((x : X)  (A x × B x))
                      ((x : X)  A x) × ((x : X)  B x)
into-product-dep F =  x  pr₁ (F x)) ,  x  pr₂ (F x))
into-product-dep-is-equiv :  {i j k} {X : Type i} {A : X  Type j} {B : X  Type k}
                             isEquiv (into-product-dep {X = X} {A = A} {B = B})
into-product-dep-is-equiv =
  isequiv-adjointify
    ((λ { (F , G) x  F x , G x}) ,
     { (F , G)  refl}) ,
    λ { F  funextD λ x  path-equiv-prod (refl , refl)})
into-dep-product :  {i j k} {X : Type i} {A : X  Type j} {P : (x : X)  A x  Type k}
                      ((x : X)  Σ[ a  (A x) ] P x a)
                      (Σ[ g  ((x : X)  A x) ] ((x : X)  P x (g x)))
into-dep-product F =  x  pr₁ (F x)) ,  x  pr₂ (F x))
into-dep-product-is-equiv :  {i j k} {X : Type i} {A : X  Type j} {P : (x : X)  A x  Type k}
                             isEquiv (into-dep-product {X = X} {A = A} {P = P})
into-dep-product-is-equiv =
  isequiv-adjointify
    ((λ { (F , G) x  (F x) , (G x)}) ,
     { (F , G)  refl}) ,
    λ F  funextD λ x  path-equiv-sigma (refl , refl))

3 Path Induction

4 Coproducts

5 Unit

6 Empty

7 Pullbacks

Author: James Leslie

Created: 2021-03-27 Sat 10:47