Agda with the graphical interface Alfa is an interactive system for direct manipulation of proofs and programs. It is implementing Structured Type Theory which is a dependently typed functional language with modern language constructs such as pattern matching, parametrised modules and records.