Core.bracket

-- The bracket type [A] β‰œ A / ⊀ (Awodey–Bauer), as a π•Œ-CODE.
--
-- Nova has two truncations. βˆ₯Tβˆ₯ : Ξ© is the irrelevant one: Ξ© compares
-- its elements by inhabitation alone (code-prop-eq), so βˆ₯Tβˆ₯ has
-- the single canonical form ⋆ and a prop never exposes it β€” the witness
-- is unrecoverable, and elimination is confined to props and equations
-- (NovaFoundation.txt:1267, :1296).
--
-- Br a β‰œ a / (x y. βˆ₯πŸ™βˆ₯) is the other one. class x RETAINS x, so
-- el-quot-beta computes, and el-quot-e's motive ranges over arbitrary
-- TYPES: the eliminator lands wherever the method is constant. What it
-- gives up is Ξ©-membership β€” impredicativity, and iff-collapse.
--
-- It is nonetheless a DEFINITIONAL subsingleton: el-quot-eq concludes
-- ≐, not ≑. (Lean's Squash, the same quotient, is only a propositional
-- one β€” Quot.sound is not judgemental.)

import Core.prop (propExt)
import Core.equality (cong, sym, trans, pairext)
import Core.id (Id, refl, idToEq)
import Core.uip (uip, idCanon)

Br : π•Œ β†’ π•Œ
Br = Ξ»a. a / (x y. βˆ₯πŸ™βˆ₯)

br : {a : π•Œ} β†’ a β†’ Br a using (Br.unfold)
br = Ξ»a x. class x

-- Elimination into an ARBITRARY code, along any constant map.
brElim : {a b : π•Œ} (f : a β†’ b) (c : (x y : a) β†’ f x ≑ f y) (t : Br a) β†’ b using (Br.unfold)
brElim = Ξ»a b f c t. quot-elim (x. f x) t

-- ...and it COMPUTES.
brBeta : {a b : π•Œ} (f : a β†’ b) (c : (x y : a) β†’ f x ≑ f y) (x : a) β†’ brElim f c (br x) ≑ f x
  using (Br.unfold, br.eq, brElim.eq)
brBeta f c x = ⋆

-- ---------------------------------------------------------------
-- [A] is a proposition β€” JUDGEMENTALLY (el-quot-eq concludes ≐)
brIsProp : {a : π•Œ} (u v : Br a) β†’ u ≑ v using (Br.unfold)
brIsProp u v = quot-elim (y. quot-elim (x. ⋆) u) v

-- Consequently EVERY map out of [A] is constant on representatives,
-- with no hypothesis at all: the coherence brElim asks for is free
-- whenever the function already factors through the bracket.
brOutConst : {a b : π•Œ} (g : Br a β†’ b) (x y : a) β†’ g (br x) ≑ g (br y)
brOutConst = Ξ»a b g x y. cong (Ξ»w. b) g (brIsProp (br x) (br y))

-- Ξ· / uniqueness: brElim is the ONLY map agreeing with g on classes.
brEta : {a b : π•Œ} (g : Br a β†’ b) (t : Br a) β†’ brElim (Ξ»x. g (br x)) (brOutConst g) t ≑ g t
  using (Br.unfold, br.eq, brElim.eq, brOutConst.eq)
brEta = Ξ»a b g t. quot-elim (x. ⋆) t

-- ---------------------------------------------------------------
-- br is surjective β€” merely, but that is all a bracket can say
brSurj : {a : π•Œ} (t : Br a) β†’ βˆ₯(x : a) Γ— br x ≑ tβˆ₯ using (Br.unfold, br.eq)
brSurj = Ξ»a t. quot-elim (x. ⋆ (x, ⋆)) t

-- ---------------------------------------------------------------
-- [A] and A have the same Ξ©-squash: the bracket is a REFINEMENT of
-- βˆ₯Β·βˆ₯, carrying strictly more (it keeps the witness) and asserting
-- exactly the same thing.
brToSquash : {a : π•Œ} β†’ Br a β†’ βˆ₯aβˆ₯ using (Br.unfold)
brToSquash = Ξ»a t. quot-elim (x. ⋆ x) t

