Reference · Finite types, distributions and Markov chains

rainbow.math.finite.subtype

Finite types, distributions and Markov chains src/rainbow/math/finite/subtype.clj0 definitions, 5 theorems

Finite propositions and finite-subtype bridges as checked proof data.

type/finite-proposition

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7Source, line 79

type/finite-proposition :
  (P : Prop)
  → type/finite P

type/finite-of-subsingleton

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 123

type/finite-of-subsingleton.{l} :
  (A : Sort l) (subsingleton : type/subsingleton A)
  → type/finite A

subtype/extensional

TheoremFor all inputsAxioms: sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7Source, line 187

subtype/extensional.{u} :
  (A : Type u) (source : set/Set A) (left right : data/Subtype A source)
  (same-value : subtype/value A source left = subtype/value A source right)
  → left = right

= = equality/Eq

set/finite-subtype-equivalence

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7Source, line 290

set/finite-subtype-equivalence.{u} :
  (A : Type u) (source : set/Set A)
  → proposition/conjunction (set/finite A source → type/finite (data/Subtype A source)) (type/finite (data/Subtype A source) → set/finite A source)

set/finite-subtype-proposition-equality

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 356

set/finite-subtype-proposition-equality.{u} :
  (A : Type u) (source : set/Set A)
  → set/finite A source = type/finite (data/Subtype A source)

= = equality/Eq