Library Coq.Init.Logic_Type

This module defines type constructors for types in Type (Datatypes.v and Logic.v defined them for types in Set)

Set Implicit Arguments.

Require Import Ltac.
Require Import Datatypes.
Require Export Logic.

Negation of a type in Type

Definition notT (A:Type) := A -> False.

Properties of identity

Section identity_is_a_congruence.

Variables A B : Type.
Variable f : A -> B.

Variables x y z : A.

Lemma identity_sym : identity x y -> identity y x.

Lemma identity_trans : identity x y -> identity y z -> identity x z.

Lemma identity_congr : identity x y -> identity (f x) (f y).

Lemma not_identity_sym : notT (identity x y) -> notT (identity y x).

End identity_is_a_congruence.

Definition identity_ind_r :
  forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y.
Defined.

Definition identity_rec_r :
  forall (A:Type) (a:A) (P:A -> Set), P a -> forall y:A, identity y a -> P y.
Defined.

Definition identity_rect_r :
  forall (A:Type) (a:A) (P:A -> Type), P a -> forall y:A, identity y a -> P y.
Defined.

#[global]
Hint Immediate identity_sym not_identity_sym: core.

Notation refl_id := identity_refl (only parsing).
Notation sym_id := identity_sym (only parsing).
Notation trans_id := identity_trans (only parsing).
Notation sym_not_id := not_identity_sym (only parsing).