brSquashEq : {a : π•Œ} β†’ βˆ₯Br aβˆ₯ ≑ βˆ₯aβˆ₯ using (Br.unfold, br.eq, brToSquash.eq)
brSquashEq = Ξ»a. propExt (Ξ»h. squash-elim h (t. brToSquash t)) (Ξ»h. squash-elim h (x. ⋆ (br x)))

-- ---------------------------------------------------------------
-- [-] is an idempotent monad on π•Œ: unit br, multiplication brJoin,
-- functorial action brMap.
brMap : {a b : π•Œ} (f : a β†’ b) (t : Br a) β†’ Br b using (Br.unfold, br.eq)
brMap = Ξ»a b f t. quot-elim (x. br (f x)) t

brMapBeta : (a b : π•Œ) (f : a β†’ b) (x : a) β†’ brMap f (br x) ≑ br (f x)
  using (Br.unfold, br.eq, brMap.eq)
brMapBeta = Ξ»a b f x. ⋆

-- the coherence brElim demands IS brIsProp, verbatim
brJoin : {a : π•Œ} (s : Br (Br a)) β†’ Br a
brJoin s = brElim (Ξ»t. t) brIsProp s

-- idempotence, both round trips
brJoinUnit : {a : π•Œ} (t : Br a) β†’ brJoin (br t) ≑ t using (Br.unfold, br.eq, brJoin.eq, brElim.eq)
brJoinUnit t = ⋆

brUnitJoin : {a : π•Œ} (s : Br (Br a)) β†’ br (brJoin s) ≑ s
brUnitJoin s = brIsProp _ _

-- ---------------------------------------------------------------
-- The bracket REFLECTS emptiness β€” by ordinary elimination.
--
-- Compare Core.prop.absurdP: a βŠ₯-proof β†’ 𝟘 is NOT available that way
-- (el-squash-e-prf reaches only further propositions); Core.prop.absurd
-- has to detour through el-reflect on a false equation. Here quot-elim
-- lands in 𝟘 directly, because the scrutinee still holds its witness.
zeroConst : {b : π•Œ} (f : 𝟘 β†’ b) (x y : 𝟘) β†’ f x ≑ f y
zeroConst f x y = 𝟘-elim x

brEmpty : Br 𝟘 β†’ 𝟘 using (Br.unfold, zeroConst.eq)
brEmpty t = quot-elim (x. 𝟘-elim x) t

-- ---------------------------------------------------------------
-- DESCRIPTION. On a subsingleton the bracket is the type itself: the
-- witness comes back out, as data, and it computes.
--
-- This is exactly what βˆ₯Β·βˆ₯ : Ξ© must not have β€” unique choice is one of
-- the three prohibitions licensing Ξ©'s impredicativity
-- (NovaFoundation.txt:1316, Chicli–Pottier–Simpson). The bracket may
-- have it precisely because it is NOT a proposition of Ξ©: nothing
-- coerces into (Br a) from an iff-equal prop, so the only way to
-- hold one is to have built it from an element.
brDescr : {a : π•Œ} (s : (x y : a) β†’ x ≑ y) (t : Br a) β†’ a using (Br.unfold)
brDescr s t = quot-elim (x. x) t

brDescrBeta : {a : π•Œ} (s : (x y : a) β†’ x ≑ y) (x : a) β†’ brDescr s (br x) ≑ x
  using (Br.unfold, br.eq, brDescr.eq)
brDescrBeta = Ξ»a s x. ⋆

brDescrEta' : {a : π•Œ} (s : (x y : a) β†’ x ≑ y) (t : Br a) β†’ br (brDescr s t) ≑ t
brDescrEta' s t = brIsProp _ _

