Library lam_models


Require Import List.

Require Import basics.
Require Import categories.
Require Import preord.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import effective.
Require Import plotkin.
Require Import profinite.
Require Import embed.
Require Import joinable.
Require Import directed.
Require Import cont_functors.
Require Import bilimit.
Require Import exp_functor.
Require Import profinite_adj.
Require Import cont_adj.

Notation Ue := liftEMBED.
Notation Le := forgetEMBED.

Models of untyped λ-calculi