Σ-types Properties

1. Σ Properties

1 Σ Properties

module Lib.Prop.Σ where

This file proves some useful basic facts on Σ-types.

1.1 Packages imports

The imported packages can be accessed via the following links:

Lib/Prop/Paths

import Stdlib.Prelude
import Lib.Prop.Paths

1.2 Induction principle

ind-Σ (A : U) (B : A → U) (P : Σ A B → U) (g : (x : A) (y : B x) → P(x, y)) : (z : Σ A B) → P z =
  λz. g z.1 z.2

1.3 Accessors

pr1 (A : U) (B : A → U) (u : Σ A B) : A = u.1
pr2 (A : U) (B : A → U) (u : Σ A B) : B (pr1 A B u) = u.2

1.4 Properties

1.4.1 Σ-Path implies subpaths

Let u, v be Σ-types such that u = v. Then, by path induction, we have p : u.1 = v.1 and (tr p u.2) = v.2.

Sg-path/left (A : U) (B : A → U) (u v : Σ A B) (p : Path (Σ A B) u v) : Path A u.1 v.1 =
  λi. (p i).1

PathSg→SgPathO (A : U) (B : A → U) (u v : Σ A B) : Path (Σ A B) u v → SgPathO A B u v =
  coe 0 1 (i. PathSg-eq-SgPathO A B u v i)

Sg-path/right (A : U) (B : A → U) (u v : Σ A B) (p : Path (Σ A B) u v)
                 : PathO A u.1 v.1 (PathSg→SgPathO A B u v p).1 B u.2 v.2 =
  (PathSg→SgPathO A B u v p).2

1.4.2 Closed retract

If B, C are type families over A and B a retract of C, then Σ A B is also a retract of Σ A C.

Sg/closed-retract (A : U) (B C : A → U) (H : (x : A) → retract-of (B x) (C x)) : retract-of (Σ A B) (Σ A C) =
  let s : Σ A B → Σ A C = λu. (u.1, (H u.1).1 u.2)
      r : Σ A C → Σ A B = λu. (u.1, (H u.1).2.1 u.2) in
  (s, (r, λu. SgPathO→PathΣ A B (r (s u)) u (refl A u.1, PathO/refl A u.1 B (r (s u)).2 u.2 ((H u.1).2.2 u.2))))