prop 0.47.0

Propositional logic with types in Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135

//! # Homotopy Type Theory
//!
//! *Notice! This module is experimental and in early stages of development.*
//!
//! This is a model of Homotopy Type Theory that attempts to be similar to the version in
//! the [standard HoTT book](https://homotopytypetheory.org/book/).

use crate::*;
use fun::{App, Type};
use hooo::Pow;
use path_semantics::Ty;
use nat::{Nat, S, Z};

/// Whether some type is a homotopy proposition.
#[derive(Copy, Clone)]
pub struct IsHType<N: Nat, A: Prop>(N, A);

/// Identity type.
#[derive(Copy, Clone)]
pub struct Id<T: Prop, PathP: Prop, PathQ: Prop>(T, PathP, PathQ);

/// Reflexivity proof of identity type.
#[derive(Copy, Clone)]
pub struct Refl<X: Prop, A: Prop>(X, A);

/// Whether some type is a homotopy proposition of level 0.
pub type IsContr<A> = IsHType<Z, A>;
/// Whether some type is a homotopy proposition of level 1.
pub type IsProp<A> = IsHType<S<Z>, A>;
/// Whether some type is a homotopy proposition of level 2.
pub type IsSet<A> = IsHType<S<S<Z>>, A>;
/// Whether some type is a homotopy n-groupoid.
pub type IsNGroupoid<N, A> = IsHType<S<S<N>>, A>;
/// Whether some type is a groupoid.
pub type IsGroupoid<A> = IsNGroupoid<S<Z>, A>;

