{"size": 2337, "ext": "scrbl", "max_stars_repo_path": "cur-doc/cur/scribblings/stdlib/equality.scrbl", "max_stars_repo_name": "pwang347/cur", "max_stars_repo_stars_event_min_datetime": null, "max_stars_repo_stars_event_max_datetime": null, "max_issues_repo_path": "cur-doc/cur/scribblings/stdlib/equality.scrbl", "max_issues_repo_name": "pwang347/cur", "max_issues_repo_issues_event_min_datetime": null, "max_issues_repo_issues_event_max_datetime": null, "max_forks_repo_path": "cur-doc/cur/scribblings/stdlib/equality.scrbl", "max_forks_repo_name": "pwang347/cur", "max_forks_repo_forks_event_min_datetime": null, "max_forks_repo_forks_event_max_datetime": null}
{"max_stars_count": null, "max_issues_count": null, "max_forks_count": null, "avg_line_length": 36.515625, "max_line_length": 105, "alphanum_fraction": 0.539580659}
#lang scribble/manual

@(require
  "../defs.rkt"
  (for-label (only-meta-in 0 cur/stdlib/equality))
  (for-label (only-meta-in 0 cur/stdlib/nat))
  (for-label (except-in cur/stdlib/sugar :))
  scribble/eval)

@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/sugar cur/stdlib/equality)"))

@title{Equality}
@defmodule[cur/stdlib/equality]
This library defines the Paulin-Mohring and Martin-Löf equality types.

@deftogether[(@defthing[#:kind "2 parameter type" == (-> (A : Type) (x : A) (y : A) Type)]
              @defthing[#:kind "constructor" refl (-> (A : Type) (x : A) (== A x x))]
              @defproc[(sym [A Type] [n A] [m A] [n=m (PM-= A n m)]) (== A m n)]
              @defproc[(trans [A Type] [a A] [b A] [c A] [H1 (PM-= A a b)] [H2 (PM-= A b c)]) (== A a c)]
              )]{
Equivalent to @racket[PM-=], @racket[PM-refl], @racket[PM-sym], and @racket[PM-trans], respectively.
}

@deftogether[(@defthing[#:kind "2 parameter type" PM-= (-> (A : Type) (x : A) (y : A) Type)]
              @defthing[#:kind "constructor" PM-refl (-> (A : Type) (x : A) (PM-= A x x))])]{
The Paulin-Mohring equality type (PM equality).

Also provided as @racket[==] and @racket[refl], as this
should be considered the default equality.

@examples[#:eval curnel-eval
          (:: (PM-refl Nat z) (PM-= Nat z z))
          (new-elim (PM-refl Nat z)
                    (lambda (x : Nat) (t : (PM-= Nat z x))
                      (PM-= Nat z z))
                    (PM-refl Nat z))
]
}

@defproc[(PM-sym [A Type] [n A] [m A] [n=m (PM-= A n m)]) (PM-= A m n)]{
A proof of symmetry for PM equality.

Also provided as @racket[sym].
}

@defproc[(PM-trans [A Type] [a A] [b A] [c A] [H1 (PM-= A a b)] [H2 (PM-= A b c)]) (PM-= A a c)]{
A proof of transitivity for PM equality.

Also provided as @racket[trans].
}

@deftogether[(@defthing[#:kind "1 parameter type" ML-= (-> (A : Type) (x : A) (y : A) Type)]
              @defthing[#:kind "constructor" ML-refl (-> (A : Type) (x : A) (PM-= A x x))])]{
The Martin-Löf equality type (ML equality).

@examples[#:eval curnel-eval
          (:: (ML-refl Nat z) (ML-= Nat z z))
          (new-elim (ML-refl Nat z)
                    (lambda (x : Nat) (y : Nat) (t : (ML-= Nat x y))
                      (ML-= Nat x y))
                    (lambda (x : Nat) (ML-refl Nat x)))
]
}
