Brendan Hart 2019-2020

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc

module DomainTheory.Basics.FunctionComposition
        (pt : propositional-truncations-exist)
        (fe : βˆ€ {𝓀 π“₯} β†’ funext 𝓀 π“₯)
        (π“₯ : Universe)
       where

open import DomainTheory.Basics.Dcpo pt fe π“₯
open import DomainTheory.Basics.Miscelanea pt fe π“₯
open import DomainTheory.Basics.Pointed pt fe π“₯

open import OrderedTypes.Poset fe

open PosetAxioms

[_,_,_]_βˆ˜α΅ˆαΆœα΅–α΅’_ : (𝓓 : DCPO {𝓀} {𝓀'})
                 (𝓔 : DCPO {𝓣} {𝓣'})
                 (𝓕 : DCPO {𝓦} {𝓦'})
               β†’ DCPO[ 𝓔 , 𝓕 ]
               β†’ DCPO[ 𝓓 , 𝓔 ]
               β†’ DCPO[ 𝓓 , 𝓕 ]
[ 𝓓 , 𝓔 , 𝓕 ] g βˆ˜α΅ˆαΆœα΅–α΅’ f = h , c
 where
  h : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓕 ⟩
  h = pr₁ g ∘ pr₁ f

  h-is-monotone : is-monotone 𝓓 𝓕 h
  h-is-monotone x y p = Ξ³
   where
    Ξ΄ : pr₁ f x βŠ‘βŸ¨ 𝓔 ⟩ pr₁ f y
    Ξ΄ = monotone-if-continuous 𝓓 𝓔 f x y p

    Ξ³ : h x βŠ‘βŸ¨ 𝓕 ⟩ h y
    Ξ³ = monotone-if-continuous 𝓔 𝓕 g (pr₁ f x) (pr₁ f y) Ξ΄

  c : is-continuous 𝓓 𝓕 h
  c I Ξ± Ξ΄ = u , v
    where
     u : is-upperbound (underlying-order 𝓕) (h (∐ 𝓓 Ξ΄)) (Ξ» i β†’ h (Ξ± i))
     u i = h-is-monotone (Ξ± i) (∐ 𝓓 Ξ΄) (∐-is-upperbound 𝓓 Ξ΄ i)

     v : (z : ⟨ 𝓕 ⟩) β†’
         ((i : I) β†’ h (Ξ± i) βŠ‘βŸ¨ 𝓕 ⟩ z) β†’
         h (∐ 𝓓 Ξ΄) βŠ‘βŸ¨ 𝓕 ⟩ z
     v z p = transport (Ξ» - β†’ - βŠ‘βŸ¨ 𝓕 ⟩ z) (e ⁻¹) q
       where
        isdir₁ : is-Directed 𝓔 (Ξ» i β†’ pr₁ f (Ξ± i))
        isdir₁ = image-is-directed 𝓓 𝓔 (monotone-if-continuous 𝓓 𝓔 f) Ξ΄

        isdirβ‚‚ : is-Directed 𝓕 (Ξ» i β†’ (pr₁ g ∘ pr₁ f) (Ξ± i))
        isdirβ‚‚ = image-is-directed 𝓔 𝓕 (monotone-if-continuous 𝓔 𝓕 g) isdir₁

        e : h (∐ 𝓓 Ξ΄) ＝ ∐ 𝓕 isdirβ‚‚
        e = h (∐ 𝓓 Ξ΄)          ＝⟨ ap (Ξ» - β†’ pr₁ g -) (continuous-∐-＝ 𝓓 𝓔 f Ξ΄) ⟩
            pr₁ g (∐ 𝓔 isdir₁) ＝⟨ continuous-∐-＝ 𝓔 𝓕 g isdir₁ ⟩
            ∐ 𝓕 isdirβ‚‚         ∎

        q : ∐ 𝓕 isdirβ‚‚ βŠ‘βŸ¨ 𝓕 ⟩ z
        q = ∐-is-lowerbound-of-upperbounds 𝓕 isdirβ‚‚ z p

[_,_,_]_βˆ˜α΅ˆαΆœα΅–α΅’βŠ₯_ : (𝓓 : DCPOβŠ₯ {𝓀} {𝓀'})
                  (𝓔 : DCPOβŠ₯ {𝓣} {𝓣'})
                  (𝓕 : DCPOβŠ₯ {𝓦} {𝓦'})
                β†’ DCPOβŠ₯[ 𝓔 , 𝓕 ]
                β†’ DCPOβŠ₯[ 𝓓 , 𝓔 ]
                β†’ DCPOβŠ₯[ 𝓓 , 𝓕 ]
[ 𝓓 , 𝓔 , 𝓕 ] g βˆ˜α΅ˆαΆœα΅–α΅’βŠ₯ f = [ (𝓓 ⁻) , (𝓔 ⁻) , (𝓕 ⁻) ] g βˆ˜α΅ˆαΆœα΅–α΅’ f

\end{code}