Module prop::path_semantics

source · [−]

Expand description

Path Semantics

Path Semantics has a core axiom which is used to model mathematics.

This core axiom is modelled here, lifting proof of path semantical order to expressions of propositions.

For more information, see https://github.com/advancedresearch/path_semantics.

Re-exports

pub use quality::Q;

pub use quality::EqQ;

pub use quality::left as refl_left;

pub use quality::right as refl_right;

Structs

LTrue

True for a path semantical level.

POrdProof

Proof of path semantical order.

Traits

DLProp

Shorthand for decidable proposition with path semantical level.

ELProp

Shorthand for existential proposition with path semantical level.

LProp

Path semantical proposition level.

Lookup

Look by index.

POrd

Path semantical order.

SortMax

Sorts two types.

SortMin

Sorts two types.

Functions

assume

Assumes the core axiom safely for propositions.

assume_inc_path_level

Generates naive core axiom at increased path semantical proposition level.

assume_naive

Assume naive core axiom safely.

assume_norm_path_level

Assume a normalised naive core axiom.

assume_refl

Generates a naive core axiom which has reflection as end-lines.

check_q

Checks that X is qual to T.

comp

Composition.

creation

Creation theorem.

creation_hom

Creation theorem using homotopy map.

eq_lev

Checks whether two proposition levels are equal.

true == ltrue.

(x ~~ x) == x.

x.

Checks whether a proposition level is less than another.

naive_comp

Composition using the naive core axiom.

naive_red_false

Reduce naive core axiom in case of false to equality of associated propositions.

pand_both_eq

Use both PAndFst and PAndSnd to prove a = b.

q_true

true ~~ x.

qlim

(x ~~ x) ~~ x.

to_naive

Converts to naive core axiom.

to_pand_fst

Converts core axiom to PAndFst.

to_pand_snd

Converts core axiom to PAndSnd.

to_por_fst

Converts core axiom to POrFst.

to_por_snd

Converts core axiom to POrSnd.

true_q

x ~~ x.

ty_and

(x : a) ⋀ (y : b) => ((x ⋀ y) : (a ⋀ b)).

ty_eqq_imply

(x : a) ⋀ (y : b) ⋀ eqq(x, y) => ((x => y) : (a => b)).

ty_hom_imply

(x : a) ⋀ (y : b) ⋀ hom(x, y) => ((x => y) : (a => b)).

ty_in_left_arg

(a : b) ⋀ (a == c) => (c : b).

ty_in_right_arg

(a : b) ⋀ (b == c) => (a : c).

ty_ltrue

x : ltrue.

ty_or

(x : a) ⋀ (y : b) => ((x ⋁ y) : (a ⋁ b)).

ty_or_split_da

(a : (b ⋁ c)) => (a : b) ⋁ (a : c).

ty_or_split_db

(a : (b ⋁ c)) => (a : b) ⋁ (a : c).

ty_or_split_dc

(a : (b ⋁ c)) => (a : b) ⋁ (a : c).

ty_true

x : true.

uniq_ty

Proves that types are unique.

use_pand_both

Use both PAndFst and PAndSnd.

xy_norm

Constructs a 2D naive core axiom from two naive core axioms, where one is normalised of the other.

Type Definitions

Inc

Increases level one step.

IncLevel

Increases proposition level of A with some amount N.

LN

Look up type N among the normalised A, B, C, D.

Max

Returns the maximum LProp.

MaxMax

The decided maximum (4th of 4).

MaxMin

The undecided maximum minimum.

Maxi

The decided maximum of undecided middle (3rd of 4).

Min

Returns the minimum LProp.

MinMax

The undecided minimum maximum.

MinMin

The decided minimum (1st of 4).

Mixi

The decided minimum of undecided middle (2nd of 4).

Normalise

Normalise 4 LProps (sorted ascending by propositional level).

PAndFst

Sends first argument of Logical AND to higher level.

PAndSnd

Sends second argument of Logical AND to higher level.

POrFst

Sends first argument of Logical OR to higher level.

POrSnd

Sends second argument of Logical OR to higher level.

PSem

Core axiom of Path Semantics.

PSemNaive

Naive axiom of Path Semantics (without order assumption).

PSemNaiveNorm

Normalised naive core axiom.

Ty

Models a type relation a : t.