UniAgda.Core.SetsAndLogic.Props

Table of Contents

1 Prelude

2 The unit is a proposition

3 Results

3.2 Equivalence of propositions

Two propositions are equivalent if and only if they are logically equivalent.

props-equiv : {i j : Level} {P : Type i} {Q : Type j}
          isProp P  isProp Q  (P  Q)  (Q  P)
          P  Q
props-equiv {i} {j} {P} {Q} X Y f g = equiv-adjointify (f , g , ((λ y  Y ((f o g) y) y) , λ x  X ((g o f) x) x))

Being a proposition is preserved under equivalence.

equiv-with-prop :  {i j} {A : Type i} {B : Type j}
                   A  B  isProp A
                   isProp B
equiv-with-prop (f , g , α , β , γ) F x y = (((ap f (F (g y) (g x)))  β x) ^)  β y

3.4 Being a set or proposition is a proposition

3.6 Propositions are preserved under products

Given a two proposition, their product is a proposition.

prod-of-props-is-prop :  {i j} {A : Type i} {B : Type j}
                         isProp A  isProp B
                         isProp (A × B)
prod-of-props-is-prop H H' (a , b) (a' , b') =
  path-equiv-prod
    ((H a a') , (H' b b'))

Author: James Leslie

Created: 2021-03-27 Sat 10:47