Cheshire Cat y-taka-23

y-taka-23 / coq_topology.v

Created January 6, 2013 12:24

A Proof of the Elementary Property of Connected Spaces

y-taka-23 / coq_filter.v

Last active May 21, 2018 03:26

Validation of the filter Function (via "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/Logic.html)

	(******************************************************)
	(** //// Validation of the "filter" Function //// *)
	(******************************************************)

	Require Import List Bool Lt.

	Section Filter.


	(////////////////////////////////////////////////////)

y-taka-23 / coq_mlattice.v

Created December 22, 2012 17:10

An Example of Modular Lattices (The Lattice of Normal Subgroups of a Group)

	(******************************************************)
	(** //// Modular Lattices //// *)
	(******************************************************)

	Section ModularLattice.

	Require Import Relation_Definitions Setoid Morphisms.


	(////////////////////////////////////////////////////)

y-taka-23 / coq_kleisli.v

Last active December 10, 2015 01:28

Kleisli Construction of Monads (Equivalency of Category Theory Style and Haskell Style)

	(******************************************************)
	(** //// Kliesli Construction of Monads //// *)
	(******************************************************)

	Require Import Logic.FunctionalExtensionality.


	(////////////////////////////////////////////////////)
	(** Preliminaries *)
	(////////////////////////////////////////////////////)