日々の流転

λ. An Implementation of a setoid model in Agda

Extensional Equality in Intensional Type Theory の setoid model を、LEGOでの実装を元にAgdaで実装中。大体実装できた。

(2005-09-30 追記) だいぶ苦戦してしまったが、基本的な部分を何とか書けた。色々汚いので、きれいに書き直したいな。それと、LEGOでの実装と比較しなくては。

Meta.agda

Approximative Implementation of the meta theory.

Setoid.agda

Definition of the core model.

Compr.agda

Definition of context comprehension.

Pi.agda

Definition of ∏-types.

Prod.agda

Definition of (non-dependent) product types.

Id.agda

Definition of Identity types.

λ. 旅行