-- ---------------------------------------------------------------
-- The payoff, in miniature: a truncated existential whose witness is
-- recovered AS DATA and evaluates.
--
-- ≑ is Ξ©-valued and has no π•Œ-code, so the subsingleton is built from
-- the Id QIIT instead: Fib n β‰œ (m : β„•) Γ— Id β„• m n, an "βˆƒm. m = n"
-- that IS a code. uip makes it a subsingleton, brDescr opens it.
-- Its Ξ© twin, βˆ₯(Fib n)βˆ₯, says exactly the same thing
-- (brSquashEq) and yields nothing.
Fib : β„• β†’ π•Œ
Fib n = (m : β„•) Γ— Id _ m n

-- every element of Fib n is (n , refl): reflect the index equation
-- first, then uip finishes at the reflected type
fibCanon : {n : β„•} (u : Fib n) β†’ u ≑ (n, refl β„• n)
  using (Fib.unfold, hyp.rw, sigma.eta, Core.id.Id.unfold, Core.id.Id.eq)
fibCanon =
  Ξ»n u. let h = idToEq _ _ _ (u .Ο€β‚‚)
            pairext {β„•} {Ξ»m. Id _ m n} {_} {n, refl β„• n} h (idCanon (u .Ο€β‚‚) h)

fibIsProp : (n : β„•) (u v : Fib n) β†’ u ≑ v using (Fib.unfold, Core.id.Id.unfold, Core.id.Id.eq)
fibIsProp = Ξ»n u v. trans _ _ _ (fibCanon u) (sym _ _ (fibCanon v))

fibWitness : (n : β„•) (t : Br (Fib n)) β†’ β„• using (Fib.unfold)
fibWitness = Ξ»n t. brDescr (fibIsProp n) t .π₁

-- ⋆ means: this equation holds DEFINITIONALLY. The witness survived
-- the truncation and the projection reduced to a numeral.
fibWitnessComputes : fibWitness 2 (br (2, refl β„• 2)) ≑ 2
  using (Fib.unfold, br.eq, brDescr.eq, fibWitness.eq, Core.id.Id.eq)
fibWitnessComputes = ⋆

-- ---------------------------------------------------------------
-- [-] preserves binary products: (Br (a Γ— b)) β‰… (Br a Γ— Br b).
--
-- All the work is in building the two maps; both round trips are FREE,
-- because every equation between elements of a bracket is (brIsProp).
-- That is the shape of every proof about this modality: propositions
-- are cheap, elimination is the content.
brProdIsProp : {a b : π•Œ} (u v : Br a Γ— Br b) β†’ u ≑ v using (sigma.eta)
brProdIsProp = Ξ»a b u v. pairext (brIsProp (u .π₁) (v .π₁)) (brIsProp (u .Ο€β‚‚) (v .Ο€β‚‚))

brPairIn : {a b : π•Œ} (t : Br (a Γ— b)) β†’ Br a Γ— Br b
brPairIn =
  Ξ»a b t. brElim
    Ξ»p. br (p .π₁), br (p .Ο€β‚‚)
    Ξ»p q. brProdIsProp (br (p .π₁), br (p .Ο€β‚‚)) (br (q .π₁), br (q .Ο€β‚‚))
    t

brPairOutAt : {a b : π•Œ} (x : a) (v : Br b) β†’ Br (a Γ— b)
brPairOutAt = Ξ»a b x v. brElim (Ξ»y. br (x, y)) (Ξ»y y'. brIsProp (br (x, y)) (br (x, y'))) v

brPairOut : {a b : π•Œ} (p : Br a Γ— Br b) β†’ Br (a Γ— b)
brPairOut =
  Ξ»a b p. brElim
    Ξ»x. brPairOutAt x (p .Ο€β‚‚)
    Ξ»x x'. brIsProp (brPairOutAt x (p .Ο€β‚‚)) (brPairOutAt x' (p .Ο€β‚‚))
    p .π₁

brProdIso1 : {a b : π•Œ} (t : Br (a Γ— b)) β†’ brPairOut (brPairIn t) ≑ t
brProdIso1 = Ξ»a b t. brIsProp _ _

brProdIso2 : {a b : π•Œ} (p : Br a Γ— Br b) β†’ brPairIn (brPairOut p) ≑ p
brProdIso2 = Ξ»a b p. brProdIsProp _ _