part:
- frontmatter: True
  title: "Front matter"
  chapter:
  - include: src/plfa/frontmatter/Dedication.md
    epub-type: dedication
  - include: src/plfa/frontmatter/Preface.md
    epub-type: preface
  - include: README.md
    epub-type: foreword
- mainmatter: True
  title: "Part 1: Logical Foundations"
  chapter:
  - include: src/plfa/part1/Naturals.lagda.md
  - include: src/plfa/part1/Induction.lagda.md
  - include: src/plfa/part1/Relations.lagda.md
  - include: src/plfa/part1/Equality.lagda.md
  - include: src/plfa/part1/Isomorphism.lagda.md
  - include: src/plfa/part1/Connectives.lagda.md
  - include: src/plfa/part1/Negation.lagda.md
  - include: src/plfa/part1/Quantifiers.lagda.md
  - include: src/plfa/part1/Decidable.lagda.md
  - include: src/plfa/part1/Lists.lagda.md
- title: "Part 2: Programming Language Foundations"
  chapter:
  - include: src/plfa/part2/Lambda.lagda.md
  - include: src/plfa/part2/Properties.lagda.md
  - include: src/plfa/part2/DeBruijn.lagda.md
  - include: src/plfa/part2/More.lagda.md
  - include: src/plfa/part2/Bisimulation.lagda.md
  - include: src/plfa/part2/Inference.lagda.md
  - include: src/plfa/part2/Untyped.lagda.md
  - include: src/plfa/part2/Confluence.lagda.md
  - include: src/plfa/part2/BigStep.lagda.md
- title: "Part 3: Denotational Semantics"
  chapter:
  - include: src/plfa/part3/Denotational.lagda.md
  - include: src/plfa/part3/Compositional.lagda.md
  - include: src/plfa/part3/Soundness.lagda.md
  - include: src/plfa/part3/Adequacy.lagda.md
  - include: src/plfa/part3/ContextualEquivalence.lagda.md
- backmatter: True
  title: "Appendix"
  chapter:
  - include: src/plfa/part2/Substitution.lagda.md
    epub-type: appendix
- title: "Back matter"
  chapter:
  - include: src/plfa/backmatter/Acknowledgements.md
    epub-type: acknowledgements
  - include: src/plfa/backmatter/Fonts.lagda.md
    epub-type: appendix