open import 1Lab.HLevel.Retracts
open import 1Lab.HLevel.Universe
open import 1Lab.Resizing
open import 1Lab.HLevel
open import 1Lab.Path
open import 1Lab.Type
module 1Lab.Underlying where
record Underlying {ℓ} (T : Type ℓ) : Typeω where
field
ℓ-underlying : Level
⌞_⌟ : T → Type ℓ-underlying
open Underlying ⦃ ... ⦄ using (⌞_⌟) public
open Underlying using (ℓ-underlying)
{-# DISPLAY Underlying.⌞_⌟ f x = ⌞ x ⌟ #-}
instance
Underlying-Type : ∀ {ℓ} → Underlying (Type ℓ)
Underlying-Type {ℓ} .ℓ-underlying = ℓ
Underlying-Type .⌞_⌟ x = x
Underlying-n-Type : ∀ {ℓ n} → Underlying (n-Type ℓ n)
Underlying-n-Type {ℓ} .ℓ-underlying = ℓ
Underlying-n-Type .⌞_⌟ x = ∣ x ∣
Underlying-prop : Underlying Ω
Underlying-prop .ℓ-underlying = lzero
Underlying-prop .⌞_⌟ x = ∣ x ∣
Underlying-Σ
: ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
→ ⦃ ua : Underlying A ⦄
→ Underlying (Σ A B)
Underlying-Σ ⦃ ua ⦄ .ℓ-underlying = ua .ℓ-underlying
Underlying-Σ .⌞_⌟ x = ⌞ x .fst ⌟
Underlying-Lift
: ∀ {ℓ ℓ'} {A : Type ℓ} ⦃ ua : Underlying A ⦄
→ Underlying (Lift ℓ' A)
Underlying-Lift ⦃ ua ⦄ .ℓ-underlying = ua .ℓ-underlying
Underlying-Lift .⌞_⌟ x = ⌞ x .Lift.lower ⌟
from-is-true
: ∀ {ℓ} {A : Type ℓ} ⦃ _ : Underlying A ⦄ {P Q : A} ⦃ _ : H-Level ⌞ Q ⌟ 0 ⦄
→ P ≡ Q
→ ⌞ P ⌟
from-is-true prf = subst ⌞_⌟ (sym prf) (hlevel 0 .centre)
_∈_ : ∀ {ℓ ℓ'} {A : Type ℓ} {P : Type ℓ'} ⦃ u : Underlying P ⦄
→ A → (A → P) → Type (u .ℓ-underlying)
x ∈ P = ⌞ P x ⌟
record
Funlike {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} (F : A → B → Type ℓ'') : Typeω where
infixl 999 _#_
field
overlap ⦃ au ⦄ : Underlying A
overlap ⦃ bu ⦄ : Underlying B
_#_ : ∀ {A B} → F A B → ⌞ A ⌟ → ⌞ B ⌟
open Funlike ⦃ ... ⦄ using (_#_) public
{-# DISPLAY Funlike._#_ p f x = f # x #-}
apply
: ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {F : A → B → Type ℓ''}
→ ⦃ _ : Funlike F ⦄
→ ∀ {a b} → F a b → ⌞ a ⌟ → ⌞ b ⌟
apply = _#_
ap#
: ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {F : A → B → Type ℓ''}
→ ⦃ _ : Funlike F ⦄
→ ∀ {a : A} {b : B} (f : F a b) → ∀ {x y : ⌞ a ⌟} → x ≡ y → f # x ≡ f # y
ap# f = ap (apply f)
_#ₚ_
: ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {F : A → B → Type ℓ''}
→ ⦃ _ : Funlike F ⦄
→ {a : A} {b : B} {f g : F a b} → f ≡ g → ∀ (x : ⌞ a ⌟) → f # x ≡ g # x
f #ₚ x = ap₂ _#_ f refl
instance
Funlike-Fun
: ∀ {ℓ ℓ'}
→ Funlike {lsuc ℓ} {lsuc ℓ'} {ℓ ⊔ ℓ'} {Type ℓ} {Type ℓ'} λ x y → x → y
Funlike-Fun = record
{ _#_ = _$_
}