Jules' dependent prism

DepPrism.agda

module DepPrism where

open import Prelude

open import Data.Empty
open import Data.Sum

private variable
  ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
  X : 𝒰 ℓ₁
  Y : 𝒰 ℓ₂
  A : X → 𝒰 ℓ₃
  B : Y → 𝒰 ℓ₄

lim : {B : Y → 𝒰 ℓ₄} {x : X} → A x ⊎ Y → 𝒰 ℓ₄
lim {ℓ₄} (inl _) = Lift ℓ₄ ⊥
lim {B}  (inr y) = B y 

record DPrism (X : 𝒰 ℓ₁) (Y : 𝒰 ℓ₂) (A : X → 𝒰 ℓ₃) (B : Y → 𝒰 ℓ₄) : 𝒰 (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
  constructor dpr
  field
   fw : (x : X) → A x ⊎ Y
   bw : (x : X) → lim {A = A} {B = B} (fw x) → A x

open DPrism

bweq : (d : DPrism X Y A B)
     → (x : X) → (y : Y) → d .fw x ＝ inr y → B y → A x
bweq {B} d x y e by with d .fw x | recall (d .fw) x
... | inl _ | ⟪ _ ⟫  = absurd (⊎-disjoint e)
... | inr _ | ⟪ eq ⟫ = d .bw x (subst lim (eq ⁻¹) (subst B (inr-inj e ⁻¹) by))

eqbw : (fw : (x : X) → A x ⊎ Y)
     → ((x : X) → (y : Y) → fw x ＝ inr y → B y → A x)
     → DPrism X Y A B
eqbw {X} {A} {B} fw bw = dpr fw go
  where
  go : (x : X) → lim {A = A} {B = B} (fw x) → A x
  go x with fw x | recall fw x
  go x | inl _ | ⟪ eq ⟫ = λ ()
  go x | inr y | ⟪ eq ⟫ = bw x y eq

DepPrism0.agda

module DepPrism0 where

open import Prelude

open import Data.Empty
open import Data.Sum

private variable
  ℓ₁ ℓ₂ ℓₛ ℓₜ : Level
  X : 𝒰 ℓ₁
  Y : 𝒰 ℓ₂
  S : X → 𝒰 ℓₛ
  T : Y → 𝒰 ℓₜ

lim : {T : Y → 𝒰 ℓₜ} {x : X} → S x ⊎ Y → 𝒰 ℓₜ
lim {ℓₜ} (inl _) = Lift ℓₜ ⊥
lim {T} (inr y) = T y 

record @0 DPrism (X : 𝒰 ℓ₁) (Y : 𝒰 ℓ₂) (S : X → 𝒰 ℓₛ) (T : Y → 𝒰 ℓₜ) : 𝒰 (ℓ₁ ⊔ ℓ₂ ⊔ ℓₛ ⊔ ℓₜ) where
  constructor dpr
  field
   fw : (x : X) → S x ⊎ Y
   bw : (@0 x : X) → lim {S = S} {T = T} (fw x) → S x

DepPrismEq.agda

module DepPrismEq where

open import Prelude

open import Data.Empty
open import Data.Sum

private variable
  ℓ₁ ℓ₂ ℓₛ ℓₜ : Level

record DPrism (X : 𝒰 ℓ₁) (Y : 𝒰 ℓ₂) (S : @0 X → 𝒰 ℓₛ) (T : @0 Y → 𝒰 ℓₜ) : 𝒰 (ℓ₁ ⊔ ℓ₂ ⊔ ℓₛ ⊔ ℓₜ) where
  constructor dpr
  field
   fw : (x : X) → S x ⊎ Y
   bw : (@0 x : X) → (@0 y : Y) → (@0 _ : fw x ＝ inr y) → T y → S x

DepPrismErased.agda

module DepPrism where

open import Prelude

open import Data.Empty
open import Data.Sum

private variable
  ℓ₁ ℓ₂ ℓₛ ℓₜ : Level
  X : 𝒰 ℓ₁
  Y : 𝒰 ℓ₂
  S : X → 𝒰 ℓₛ
  T : Y → 𝒰 ℓₜ

lim : {T : Y → 𝒰 ℓₜ} {@0 x : X} → S x ⊎ Y → 𝒰 ℓₜ
lim {ℓₜ} (inl _) = Lift ℓₜ ⊥
lim {T} (inr y) = T y 

record DPrism (X : 𝒰 ℓ₁) (Y : 𝒰 ℓ₂) (S : X → 𝒰 ℓₛ) (T : Y → 𝒰 ℓₜ) : 𝒰 (ℓ₁ ⊔ ℓ₂ ⊔ ℓₛ ⊔ ℓₜ) where
  constructor dpr
  field
   fw : (x : X) → S x ⊎ Y
   bw : (@0 x : X) → Erased (lim {S = λ y → S (y .erased)} {T = T} (fw x) → S x)