Sandro Stucki sstucki
TOTBWF
/ Fixpoint.agda
Last active
June 10, 2021 14:36
Agda proof of the Knaster-Tarski Fixpoint Theorem
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- A proof of the Knaster-Tarski Fixpoint Theorem | |
| -- See https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem | |
| module Fixpoint where | |
| open import Level | |
| open import Data.Product | |
| open import Relation.Binary | |
| open import Relation.Binary.Morphism |