open import Level open import Function open import Data.Unit open import Data.Product open import Data.Nat open import Data.Fin hiding (lift) open import Chapter2.Logic open import Chapter5.IDesc open import Chapter8.Ornament module Chapter8.Ornament.CartesianMorphism {ℓ k : Level} {I J K L : Set k} {D : func ℓ K L} {u : I → K}{v : J → L} (o : orn D u v) where forgetOrnNat : ∀{X : K → Set ℓ}{D} → (O : Orn u D) → ⟦ ⟦ O ⟧Orn ⟧ (X ∘ u) → ⟦ D ⟧ X forgetOrnNat (insert S D⁺) (s , xs) = forgetOrnNat (D⁺ s) xs forgetOrnNat (`var (inv i)) xs = xs forgetOrnNat `1 (lift tt) = lift tt forgetOrnNat (O₁ `× O₂) (t₁ , t₂) = forgetOrnNat O₁ t₁ , forgetOrnNat O₂ t₂ forgetOrnNat (`σ T⁺) (k , xs) = k , forgetOrnNat (T⁺ k) xs forgetOrnNat (`Σ T⁺) (s , xs) = s , forgetOrnNat (T⁺ s) xs forgetOrnNat (`Π T⁺) f = λ s → forgetOrnNat (T⁺ s) (f s) forgetOrnNat (deleteΣ s T⁺) xs = s , forgetOrnNat T⁺ xs forgetOrnNat (deleteσ k T⁺) xs = k , forgetOrnNat T⁺ xs forgetNat : {X : K → Set ℓ} → {j : J} → ⟦ ⟦ o ⟧orn ⟧func (X ∘ u) j → ⟦ D ⟧func X (v j) forgetNat {X} {j} = forgetOrnNat (orn.out o j)