{-
  Agda formalisation of the results of:
  
  i. “A Topological Counterpart of Well-founded Trees
  in Dependent Type Theory”

  ii. “A Topological Reading of Coinductive Predicates
  in Dependent Type Theory”
-}

module everything where

import Endofunctors

import Inductive.Constructors.Ind-types
import Inductive.Constructors.DW-types
import Inductive.Constructors.▹-types
import Inductive.Constructors.W-types

import Inductive.Equivalences.Impredicative-Ind-types
import Inductive.Equivalences.Ind-as-fixedpoint
import Inductive.Equivalences.▹-as-fixedpoint
import Inductive.Equivalences.▹-give-Ind
import Inductive.Equivalences.Ind-give-▹
import Inductive.Equivalences.Ind-give-W
import Inductive.Equivalences.DW-give-Ind
import Inductive.Equivalences.W-give-DW

import Coinductive.Constructors.Coind-types
import Coinductive.Constructors.⋊-types

import Coinductive.Equivalences.Impredicative-Coind-types
import Coinductive.Equivalences.Coind-gives-⋊
import Coinductive.Equivalences.⋊-gives-Coind
import Coinductive.Equivalences.DM-gives-Coind