{-# OPTIONS --rewriting #-}

module Main where

----------------------------------------------------------------------
-- Interval Type Theory
----------------------------------------------------------------------

-- Axioms for an interval as a total order with monus
open import Interval

-- Paths based on the interval
open import Path

-- Function extensionality with respect to the path-based identity types
open import FunExt

-- Fibrant families for this notion of path
open import Fibration

-- Closure of fibrant families under various type constructs
open import DisjointUnion -- disjoint union types
open import Sigma         -- dependent product types
open import Pi            -- dependent function types
open import WF            -- well-founded tree types
open import Id            -- propositional identity types

-- Path-contractible types
open import Contractible

open import Equivalence
--open import Univalence