Sigma.idr

Lemma

Projecting both sides of a sigma and building a new sigma is the same as doing nothing.

sigmaProjId : {0 a : Type} -> {0 b : a -> Type} ->
              (x : Σ a b) -> (x.π1 ## x.π2) === x
sigmaProjId ((f ## s)) = Refl

Definition

Equality between sigma types is ensure when both the first and second projection are equal.

record SigEq (a, b : Σ f s) where
  constructor MkSigEq
  fstEq : a.π1 === b.π1
  sndEq : (a.π2 ≡≡ b.π2) {p = s}
 
export 0
sigEqRefl : (x : Σ f s) -> SigEq x x
sigEqRefl x = MkSigEq Refl (IRefl Refl)

The equality between sigma types relies on indexed propositional equality \defref{def:ix-eq} since the second projection is indexed by the first.

Lemma

We can convert from Σ-equality to propositional equality

0 sigEqToEq : SigEq a b -> a === b
sigEqToEq {a = _ ## _} {b = _ ## _} (MkSigEq Refl (IRefl Refl)) = Refl