{-# OPTIONS --safe --without-K #-}
open import Data.Product using (∃; _,_; -,_) renaming (_×_ to _∧_; proj₁ to fst; proj₂ to snd)

open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)

module Semantics.Presheaf.Evaluation.IS4
  (C                 : Set)

  (_⩽_               : (X Y : C) → Set)

  (⩽-trans           : ∀ {X X' X'' : C} (f : X ⩽ X') (g : X' ⩽ X'') → X ⩽ X'')
  (⩽-trans-assoc     : ∀ {X X' X'' X''' : C} (f : X ⩽ X') (g : X' ⩽ X'') (h : X'' ⩽ X''') → ⩽-trans f (⩽-trans g h) ≡ ⩽-trans (⩽-trans f g) h)

  (⩽-refl            : ∀ {X : C} → X ⩽ X)
  (⩽-refl-unit-left  : ∀ {X X' : C} (f : X ⩽ X') → ⩽-trans f ⩽-refl ≡ f)
  (⩽-refl-unit-right : ∀ {X X' : C} (f : X ⩽ X') → ⩽-trans ⩽-refl f ≡ f)

  (_R_               : (X Y : C) → Set)

  (R-trans           : ∀ {X Y Z : C} (r : X R Y) (r' : Y R Z) → X R Z)
  (R-trans-assoc     : ∀ {X Y Z Z' : C} (r : X R Y) (r' : Y R Z) (r'' : Z R Z') → R-trans r (R-trans r' r'') ≡ R-trans (R-trans r r') r'')

  (R-refl            : ∀ {X : C} → X R X)
  (R-refl-unit-left  : ∀ {X Y : C} (r : X R Y) → R-trans r R-refl ≡ r)
  (R-refl-unit-right : ∀ {X Y : C} (r : X R Y) → R-trans R-refl r ≡ r)

  (factor            : ∀ {X Y Y' : C} (r : X R Y) (w : Y ⩽ Y') → ∃ λ X' → X ⩽ X' ∧ X' R Y')
  (let lCtx          : ∀ {X Y Y' : C} (r : X R Y) (w : Y ⩽ Y') → C      ; lCtx     = λ r w → factor r w .fst)
  (let factorWk      : ∀ {X Y Y' : C} (r : X R Y) (w : Y ⩽ Y') → X ⩽ _  ; factorWk = λ r w → factor r w .snd .fst)
  (let factorR       : ∀ {X Y Y' : C} (r : X R Y) (w : Y ⩽ Y') → _ R Y' ; factorR  = λ r w → factor r w .snd .snd)
  (factor-pres-id    : ∀ {X Y : C} (r : X R Y) → factor r ⩽-refl ≡ (-, ⩽-refl , r))
  (factor-pres-∘     : ∀ {X Y Y' Y'' : C} (r : X R Y) (w : Y ⩽ Y') (w' : Y' ⩽ Y'') → factor r (⩽-trans w w') ≡ (-, ⩽-trans (factorWk r w) (factorWk (factorR r w) w') , factorR (factorR r w) w'))
  (factor-pres-refl  : ∀ {X X' : C} (w : X ⩽ X') → factor R-refl w ≡ (X' , w , R-refl))
  (factor-pres-trans : ∀ {X Y Z Z' : C} (r : X R Y) (r' : Y R Z) (w : Z ⩽ Z') → factor (R-trans r r') w ≡ (lCtx r (factorWk r' w) , factorWk r _ , R-trans (factorR r _) (factorR r' _)))
  where

import Semantics.Presheaf.Base C _⩽_ ⩽-refl ⩽-trans as PresheafBase
import Semantics.Presheaf.CartesianClosure C _⩽_ ⩽-trans ⩽-trans-assoc ⩽-refl ⩽-refl-unit-left ⩽-refl-unit-right as PresheafCartesianClosure
import Semantics.Presheaf.Necessity C _⩽_ ⩽-trans ⩽-trans-assoc ⩽-refl ⩽-refl-unit-left ⩽-refl-unit-right _R_ factor factor-pres-id factor-pres-∘ as PresheafNecessity

module PresheafNecessityIS4 = PresheafNecessity.IS4 R-trans R-trans-assoc R-refl R-refl-unit-left R-refl-unit-right factor-pres-refl factor-pres-trans

open PresheafBase             public
open PresheafCartesianClosure public
open PresheafNecessity        public
open PresheafNecessityIS4     public

import Semantics.Clouston.Evaluation.IS4.Base
    Psh _→̇_ _≈̇_ ≈̇-refl ≈̇-sym ≈̇-trans _∘_ id'[_]
    []' unit' _×'_ ⟨_,_⟩' π₁'[_] π₂'[_]
    _⇒'_ lam' app'
    ✦'_ ✦'-map_ μ'[_] η'[_]
    □'_ box' λ'
  as CloustonEvaluationIS4Base

open CloustonEvaluationIS4Base public using (module Eval)

module EvalProperties (N : Psh) where
  import Semantics.Clouston.Evaluation.IS4.Properties
      Psh _→̇_ _≈̇_ ≈̇-refl ≈̇-sym ≈̇-trans _∘_ ∘-pres-≈̇ ∘-assoc id'[_] id'-unit-left id'-unit-right
      []' unit' []'-eta _×'_ ⟨_,_⟩' ⟨,⟩'-pres-≈̇ π₁'[_] π₂'[_] ×'-beta-left ×'-beta-right ×'-eta ⟨,⟩'-nat
      _⇒'_ lam' lam'-pres-≈̇ app' app'-pres-≈̇ ⇒'-beta ⇒'-eta lam'-nat app'-nat
      ✦'_ ✦'-map_ ✦'-map-pres-≈̇ ✦'-map-pres-id' ✦'-map-pres-∘ μ'[_] μ'-nat μ'-assoc[_] η'[_] η'-nat η'-unit-left[_] η'-unit-right[_]
      □'_ □'-map_ box' box'-pres-≈̇ λ' λ'-pres-≈̇ □'-beta □'-eta box'-nat-dom λ'-nat-dom
      N
    as CloustonEvaluationIS4Properties

  open CloustonEvaluationIS4Properties public

Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.