/// `(x : type(n)) ⋀ (a : x) ⋀ (b : x)  =>  id{x}(a, b) : type(n)`.
pub fn id_ty<X: Prop, A: Prop, B: Prop, N: Nat>(
    _ty_x: Ty<X, Type<N>>,
    _ty_a: Ty<A, X>,
    _ty_b: Ty<B, X>
) -> Ty<Id<X, A, B>, Type<N>> {unimplemented!()}
/// `(a : x)  =>  refl{x}(a) : id{x}(a, a)`.
pub fn refl<A: Prop, X: Prop, PathP: Prop>(_ty_a: Ty<A, X>) -> Ty<Refl<X, A>, Id<X, A, A>>{
    unimplemented!()
}
/// `id{x}(a, b) => (a == b)`.
pub fn id_to_eq<A: Prop, B: Prop, X: Prop>(_: Id<X, A, B>) -> Eq<A, B> {unimplemented!()}
/// `(id{x}(a, b) ⋀ id{x}(a, c)) => id{x}(c, b)`.
pub fn id_in_left_arg<A: Prop, B: Prop, C: Prop, X: Prop>(
    p: Id<X, A, B>,
    q: Id<X, A, C>
) -> Id<X, C, B> {Id(p.0, q.2, p.2)}
/// `(id{x}(a, b) ⋀ id{x}(b, c)) => id{x}(a, b)`.
pub fn id_in_right_arg<A: Prop, B: Prop, C: Prop, X: Prop>(
    p: Id<X, A, B>,
    q: Id<X, B, C>
) -> Id<X, A, C> {Id(p.0, p.1, q.2)}
/// `(f : x -> y) ⋀ id{x}(a, b) => id{y}(f(a), f(b))`.
pub fn ap_fun<F: Prop, X: Prop, Y: Prop, A: Prop, B: Prop>(
    _f: Ty<F, Pow<Y, X>>,
    _p: Id<X, A, B>,
) -> Id<Y, App<F, A>, App<F, B>> {unimplemented!()}
/// `(f : x => y) ⋀ id{x}(a, b) => id{y}(f(a), f(b))`.
pub fn ap_lam<F: Prop, X: Prop, Y: Prop, A: Prop, B: Prop>(
    _f: Ty<F, Imply<X, Y>>,
    _p: Id<X, A, B>,
) -> Id<Y, App<F, A>, App<F, B>> {unimplemented!()}
/// `is_contr(a) => a`.
pub fn from_is_contr<A: Prop>(x: IsContr<A>) -> A {x.1}
/// `a => is_contr(a)`.
pub fn to_is_contr<A: Prop>(x: A) -> IsContr<A> {IsHType(Z, x)}
/// `(is_htype(n+1, x) ⋀ (a : x) ⋀ (b : x)) => is_htype(n, id{x}(a, b))`.
pub fn is_htype_to_id<A: Prop, B: Prop, X: Prop, N: Nat>(
    _: IsHType<S<N>, X>,
    _: Ty<A, X>,
    _: Ty<B, X>
) -> IsHType<N, Id<X, A, B>> {unimplemented!()}
/// `(is_prop(x) ⋀ (a : x) ⋀ (b : x)) => id{x}(a, b)`.
pub fn is_prop_to_id<A: Prop, B: Prop, X: Prop>(
    is_prop: IsProp<X>,
    ty_a: Ty<A, X>,
    ty_b: Ty<B, X>
) -> Id<X, A, B> {
    from_is_contr(is_htype_to_id(is_prop, ty_a, ty_b))
}
/// `(is_set(x) ⋀ (a : x) ⋀ (b : x)) => is_prop(id{x}(a, b))`.
pub fn is_set_to_is_prop<A: Prop, B: Prop, X: Prop>(
    is_set: IsSet<X>,
    ty_a: Ty<A, X>,
    ty_b: Ty<B, X>
) -> IsProp<Id<X, A, B>> {
    is_htype_to_id(is_set, ty_a, ty_b)
}
/// `(is_groupoid(x) ⋀ (a : x) ⋀ (b : x)) => is_set(id{x}(a, b))`.
pub fn is_groupoid_to_is_set<A: Prop, B: Prop, X: Prop>(
    is_groupoid: IsGroupoid<X>,
    ty_a: Ty<A, X>,
    ty_b: Ty<B, X>
) -> IsSet<Id<X, A, B>> {
    is_htype_to_id(is_groupoid, ty_a, ty_b)
}
/// `(is_set(x) ⋀ (a : x) ⋀ (b : x) ⋀ (p : id{x}(a, b)) ⋀ (q : id{x}(a, b))) =>
/// id{id{x}(a, b)}(p, q)`.
pub fn is_set_to_id<A: Prop, B: Prop, X: Prop, PathP: Prop, PathQ: Prop>(
    is_set: IsSet<X>,
    ty_a: Ty<A, X>,
    ty_b: Ty<B, X>,
    path_p: Ty<PathP, Id<X, A, B>>,
    path_q: Ty<PathQ, Id<X, A, B>>
) -> Id<Id<X, A, B>, PathP, PathQ> {
    let is_prop_eq: IsProp<Id<X, A, B>> = is_set_to_is_prop(is_set, ty_a, ty_b);
    is_prop_to_id(is_prop_eq, path_p, path_q)
}
/// `(is_groupoid(x) ⋀ (a : x) ⋀ (b : x) ⋀ (p : id{x}(a, b)) ⋀
/// (q : id{x}(a, b)) ⋀ (hp : id{id{x}(a, b)}(p, q)) ⋀ (hq : id{id{x}(a, b)}(p, a))) =>
/// id{id{id{x}(a, b)}(p, q)}(hp, hq)`.
pub fn is_groupoid_to_id<
    A: Prop, B: Prop, X: Prop,
    PathP: Prop, PathQ: Prop, HomP: Prop, HomQ: Prop,
>(
    is_groupoid: IsGroupoid<X>,
    ty_a: Ty<A, X>,
    ty_b: Ty<B, X>,
    path_p: Ty<PathP, Id<X, A, B>>,
    path_q: Ty<PathQ, Id<X, A, B>>,
    hom_p: Ty<HomP, Id<Id<X, A, B>, PathP, PathQ>>,
    hom_q: Ty<HomQ, Id<Id<X, A, B>, PathP, PathQ>>
) -> Id<Id<Id<X, A, B>, PathP, PathQ>, HomP, HomQ> {
    let is_set_eq = is_groupoid_to_is_set(is_groupoid, ty_a, ty_b);
    let is_prop_eq = is_set_to_is_prop(is_set_eq, path_p, path_q);
    is_prop_to_id(is_prop_eq, hom_p, hom_q)
}
/// `is_contr(true)`.
pub fn true_is_contr() -> IsContr<True> {to_is_contr(True)}