text:
{-# OPTIONS --without-K --allow-unsolved-metas --exact-split #-}

module 21-pushouts where

import 20-pullbacks
open 20-pullbacks public

-- Section 14.1

{- We define the type of cocones with vertex X on a span. Since we will use it
   later on, we will also characterize the identity type of the type of cocones
   with a given vertex X. -}

cocone :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) → UU l4 → UU _
cocone {A = A} {B = B} f g X =
  Σ (A → X) (λ i → Σ (B → X) (λ j → (i ∘ f) ~ (j ∘ g)))

{- We characterize the identity type of the type of cocones with vertex C. -}

coherence-htpy-cocone :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c c' : cocone f g X) →
  (K : (pr1 c) ~ (pr1 c')) (L : (pr1 (pr2 c)) ~ (pr1 (pr2 c'))) → UU (l1 ⊔ l4)
coherence-htpy-cocone f g c c' K L =
  ((pr2 (pr2 c)) ∙h (L ·r g)) ~ ((K ·r f) ∙h (pr2 (pr2 c')))

htpy-cocone :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} →
  cocone f g X → cocone f g X → UU (l1 ⊔ (l2 ⊔ (l3 ⊔ l4)))
htpy-cocone f g c c' =
  Σ ((pr1 c) ~ (pr1 c'))
    ( λ K → Σ ((pr1 (pr2 c)) ~ (pr1 (pr2 c')))
      ( coherence-htpy-cocone f g c c' K))

reflexive-htpy-cocone :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  htpy-cocone f g c c
reflexive-htpy-cocone f g (pair i (pair j H)) =
  pair refl-htpy (pair refl-htpy htpy-right-unit)

htpy-cocone-eq :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c c' : cocone f g X) →
  Id c c' → htpy-cocone f g c c'
htpy-cocone-eq f g c .c refl = reflexive-htpy-cocone f g c

is-contr-total-htpy-cocone :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  is-contr (Σ (cocone f g X) (htpy-cocone f g c))
is-contr-total-htpy-cocone f g c =
  is-contr-total-Eq-structure
    ( λ i' jH' K → Σ ((pr1 (pr2 c)) ~ (pr1 jH'))
      ( coherence-htpy-cocone f g c (pair i' jH') K))
    ( is-contr-total-htpy (pr1 c))
    ( pair (pr1 c) refl-htpy)
    ( is-contr-total-Eq-structure
      ( λ j' H' → coherence-htpy-cocone f g c
        ( pair (pr1 c) (pair j' H'))
        ( refl-htpy))
      ( is-contr-total-htpy (pr1 (pr2 c)))
      ( pair (pr1 (pr2 c)) refl-htpy)
      ( is-contr-is-equiv'
        ( Σ (((pr1 c) ∘ f) ~ ((pr1 (pr2 c)) ∘ g)) (λ H' → (pr2 (pr2 c)) ~ H'))
        ( tot (λ H' M → htpy-right-unit ∙h M))
        ( is-equiv-tot-is-fiberwise-equiv (λ H' → is-equiv-htpy-concat _ _))
        ( is-contr-total-htpy (pr2 (pr2 c)))))

is-equiv-htpy-cocone-eq :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c c' : cocone f g X) →
  is-equiv (htpy-cocone-eq f g c c')
is-equiv-htpy-cocone-eq f g c =
  fundamental-theorem-id c
    ( reflexive-htpy-cocone f g c)
    ( is-contr-total-htpy-cocone f g c)
    ( htpy-cocone-eq f g c)

eq-htpy-cocone :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c c' : cocone f g X) →
  htpy-cocone f g c c' → Id c c'
eq-htpy-cocone f g c c' = inv-is-equiv (is-equiv-htpy-cocone-eq f g c c')

{- Given a cocone c on a span S with vertex X, and a type Y, the function
   cocone-map sends a function X → Y to a new cocone with vertex Y. -}

cocone-map :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} {Y : UU l5} →
  cocone f g X → (X → Y) → cocone f g Y
cocone-map f g (pair i (pair j H)) h =
  pair (h ∘ i) (pair (h ∘ j) (h ·l H))

cocone-map-id :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  Id (cocone-map f g c id) c
cocone-map-id f g (pair i (pair j H)) =
  eq-pair refl (eq-pair refl (eq-htpy (λ s → ap-id (H s))))

cocone-map-comp :
  {l1 l2 l3 l4 l5 l6 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X)
  {Y : UU l5} (h : X → Y) {Z : UU l6} (k : Y → Z) →
  Id (cocone-map f g c (k ∘ h)) (cocone-map f g (cocone-map f g c h) k)
cocone-map-comp f g (pair i (pair j H)) h k =
  eq-pair refl (eq-pair refl (eq-htpy (λ s → ap-comp k h (H s))))

{- A cocone c on a span S is said to satisfy the universal property of the
   pushout of S if the function cocone-map is an equivalence for every type Y.
   -}

universal-property-pushout :
  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} →
  cocone f g X → UU _
universal-property-pushout l f g c =
  (Y : UU l) → is-equiv (cocone-map f g {Y = Y} c)

map-universal-property-pushout :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  ( up-c : {l : Level} → universal-property-pushout l f g c)
  {Y : UU l5} → cocone f g Y → (X → Y)
map-universal-property-pushout f g c up-c {Y} = inv-is-equiv (up-c Y)

htpy-cocone-map-universal-property-pushout :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  ( f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  ( up-c : {l : Level} → universal-property-pushout l f g c)
  { Y : UU l5} (d : cocone f g Y) →
  htpy-cocone f g
    ( cocone-map f g c
      ( map-universal-property-pushout f g c up-c d))
    ( d)
htpy-cocone-map-universal-property-pushout f g c up-c {Y} d =
  htpy-cocone-eq f g
    ( cocone-map f g c (map-universal-property-pushout f g c up-c d))
    ( d)
    ( issec-inv-is-equiv (up-c Y) d)

uniqueness-map-universal-property-pushout :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  ( f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  ( up-c : {l : Level} → universal-property-pushout l f g c) →
  { Y : UU l5} (d : cocone f g Y) →
  is-contr ( Σ (X → Y) (λ h → htpy-cocone f g (cocone-map f g c h) d))
uniqueness-map-universal-property-pushout f g c up-c {Y} d =
  is-contr-is-equiv'
    ( fib (cocone-map f g c) d)
    ( tot (λ h → htpy-cocone-eq f g (cocone-map f g c h) d))
    ( is-equiv-tot-is-fiberwise-equiv
      ( λ h → is-equiv-htpy-cocone-eq f g (cocone-map f g c h) d))
    ( is-contr-map-is-equiv (up-c Y) d)

{- We derive a 3-for-2 property of pushouts, analogous to the 3-for-2 property
   of pullbacks. -}

triangle-cocone-cocone :
  { l1 l2 l3 l4 l5 l6 : Level}
  { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} {Y : UU l5}
  { f : S → A} {g : S → B} (c : cocone f g X) (d : cocone f g Y)
  ( h : X → Y) (KLM : htpy-cocone f g (cocone-map f g c h) d)
  ( Z : UU l6) →
  ( cocone-map f g d) ~ ((cocone-map f g c) ∘ (λ (k : Y → Z) → k ∘ h))
triangle-cocone-cocone {Y = Y} {f = f} {g = g} c d h KLM Z k =
  inv
    ( ( cocone-map-comp f g c h k) ∙
      ( ap
        ( λ t → cocone-map f g t k)
        ( eq-htpy-cocone f g (cocone-map f g c h) d KLM)))

is-equiv-up-pushout-up-pushout :
  { l1 l2 l3 l4 l5 : Level}
  { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} {Y : UU l5}
  ( f : S → A) (g : S → B) (c : cocone f g X) (d : cocone f g Y) →
  ( h : X → Y) (KLM : htpy-cocone f g (cocone-map f g c h) d) →
  ( up-c : {l : Level} → universal-property-pushout l f g c) →
  ( up-d : {l : Level} → universal-property-pushout l f g d) →
  is-equiv h
is-equiv-up-pushout-up-pushout f g c d h KLM up-c up-d =
  is-equiv-is-equiv-precomp h
    ( λ l Z →
      is-equiv-right-factor
        ( cocone-map f g d)
        ( cocone-map f g c)
        ( precomp h Z)
        ( triangle-cocone-cocone c d h KLM Z)
        ( up-c Z)
        ( up-d Z))

up-pushout-up-pushout-is-equiv :
  { l1 l2 l3 l4 l5 : Level}
  { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} {Y : UU l5}
  ( f : S → A) (g : S → B) (c : cocone f g X) (d : cocone f g Y) →
  ( h : X → Y) (KLM : htpy-cocone f g (cocone-map f g c h) d) →
  is-equiv h →
  ( up-c : {l : Level} → universal-property-pushout l f g c) →
  {l : Level} → universal-property-pushout l f g d
up-pushout-up-pushout-is-equiv f g c d h KLM is-equiv-h up-c Z =
  is-equiv-comp
    ( cocone-map f g d)
    ( cocone-map f g c)
    ( precomp h Z)
    ( triangle-cocone-cocone c d h KLM Z)
    ( is-equiv-precomp-is-equiv h is-equiv-h Z)
    ( up-c Z)

up-pushout-is-equiv-up-pushout :
  { l1 l2 l3 l4 l5 : Level}
  { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} {Y : UU l5}
  ( f : S → A) (g : S → B) (c : cocone f g X) (d : cocone f g Y) →
  ( h : X → Y) (KLM : htpy-cocone f g (cocone-map f g c h) d) →
  ( up-d : {l : Level} → universal-property-pushout l f g d) →
  is-equiv h →
  {l : Level} → universal-property-pushout l f g c
up-pushout-is-equiv-up-pushout f g c d h KLM up-d is-equiv-h Z =
  is-equiv-left-factor
    ( cocone-map f g d)
    ( cocone-map f g c)
    ( precomp h Z)
    ( triangle-cocone-cocone c d h KLM Z)
    ( up-d Z)
    ( is-equiv-precomp-is-equiv h is-equiv-h Z)

uniquely-unique-pushout :
  { l1 l2 l3 l4 l5 : Level}
  { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} {Y : UU l5}
  ( f : S → A) (g : S → B) (c : cocone f g X) (d : cocone f g Y) →
  ( up-c : {l : Level} → universal-property-pushout l f g c) →
  ( up-d : {l : Level} → universal-property-pushout l f g d) →
  is-contr
    ( Σ (X ≃ Y) (λ e → htpy-cocone f g (cocone-map f g c (map-equiv e)) d))
uniquely-unique-pushout f g c d up-c up-d =
  is-contr-total-Eq-substructure
    ( uniqueness-map-universal-property-pushout f g c up-c d)
    ( is-subtype-is-equiv)
    ( map-universal-property-pushout f g c up-c d)
    ( htpy-cocone-map-universal-property-pushout f g c up-c d)
    ( is-equiv-up-pushout-up-pushout f g c d
      ( map-universal-property-pushout f g c up-c d)
      ( htpy-cocone-map-universal-property-pushout f g c up-c d)
      ( up-c)
      ( up-d))

{- We will assume that every span has a pushout. Moreover, we will introduce
   some further terminology to facilitate working with these pushouts. -}

postulate pushout : {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) → UU (l1 ⊔ l2 ⊔ l3)

postulate inl-pushout : {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) → A → pushout f g

postulate inr-pushout : {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) → B → pushout f g

postulate glue-pushout : {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) → ((inl-pushout f g) ∘ f) ~ ((inr-pushout f g) ∘ g)

cocone-pushout :
  {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) → cocone f g (pushout f g)
cocone-pushout f g =
  pair
    ( inl-pushout f g)
    ( pair
      ( inr-pushout f g)
      ( glue-pushout f g))

postulate up-pushout : {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) → universal-property-pushout l4 f g (cocone-pushout f g)

cogap :
  { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  ( f : S → A) (g : S → B) →
  { X : UU l4} (c : cocone f g X) → pushout f g → X
cogap f g =
  map-universal-property-pushout f g
    ( cocone-pushout f g)
    ( up-pushout f g)

is-pushout :
  { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  ( f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
is-pushout f g c = is-equiv (cogap f g c)

-- Section 14.2 Suspensions

suspension-structure :
  {l1 l2 : Level} (X : UU l1) (Y : UU l2) → UU (l1 ⊔ l2)
suspension-structure X Y = Σ Y (λ N → Σ Y (λ S → (x : X) → Id N S))

suspension-cocone' :
  {l1 l2 : Level} (X : UU l1) (Y : UU l2) → UU (l1 ⊔ l2)
suspension-cocone' X Y = cocone (const X unit star) (const X unit star) Y

cocone-suspension-structure :
  {l1 l2 : Level} (X : UU l1) (Y : UU l2) →
  suspension-structure X Y → suspension-cocone' X Y
cocone-suspension-structure X Y (pair N (pair S merid)) =
  pair
    ( const unit Y N)
    ( pair
      ( const unit Y S)
      ( merid))

universal-property-suspension' :
  (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2)
  (susp-str : suspension-structure X Y) → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-suspension' l X Y susp-str-Y =
  universal-property-pushout l
    ( const X unit star)
    ( const X unit star)
    ( cocone-suspension-structure X Y susp-str-Y)

is-suspension :
  (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2) → UU (lsuc l ⊔ l1 ⊔ l2)
is-suspension l X Y =
  Σ (suspension-structure X Y) (universal-property-suspension' l X Y)

suspension :
  {l : Level} → UU l → UU l
suspension X = pushout (const X unit star) (const X unit star)

N-susp :
  {l : Level} {X : UU l} → suspension X
N-susp {X = X} = inl-pushout (const X unit star) (const X unit star) star

S-susp :
  {l : Level} {X : UU l} → suspension X
S-susp {X = X} = inr-pushout (const X unit star) (const X unit star) star

merid-susp :
  {l : Level} {X : UU l} → X → Id (N-susp {X = X}) (S-susp {X = X})
merid-susp {X = X} = glue-pushout (const X unit star) (const X unit star)

sphere : ℕ → UU lzero
sphere zero-ℕ = bool
sphere (succ-ℕ n) = suspension (sphere n)

N-sphere : (n : ℕ) → sphere n
N-sphere zero-ℕ = true
N-sphere (succ-ℕ n) = N-susp

S-sphere : (n : ℕ) → sphere n
S-sphere zero-ℕ = false
S-sphere (succ-ℕ n) = S-susp

{- We now work towards Lemma 17.2.2. -}

suspension-cocone :
  {l1 l2 : Level} (X : UU l1) (Z : UU l2) → UU _
suspension-cocone X Z = Σ Z (λ z1 → Σ Z (λ z2 → (x : X) → Id z1 z2))

ev-suspension :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
  (susp-str-Y : suspension-structure X Y) →
  (Z : UU l3) → (Y → Z) → suspension-cocone X Z
ev-suspension (pair N (pair S merid)) Z h =
  pair (h N) (pair (h S) (h ·l merid))

universal-property-suspension :
  (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2) →
  suspension-structure X Y → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-suspension l X Y susp-str-Y =
  (Z : UU l) → is-equiv (ev-suspension susp-str-Y Z)

comparison-suspension-cocone :
  {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
  suspension-cocone' X Z ≃ suspension-cocone X Z
comparison-suspension-cocone X Z =
  equiv-toto
    ( λ z1 → Σ Z (λ z2 → (x : X) → Id z1 z2))
    ( equiv-ev-star' Z)
    ( λ z1 →
      equiv-toto
        ( λ z2 → (x : X) → Id (z1 star) z2)
        ( equiv-ev-star' Z)
        ( λ z2 → equiv-id ((x : X) → Id (z1 star) (z2 star))))

map-comparison-suspension-cocone :
  {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
  suspension-cocone' X Z → suspension-cocone X Z
map-comparison-suspension-cocone X Z =
  map-equiv (comparison-suspension-cocone X Z)

is-equiv-map-comparison-suspension-cocone :
  {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
  is-equiv (map-comparison-suspension-cocone X Z)
is-equiv-map-comparison-suspension-cocone X Z =
  is-equiv-map-equiv (comparison-suspension-cocone X Z)

triangle-ev-suspension :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
  (susp-str-Y : suspension-structure X Y) →
  (Z : UU l3) →
  ( ( map-comparison-suspension-cocone X Z) ∘
    ( cocone-map
      ( const X unit star)
      ( const X unit star)
      ( cocone-suspension-structure X Y susp-str-Y))) ~
  ( ev-suspension susp-str-Y Z)
triangle-ev-suspension (pair N (pair S merid)) Z h = refl

is-equiv-ev-suspension :
  { l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
  ( susp-str-Y : suspension-structure X Y) →
  ( up-Y : universal-property-suspension' l3 X Y susp-str-Y) →
  ( Z : UU l3) → is-equiv (ev-suspension susp-str-Y Z)
is-equiv-ev-suspension {X = X} susp-str-Y up-Y Z =
  is-equiv-comp
    ( ev-suspension susp-str-Y Z)
    ( map-comparison-suspension-cocone X Z)
    ( cocone-map
      ( const X unit star)
      ( const X unit star)
      ( cocone-suspension-structure X _ susp-str-Y))
    ( htpy-inv (triangle-ev-suspension susp-str-Y Z))
    ( up-Y Z)
    ( is-equiv-map-comparison-suspension-cocone X Z)

{- Pointed maps and pointed homotopies. -}

pointed-fam :
  {l1 : Level} (l : Level) (X : UU-pt l1) → UU (lsuc l ⊔ l1)
pointed-fam l (pair X x) = Σ (X → UU l) (λ P → P x)

pointed-Π :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) → UU (l1 ⊔ l2)
pointed-Π (pair X x) (pair P p) = Σ ((x' : X) → P x') (λ f → Id (f x) p)

pointed-htpy :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) →
  (f g : pointed-Π X P) → UU (l1 ⊔ l2)
pointed-htpy (pair X x) (pair P p) (pair f α) g =
  pointed-Π (pair X x) (pair (λ x' → Id (f x') (pr1 g x')) (α ∙ (inv (pr2 g))))

pointed-refl-htpy :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) →
  (f : pointed-Π X P) → pointed-htpy X P f f
pointed-refl-htpy (pair X x) (pair P p) (pair f α) =
  pair refl-htpy (inv (right-inv α))

pointed-htpy-eq :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) →
  (f g : pointed-Π X P) → Id f g → pointed-htpy X P f g
pointed-htpy-eq X P f .f refl = pointed-refl-htpy X P f

is-contr-total-pointed-htpy :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) (f : pointed-Π X P) →
  is-contr (Σ (pointed-Π X P) (pointed-htpy X P f))
is-contr-total-pointed-htpy (pair X x) (pair P p) (pair f α) =
  is-contr-total-Eq-structure
    ( λ g β (H : f ~ g) → Id (H x) (α ∙ (inv β)))
    ( is-contr-total-htpy f)
    ( pair f refl-htpy)
    ( is-contr-equiv'
      ( Σ (Id (f x) p) (λ β → Id β α))
      ( equiv-tot (λ β → equiv-con-inv refl β α))
      ( is-contr-total-path' α))

is-equiv-pointed-htpy-eq :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) →
  (f g : pointed-Π X P) → is-equiv (pointed-htpy-eq X P f g)
is-equiv-pointed-htpy-eq X P f =
  fundamental-theorem-id f
    ( pointed-refl-htpy X P f)
    ( is-contr-total-pointed-htpy X P f)
    ( pointed-htpy-eq X P f)

eq-pointed-htpy :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) →
  (f g : pointed-Π X P) → (pointed-htpy X P f g) → Id f g
eq-pointed-htpy X P f g = inv-is-equiv (is-equiv-pointed-htpy-eq X P f g)

-- Section 14.3 Duality of pushouts and pullbacks

{- The universal property of the pushout of a span S can also be stated as a
   pullback-property: a cocone c = (pair i (pair j H)) with vertex X
   satisfies the universal property of the pushout of S if and only if the
   square

     Y^X -----> Y^B
      |          |
      |          |
      V          V
     Y^A -----> Y^S

   is a pullback square for every type Y. Below, we first define the cone of
   this commuting square, and then we introduce the type
   pullback-property-pushout, which states that the above square is a pullback.
   -}

htpy-precomp :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
  {f g : A → B} (H : f ~ g) (C : UU l3) →
  (precomp f C) ~ (precomp g C)
htpy-precomp H C h = eq-htpy (h ·l H)

compute-htpy-precomp :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (C : UU l3) →
  (htpy-precomp (refl-htpy' f) C) ~ refl-htpy
compute-htpy-precomp f C h = eq-htpy-refl-htpy (h ∘ f)

cone-pullback-property-pushout :
  {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (Y : UU l) →
  cone (λ (h : A → Y) → h ∘ f) (λ (h : B → Y) → h ∘ g) (X → Y)
cone-pullback-property-pushout f g {X} c Y =
  pair
    ( precomp (pr1 c) Y)
    ( pair
      ( precomp (pr1 (pr2 c)) Y)
      ( htpy-precomp (pr2 (pr2 c)) Y))

pullback-property-pushout :
  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  UU (l1 ⊔ (l2 ⊔ (l3 ⊔ (l4 ⊔ lsuc l))))
pullback-property-pushout l {S} {A} {B} f g {X} c =
  (Y : UU l) → is-pullback
    ( precomp f Y)
    ( precomp g Y)
    ( cone-pullback-property-pushout f g c Y)

{- In order to show that the universal property of pushouts is equivalent to
   the pullback property, we show that the maps cocone-map and the gap map fit
   in a commuting triangle, where the third map is an equivalence. The claim
   then follows from the 3-for-2 property of equivalences. -}

triangle-pullback-property-pushout-universal-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2}
  {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  {l : Level} (Y : UU l) →
  ( cocone-map f g c) ~
  ( ( tot (λ i' → tot (λ j' p → htpy-eq p))) ∘
    ( gap (λ h → h ∘ f) (λ h → h ∘ g) (cone-pullback-property-pushout f g c Y)))
triangle-pullback-property-pushout-universal-property-pushout
  {S = S} {A = A} {B = B} f g (pair i (pair j H)) Y h =
    eq-pair refl (eq-pair refl (inv (issec-eq-htpy (h ·l H))))

pullback-property-pushout-universal-property-pushout :
  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2}
  {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  universal-property-pushout l f g c → pullback-property-pushout l f g c
pullback-property-pushout-universal-property-pushout
  l f g (pair i (pair j H)) up-c Y =
  let c = (pair i (pair j H)) in
  is-equiv-right-factor
    ( cocone-map f g c)
    ( tot (λ i' → tot (λ j' p → htpy-eq p)))
    ( gap (λ h → h ∘ f) (λ h → h ∘ g) (cone-pullback-property-pushout f g c Y))
    ( triangle-pullback-property-pushout-universal-property-pushout f g c Y)
    ( is-equiv-tot-is-fiberwise-equiv
      ( λ i' → is-equiv-tot-is-fiberwise-equiv
        ( λ j' → funext (i' ∘ f) (j' ∘ g))))
    ( up-c Y)

universal-property-pushout-pullback-property-pushout :
  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2}
  {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  pullback-property-pushout l f g c → universal-property-pushout l f g c
universal-property-pushout-pullback-property-pushout
  l f g (pair i (pair j H)) pb-c Y =
  let c = (pair i (pair j H)) in
  is-equiv-comp
    ( cocone-map f g c)
    ( tot (λ i' → tot (λ j' p → htpy-eq p)))
    ( gap (λ h → h ∘ f) (λ h → h ∘ g) (cone-pullback-property-pushout f g c Y))
    ( triangle-pullback-property-pushout-universal-property-pushout f g c Y)
    ( pb-c Y)
    ( is-equiv-tot-is-fiberwise-equiv
      ( λ i' → is-equiv-tot-is-fiberwise-equiv
        ( λ j' → funext (i' ∘ f) (j' ∘ g))))

cocone-compose-horizontal :
  { l1 l2 l3 l4 l5 l6 : Level}
  { A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
  ( f : A → X) (i : A → B) (k : B → C) →
  ( c : cocone f i Y) (d : cocone (pr1 (pr2 c)) k Z) →
  cocone f (k ∘ i) Z
cocone-compose-horizontal f i k (pair j (pair g H)) (pair l (pair h K)) =
  pair
    ( l ∘ j)
    ( pair
      ( h)
      ( (l ·l H) ∙h (K ·r i)))

{-
is-pushout-rectangle-is-pushout-right-square :
  ( l : Level) { l1 l2 l3 l4 l5 l6 : Level}
  { A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
  ( f : A → X) (i : A → B) (k : B → C) →
  ( c : cocone f i Y) (d : cocone (pr1 (pr2 c)) k Z) →
  universal-property-pushout l f i c →
  universal-property-pushout l (pr1 (pr2 c)) k d →
  universal-property-pushout l f (k ∘ i) (cocone-compose-horizontal f i k c d)
is-pushout-rectangle-is-pushout-right-square l f i k c d up-Y up-Z =
  universal-property-pushout-pullback-property-pushout l f (k ∘ i)
    ( cocone-compose-horizontal f i k c d)
    ( λ T → is-pullback-htpy {!!} {!!} {!!} {!!} {!!} {!!} {!!})
-}

-- Examples of pushouts

{- The cofiber of a map. -}

cofiber :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2)
cofiber {A = A} f = pushout f (const A unit star)

cocone-cofiber :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  cocone f (const A unit star) (cofiber f)
cocone-cofiber {A = A} f = cocone-pushout f (const A unit star)

inl-cofiber :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → B → cofiber f
inl-cofiber {A = A} f = pr1 (cocone-cofiber f)

inr-cofiber :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → unit → cofiber f
inr-cofiber f = pr1 (pr2 (cocone-cofiber f))

pt-cofiber :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → cofiber f
pt-cofiber {A = A} f = inr-cofiber f star

cofiber-ptd :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → UU-pt (l1 ⊔ l2)
cofiber-ptd f = pair (cofiber f) (pt-cofiber f)

up-cofiber :
  { l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  ( {l : Level} →
    universal-property-pushout l f (const A unit star) (cocone-cofiber f))
up-cofiber {A = A} f = up-pushout f (const A unit star)

_*_ :
  {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2)
A * B = pushout (pr1 {A = A} {B = λ x → B}) pr2

cocone-join :
  {l1 l2 : Level} (A : UU l1) (B : UU l2) →
  cocone (pr1 {A = A} {B = λ x → B}) pr2 (A * B)
cocone-join A B = cocone-pushout pr1 pr2

up-join :
  {l1 l2 : Level} (A : UU l1) (B : UU l2) →
  ( {l : Level} → universal-property-pushout l
    ( pr1 {A = A} {B = λ x → B}) pr2 (cocone-join A B))
up-join A B = up-pushout pr1 pr2

inl-join :
  {l1 l2 : Level} (A : UU l1) (B : UU l2) → A → A * B
inl-join A B = pr1 (cocone-join A B)

inr-join :
  {l1 l2 : Level} (A : UU l1) (B : UU l2) → B → A * B
inr-join A B = pr1 (pr2 (cocone-join A B))

glue-join :
  {l1 l2 : Level} (A : UU l1) (B : UU l2) (t : A × B) →
  Id (inl-join A B (pr1 t)) (inr-join A B (pr2 t))
glue-join A B = pr2 (pr2 (cocone-join A B))

_∨_ :
  {l1 l2 : Level} (A : UU-pt l1) (B : UU-pt l2) → UU-pt (l1 ⊔ l2)
A ∨ B =
  pair
    ( pushout
      ( const unit (pr1 A) (pr2 A))
      ( const unit (pr1 B) (pr2 B)))
    ( inl-pushout
      ( const unit (pr1 A) (pr2 A))
      ( const unit (pr1 B) (pr2 B))
      ( pr2 A))

indexed-wedge :
  {l1 l2 : Level} (I : UU l1) (A : I → UU-pt l2) → UU-pt (l1 ⊔ l2)
indexed-wedge I A =
  pair
    ( cofiber (λ i → pair i (pr2 (A i))))
    ( pt-cofiber (λ i → pair i (pr2 (A i))))

wedge-inclusion :
  {l1 l2 : Level} (A : UU-pt l1) (B : UU-pt l2) →
  pr1 (A ∨ B) → (pr1 A) × (pr1 B)
wedge-inclusion {l1} {l2} (pair A a) (pair B b) =
  inv-is-equiv
    ( up-pushout
      ( const unit A a)
      ( const unit B b)
      ( A × B))
    ( pair
      ( λ x → pair x b)
      ( pair
        ( λ y → pair a y)
        ( refl-htpy)))

-- Exercises

-- Exercise 13.1

-- Exercise 13.2

is-equiv-universal-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g C) →
  is-equiv f →
  ({l : Level} → universal-property-pushout l f g c) → is-equiv (pr1 (pr2 c))
is-equiv-universal-property-pushout
  {A = A} {B} f g (pair i (pair j H)) is-equiv-f up-c =
  is-equiv-is-equiv-precomp j
    ( λ l T →
      is-equiv-is-pullback'
        ( λ (h : A → T) → h ∘ f)
        ( λ (h : B → T) → h ∘ g)
        ( cone-pullback-property-pushout f g (pair i (pair j H)) T)
        ( is-equiv-precomp-is-equiv f is-equiv-f T)
        ( pullback-property-pushout-universal-property-pushout
          l f g (pair i (pair j H)) up-c T))

equiv-universal-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (e : S ≃ A) (g : S → B) (c : cocone (map-equiv e) g C) →
  ({l : Level} → universal-property-pushout l (map-equiv e) g c) →
  B ≃ C
equiv-universal-property-pushout e g c up-c =
  pair
    ( pr1 (pr2 c))
    ( is-equiv-universal-property-pushout
      ( map-equiv e)
      ( g)
      ( c)
      ( is-equiv-map-equiv e)
      ( up-c))

is-equiv-universal-property-pushout' :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g C) →
  is-equiv g →
  ({l : Level} → universal-property-pushout l f g c) →
  is-equiv (pr1 c)
is-equiv-universal-property-pushout' f g (pair i (pair j H)) is-equiv-g up-c =
  is-equiv-is-equiv-precomp i
    ( λ l T →
      is-equiv-is-pullback
        ( precomp f T)
        ( precomp g T)
        ( cone-pullback-property-pushout f g (pair i (pair j H)) T)
        ( is-equiv-precomp-is-equiv g is-equiv-g T)
        ( pullback-property-pushout-universal-property-pushout
          l f g (pair i (pair j H)) up-c T))

equiv-universal-property-pushout' :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (f : S → A) (e : S ≃ B) (c : cocone f (map-equiv e) C) →
  ({l : Level} → universal-property-pushout l f (map-equiv e) c) →
  A ≃ C
equiv-universal-property-pushout' f e c up-c =
  pair
    ( pr1 c)
    ( is-equiv-universal-property-pushout'
      ( f)
      ( map-equiv e)
      ( c)
      ( is-equiv-map-equiv e)
      ( up-c))

universal-property-pushout-is-equiv :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g C) →
  is-equiv f → is-equiv (pr1 (pr2 c)) →
  ({l : Level} → universal-property-pushout l f g c)
universal-property-pushout-is-equiv f g (pair i (pair j H)) is-equiv-f is-equiv-j {l} =
  let c = (pair i (pair j H)) in
  universal-property-pushout-pullback-property-pushout l f g c
    ( λ T → is-pullback-is-equiv'
      ( λ h → h ∘ f)
      ( λ h → h ∘ g)
      ( cone-pullback-property-pushout f g c T)
      ( is-equiv-precomp-is-equiv f is-equiv-f T)
      ( is-equiv-precomp-is-equiv j is-equiv-j T))

universal-property-pushout-is-equiv' :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g C) →
  is-equiv g → is-equiv (pr1 c) →
  ({l : Level} → universal-property-pushout l f g c)
universal-property-pushout-is-equiv'
  f g (pair i (pair j H)) is-equiv-g is-equiv-i {l} =
  let c = (pair i (pair j H)) in
  universal-property-pushout-pullback-property-pushout l f g c
    ( λ T → is-pullback-is-equiv
      ( precomp f T)
      ( precomp g T)
      ( cone-pullback-property-pushout f g c T)
      ( is-equiv-precomp-is-equiv g is-equiv-g T)
      ( is-equiv-precomp-is-equiv i is-equiv-i T))

is-contr-suspension-is-contr :
  {l : Level} {X : UU l} → is-contr X → is-contr (suspension X)
is-contr-suspension-is-contr {l} {X} is-contr-X =
  is-contr-is-equiv'
    ( unit)
    ( pr1 (pr2 (cocone-pushout (const X unit star) (const X unit star))))
    ( is-equiv-universal-property-pushout
      ( const X unit star)
      ( const X unit star)
      ( cocone-pushout
        ( const X unit star)
        ( const X unit star))
      ( is-equiv-is-contr (const X unit star) is-contr-X is-contr-unit)
      ( up-pushout (const X unit star) (const X unit star)))
    ( is-contr-unit)

is-contr-cofiber-is-equiv :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  is-equiv f → is-contr (cofiber f)
is-contr-cofiber-is-equiv {A = A} {B} f is-equiv-f =
  is-contr-is-equiv'
    ( unit)
    ( pr1 (pr2 (cocone-cofiber f)))
    ( is-equiv-universal-property-pushout
      ( f)
      ( const A unit star)
      ( cocone-cofiber f)
      ( is-equiv-f)
      ( up-cofiber f))
    ( is-contr-unit)

is-equiv-cofiber-point :
  {l : Level} {B : UU l} (b : B) →
  is-equiv (pr1 (cocone-pushout (const unit B b) (const unit unit star)))
is-equiv-cofiber-point {l} {B} b =
  is-equiv-universal-property-pushout'
    ( const unit B b)
    ( const unit unit star)
    ( cocone-pushout (const unit B b) (const unit unit star))
    ( is-equiv-is-contr (const unit unit star) is-contr-unit is-contr-unit)
    ( up-pushout (const unit B b) (const unit unit star))

is-equiv-inr-join-empty :
  {l : Level} (X : UU l) → is-equiv (inr-join empty X)
is-equiv-inr-join-empty X =
  is-equiv-universal-property-pushout
    ( pr1 {A = empty} {B = λ t → X})
    ( pr2)
    ( cocone-join empty X)
    ( is-equiv-pr1-prod-empty X)
    ( up-join empty X)

left-unit-law-join :
  {l : Level} (X : UU l) → X ≃ (empty * X)
left-unit-law-join X =
  pair (inr-join empty X) (is-equiv-inr-join-empty X)

is-equiv-inl-join-empty :
  {l : Level} (X : UU l) → is-equiv (inl-join X empty)
is-equiv-inl-join-empty X =
  is-equiv-universal-property-pushout'
    ( pr1)
    ( pr2)
    ( cocone-join X empty)
    ( is-equiv-pr2-prod-empty X)
    ( up-join X empty)

right-unit-law-join :
  {l : Level} (X : UU l) → X ≃ (X * empty)
right-unit-law-join X =
  pair (inl-join X empty) (is-equiv-inl-join-empty X)

inv-map-left-unit-law-prod :
  {l : Level} (X : UU l) → X → (unit × X)
inv-map-left-unit-law-prod X = pair star

issec-inv-map-left-unit-law-prod :
  {l : Level} (X : UU l) → (pr2 ∘ (inv-map-left-unit-law-prod X)) ~ id
issec-inv-map-left-unit-law-prod X x = refl

isretr-inv-map-left-unit-law-prod :
  {l : Level} (X : UU l) → ((inv-map-left-unit-law-prod X) ∘ pr2) ~ id
isretr-inv-map-left-unit-law-prod X (pair star x) = refl

is-equiv-left-unit-law-prod :
  {l : Level} (X : UU l) → is-equiv (pr2 {A = unit} {B = λ t → X})
is-equiv-left-unit-law-prod X =
  is-equiv-has-inverse
    ( inv-map-left-unit-law-prod X)
    ( issec-inv-map-left-unit-law-prod X)
    ( isretr-inv-map-left-unit-law-prod X)

left-unit-law-prod :
  {l : Level} (X : UU l) → (unit × X) ≃ X
left-unit-law-prod X =
  pair pr2 (is-equiv-left-unit-law-prod X)

is-equiv-inl-join-unit :
  {l : Level} (X : UU l) → is-equiv (inl-join unit X)
is-equiv-inl-join-unit X =
  is-equiv-universal-property-pushout'
    ( pr1)
    ( pr2)
    ( cocone-join unit X)
    ( is-equiv-left-unit-law-prod X)
    ( up-join unit X)

left-zero-law-join :
  {l : Level} (X : UU l) → is-contr (unit * X)
left-zero-law-join X =
  is-contr-equiv'
    ( unit)
    ( pair (inl-join unit X) (is-equiv-inl-join-unit X))
    ( is-contr-unit)

inv-map-right-unit-law-prod :
  {l : Level} (X : UU l) → X → X × unit
inv-map-right-unit-law-prod X x = pair x star

issec-inv-map-right-unit-law-prod :
  {l : Level} (X : UU l) → (pr1 ∘ (inv-map-right-unit-law-prod X)) ~ id
issec-inv-map-right-unit-law-prod X x = refl

isretr-inv-map-right-unit-law-prod :
  {l : Level} (X : UU l) → ((inv-map-right-unit-law-prod X) ∘ pr1) ~ id
isretr-inv-map-right-unit-law-prod X (pair x star) = refl

is-equiv-right-unit-law-prod :
  {l : Level} (X : UU l) → is-equiv (pr1 {A = X} {B = λ t → unit})
is-equiv-right-unit-law-prod X =
  is-equiv-has-inverse
    ( inv-map-right-unit-law-prod X)
    ( issec-inv-map-right-unit-law-prod X)
    ( isretr-inv-map-right-unit-law-prod X)

right-unit-law-prod :
  {l : Level} (X : UU l) → (X × unit) ≃ X
right-unit-law-prod X =
  pair pr1 (is-equiv-right-unit-law-prod X)

is-equiv-inr-join-unit :
  {l : Level} (X : UU l) → is-equiv (inr-join X unit)
is-equiv-inr-join-unit X =
  is-equiv-universal-property-pushout
    ( pr1)
    ( pr2)
    ( cocone-join X unit)
    ( is-equiv-right-unit-law-prod X)
    ( up-join X unit)

right-zero-law-join :
  {l : Level} (X : UU l) → is-contr (X * unit)
right-zero-law-join X =
  is-contr-equiv'
    ( unit)
    ( pair (inr-join X unit) (is-equiv-inr-join-unit X))
    ( is-contr-unit)

unit-pt : UU-pt lzero
unit-pt = pair unit star

is-contr-pt :
  {l : Level} → UU-pt l → UU l
is-contr-pt A = is-contr (pr1 A)

-- Exercise 16.2

-- ev-disjunction :
--   {l1 l2 l3 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) (R : UU-Prop l3) →
--   ((type-Prop P) * (type-Prop Q) → (type-Prop R)) →
--   (type-Prop P → type-Prop R) × (type-Prop Q → type-Prop R)
-- ev-disjunction P Q R f =
--   pair
--     ( f ∘ (inl-join (type-Prop P) (type-Prop Q)))
--     ( f ∘ (inr-join (type-Prop P) (type-Prop Q)))

-- comparison-ev-disjunction :
--   {l1 l2 l3 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) (R : UU-Prop l3) →
--   cocone-join (type-Prop P) (type-Prop Q) (type-Prop R)

-- universal-property-disjunction-join-prop :
--   {l1 l2 l3 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) (R : UU-Prop l3) →
--   is-equiv (ev-disjunction P Q R)

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
{-# OPTIONS --without-K --safe #-}

open import Categories.Category
open import Categories.Category.Monoidal

-- the definition used here is not very similar to what one usually sees in nLab or
-- any textbook.  the difference is that usually closed monoidal category is defined
-- through a right adjoint of -⊗X, which is [X,-]. then there is an induced bifunctor
-- [-,-].
--
-- but in proof relevant context, the induced bifunctor [-,-] does not have to be
-- exactly the intended bifunctor! in fact, one can probably only show that the
-- intended bifunctor is only naturally isomorphic to the induced one, which is
-- significantly weaker.
--
-- the approach taken here as an alternative is to BEGIN with a bifunctor
-- already. however, is it required to have mates between any given two adjoints. this
-- definition can be shown equivalent to the previous one but just works better.
module Categories.Category.Monoidal.Closed {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where

private
  module C = Category C
  open Category C

  variable
    X Y A B : Obj

open import Level
open import Data.Product using (_,_)

open import Categories.Adjoint
open import Categories.Adjoint.Mate
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Hom
open import Categories.Category.Instance.Setoids
open import Categories.NaturalTransformation hiding (id)
open import Categories.NaturalTransformation.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism as NI

record Closed : Set (levelOfTerm M) where
  open Monoidal M public

  field
    [-,-]   : Bifunctor C.op C C
    adjoint : (-⊗ X) ⊣ appˡ [-,-] X
    mate    : (f : X ⇒ Y) → Mate (adjoint {X}) (adjoint {Y}) (appʳ-nat ⊗ f) (appˡ-nat [-,-] f)

  module [-,-]        = Functor [-,-]
  module adjoint {X}  = Adjoint (adjoint {X})
  module mate {X Y} f = Mate (mate {X} {Y} f)

  [_,-] : Obj → Functor C C
  [_,-] = appˡ [-,-]

  [-,_] : Obj → Functor C.op C
  [-,_] = appʳ [-,-]

  [_,_]₀ : Obj → Obj → Obj
  [ X , Y ]₀ = [-,-].F₀ (X , Y)

  [_,_]₁ : A ⇒ B → X ⇒ Y → [ B , X ]₀ ⇒ [ A , Y ]₀
  [ f , g ]₁ = [-,-].F₁ (f , g)

  Hom[-⊗_,-] : ∀ X → Bifunctor C.op C (Setoids ℓ e)
  Hom[-⊗ X ,-] = adjoint.Hom[L-,-] {X}

  Hom[-,[_,-]] : ∀ X → Bifunctor C.op C (Setoids ℓ e)
  Hom[-,[ X ,-]] = adjoint.Hom[-,R-] {X}

  Hom-NI : ∀ {X : Obj} → NaturalIsomorphism Hom[-⊗ X ,-] Hom[-,[ X ,-]]
  Hom-NI = Hom-NI′ adjoint

ext: agda

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Bifunctor where

open import Level
open import Data.Product using (_,_; swap)

open import Categories.Category

open import Categories.Functor public
open import Categories.Product

Bifunctor : ∀ {o ℓ e} {o′ ℓ′ e′} {o′′ ℓ′′ e′′} → Category o ℓ e → Category o′ ℓ′ e′ → Category o′′ ℓ′′ e′′ → Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′ ⊔ o′′ ⊔ ℓ′′ ⊔ e′′)
Bifunctor C D E = Functor (Product C D) E

overlap-× : ∀ {o ℓ e} {o′₁ ℓ′₁ e′₁} {o′₂ ℓ′₂ e′₂} {C : Category o ℓ e} {D₁ : Category o′₁ ℓ′₁ e′₁} {D₂ : Category o′₂ ℓ′₂ e′₂} (H : Bifunctor D₁ D₂ C) {o″ ℓ″ e″} {E : Category o″ ℓ″ e″} (F : Functor E D₁) (G : Functor E D₂) → Functor E C
overlap-× H F G = H ∘ (F ※ G)

reduce-× : ∀ {o ℓ e} {o′₁ ℓ′₁ e′₁} {o′₂ ℓ′₂ e′₂} {C : Category o ℓ e} {D₁ : Category o′₁ ℓ′₁ e′₁} {D₂ : Category o′₂ ℓ′₂ e′₂} (H : Bifunctor D₁ D₂ C) {o″₁ ℓ″₁ e″₁} {E₁ : Category o″₁ ℓ″₁ e″₁} (F : Functor E₁ D₁) {o″₂ ℓ″₂ e″₂} {E₂ : Category o″₂ ℓ″₂ e″₂} (G : Functor E₂ D₂) → Bifunctor E₁ E₂ C
reduce-× H F G = H ∘ (F ⁂ G)

flip-bifunctor : ∀ {o ℓ e} {o′ ℓ′ e′} {o′′ ℓ′′ e′′} {C : Category o ℓ e} → {D : Category o′ ℓ′ e′} → {E : Category o′′ ℓ′′ e′′} → Bifunctor C D E → Bifunctor D C E
flip-bifunctor {C = C} {D = D} {E = E} b = _∘_ b (Swap {C = C} {D = D})

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Cats.Functor.Op where

open import Cats.Category.Base
open import Cats.Category.Op using (_ᵒᵖ)
open import Cats.Functor using (Functor)

open Functor

Op : ∀ {lo la l≈ lo′ la′ l≈′}
  → {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
  → Functor C D
  → Functor (C ᵒᵖ) (D ᵒᵖ)
Op F = record
    { fobj = fobj F
    ; fmap = fmap F
    ; fmap-resp = fmap-resp F
    ; fmap-id = fmap-id F
    ; fmap-∘ = fmap-∘ F
    }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module Tactic.Deriving.Quotable where

open import Prelude
open import Container.Traversable
open import Tactic.Reflection
open import Tactic.Reflection.Quote.Class
open import Tactic.Deriving

private
  -- Bootstrapping
  qVis : Visibility → Term
  qVis visible = con (quote visible) []
  qVis hidden = con (quote hidden) []
  qVis instance′ = con (quote instance′) []

  qRel : Relevance → Term
  qRel relevant   = con (quote relevant) []
  qRel irrelevant = con (quote irrelevant) []

  qArgInfo : ArgInfo → Term
  qArgInfo (arg-info v r) = con₂ (quote arg-info) (qVis v) (qRel r)

  qArg : Arg Term → Term
  qArg (arg i x) = con₂ (quote arg) (qArgInfo i) x

  qList : List Term → Term
  qList = foldr (λ x xs → con₂ (quote List._∷_) x xs)
                (con₀ (quote List.[]))

  -- Could compute this from the type of the dictionary constructor
  quoteType : Name → TC Type
  quoteType d =
    caseM instanceTelescope d (quote Quotable) of λ
    { (tel , vs) → pure $ telPi tel $ def d vs `→ def (quote Term) []
    }

  dictConstructor : TC Name
  dictConstructor =
    caseM getConstructors (quote Quotable) of λ
    { (c ∷ []) → pure c
    ; _ → typeErrorS "impossible" }

  patArgs : Telescope → List (Arg Pattern)
  patArgs tel = map (var "x" <$_) tel

  quoteArgs′ : Nat → Telescope → List Term
  quoteArgs′ 0 _  = []
  quoteArgs′ _ [] = []
  quoteArgs′ (suc n) (a ∷ tel) =
    qArg (def₁ (quote `) (var n []) <$ a) ∷ quoteArgs′ n tel

  quoteArgs : Nat → Telescope → Term
  quoteArgs pars tel = qList $ replicate pars (qArg $ hArg (con₀ (quote Term.unknown))) ++
                               quoteArgs′ (length tel) tel

  constructorClause : Nat → Name → TC Clause
  constructorClause pars c = do
    tel ← drop pars ∘ fst ∘ telView <$> getType c
    pure (clause (vArg (con c (patArgs tel)) ∷ [])
                    (con₂ (quote Term.con) (lit (name c)) (quoteArgs pars tel)))

  quoteClauses : Name → TC (List Clause)
  quoteClauses d = do
    n ← getParameters d
    caseM getConstructors d of λ where
      [] → pure [ absurd-clause (vArg absurd ∷ []) ]
      cs → mapM (constructorClause n) cs

declareQuotableInstance : Name → Name → TC ⊤
declareQuotableInstance iname d =
  declareDef (iArg iname) =<< instanceType d (quote Quotable)

defineQuotableInstance : Name → Name → TC ⊤
defineQuotableInstance iname d = do
  fname ← freshName ("quote[" & show d & "]")
  declareDef (vArg fname) =<< quoteType d
  dictCon ← dictConstructor
  defineFun iname (clause [] (con₁ dictCon (def₀ fname)) ∷ [])
  defineFun fname =<< quoteClauses d
  return _

deriveQuotable : Name → Name → TC ⊤
deriveQuotable iname d =
  declareQuotableInstance iname d >>
  defineQuotableInstance  iname d

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
open import Data.Product using ( _×_ )
open import FRP.LTL.ISet.Core using ( ISet ; ⌈_⌉ ; M⟦_⟧ )
open import FRP.LTL.Time using ( Time )
open import FRP.LTL.Time.Bound using ( fin ; _≺_ )
open import FRP.LTL.Time.Interval using ( [_⟩ ; sing )

module FRP.LTL.ISet.Until where

data _Until_ (A B : ISet) (t : Time) : Set where
  now : M⟦ B ⟧ (sing t) → (A Until B) t
  later : ∀ {u} → .(t≺u : fin t ≺ fin u) → M⟦ A ⟧ [ t≺u ⟩ → M⟦ B ⟧ (sing u) → (A Until B) t

_U_ : ISet → ISet → ISet
A U B = ⌈ A Until B ⌉

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
module Sets.ExtensionalPredicateSet where

import      Lvl
open import Data
open import Data.Boolean
open import Data.Either as Either using (_‖_)
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Function.Equals
open import Function.Equals.Proofs
open import Function.Inverse
open import Function.Proofs
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
open import Structure.Setoid renaming (_≡_ to _≡ₑ_)
open import Structure.Function.Domain
open import Structure.Function.Domain.Proofs
open import Structure.Function
open import Structure.Relator.Equivalence
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Structure.Relator.Proofs
open import Structure.Relator
open import Syntax.Transitivity
open import Type
open import Type.Size

private variable ℓ ℓₒ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓ₁ ℓ₂ ℓ₃ : Lvl.Level
private variable T A A₁ A₂ B : Type{ℓ}

-- A set of objects of a certain type where equality is based on setoids.
-- This is defined by the containment predicate (_∋_) and a proof that it respects the setoid structure.
-- (A ∋ a) is read "The set A contains the element a".
-- Note: This is only a "set" within a certain type, so a collection of type PredSet(T) is actually a subcollection of T.
record PredSet {ℓ ℓₒ ℓₑ} (T : Type{ℓₒ}) ⦃ equiv : Equiv{ℓₑ}(T) ⦄ : Type{Lvl.𝐒(ℓ) Lvl.⊔ ℓₒ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    _∋_ : T → Stmt{ℓ}
    ⦃ preserve-equiv ⦄ : UnaryRelator(_∋_)
open PredSet using (_∋_) public
open PredSet using (preserve-equiv)

-- Element-set relations.
module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  -- The membership relation.
  -- (a ∈ A) is read "The element a is included in the set A".
  _∈_ : T → PredSet{ℓ}(T) → Stmt
  _∈_ = swap(_∋_)

  _∉_ : T → PredSet{ℓ}(T) → Stmt
  _∉_ = (¬_) ∘₂ (_∈_)

  _∌_ : PredSet{ℓ}(T) → T → Stmt
  _∌_ = (¬_) ∘₂ (_∋_)

  NonEmpty : PredSet{ℓ}(T) → Stmt
  NonEmpty(S) = ∃(_∈ S)

-- Set-bounded quantifiers.
module _ {T : Type{ℓₒ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  ∀ₛ : PredSet{ℓ}(T) → (T → Stmt{ℓ₁}) → Stmt{ℓ Lvl.⊔ ℓ₁ Lvl.⊔ ℓₒ}
  ∀ₛ(S) P = ∀{elem : T} → (elem ∈ S) → P(elem)

  ∃ₛ : PredSet{ℓ}(T) → (T → Stmt{ℓ₁}) → Stmt{ℓ Lvl.⊔ ℓ₁ Lvl.⊔ ℓₒ}
  ∃ₛ(S) P = ∃(elem ↦ (elem ∈ S) ∧ P(elem))

-- Sets and set operations.
module _ {T : Type{ℓₒ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  -- An empty set.
  -- Contains nothing.
  ∅ : PredSet{ℓ}(T)
  ∅ ∋ x = Empty
  UnaryRelator.substitution (preserve-equiv ∅) = const id

  -- An universal set.
  -- Contains everything.
  -- Note: Everything as in every object of type  T.
  𝐔 : PredSet{ℓ}(T)
  𝐔 ∋ x = Unit
  UnaryRelator.substitution (preserve-equiv 𝐔) = const id

  -- A singleton set (a set containing only one element).
  •_ : T → PredSet(T)
  (• a) ∋ x = x ≡ₑ a
  UnaryRelator.substitution (preserve-equiv (• a)) xy xa = symmetry(_≡ₑ_) xy 🝖 xa

  -- An union of two sets.
  -- Contains the elements that any of the both sets contain.
  _∪_ : PredSet{ℓ₁}(T) → PredSet{ℓ₂}(T) → PredSet(T)
  (A ∪ B) ∋ x = (A ∋ x) ∨ (B ∋ x)
  UnaryRelator.substitution (preserve-equiv (A ∪ B)) xy = Either.map (substitute₁(A ∋_) xy) (substitute₁(B ∋_) xy)
  infixr 1000 _∪_

  -- An intersection of two sets.
  -- Contains the elements that both of the both sets contain.
  _∩_ : PredSet{ℓ₁}(T) → PredSet{ℓ₂}(T) → PredSet(T)
  (A ∩ B) ∋ x = (A ∋ x) ∧ (B ∋ x)
  UnaryRelator.substitution (preserve-equiv (A ∩ B)) xy = Tuple.map (substitute₁(A ∋_) xy) (substitute₁(B ∋_) xy)
  infixr 1001 _∩_

  -- A complement of a set.
  -- Contains the elements that the set does not contain.
  ∁_ : PredSet{ℓ}(T) → PredSet(T)
  (∁ A) ∋ x = A ∌ x
  UnaryRelator.substitution (preserve-equiv (∁ A)) xy = contrapositiveᵣ (substitute₁(A ∋_) (symmetry(_≡ₑ_) xy))
  infixr 1002 ∁_

  -- A relative complement of a set.
  -- Contains the elements that the left set contains without the elements included in the right set..
  _∖_ : PredSet{ℓ₁}(T) → PredSet{ℓ₂}(T) → PredSet(T)
  A ∖ B = (A ∩ (∁ B))
  infixr 1001 _∖_

  filter : (P : T → Stmt{ℓ₁}) ⦃ _ : UnaryRelator(P) ⦄ → PredSet{ℓ₂}(T) → PredSet(T)
  filter P(A) ∋ x = (x ∈ A) ∧ P(x)
  _⨯_.left (UnaryRelator.substitution (preserve-equiv (filter P A)) xy ([∧]-intro xA Px)) = substitute₁(A ∋_) xy xA
  _⨯_.right (UnaryRelator.substitution (preserve-equiv (filter P A)) xy ([∧]-intro xA Px)) = substitute₁(P) xy Px

unapply : ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ → (f : A → B) ⦃ func-f : Function(f) ⦄ → B → PredSet(A)
unapply f(y) ∋ x = f(x) ≡ₑ y
preserve-equiv (unapply f(y)) = [∘]-unaryRelator ⦃ rel = binary-unaryRelatorᵣ ⦃ rel-P = [≡]-binaryRelator ⦄ ⦄

⊶ : ⦃ _ : Equiv{ℓₑ₂}(B) ⦄ → (f : A → B) → PredSet(B)
⊶ f ∋ y = ∃(x ↦ f(x) ≡ₑ y)
preserve-equiv (⊶ f) = [∃]-unaryRelator ⦃ rel-P = binary-unaryRelatorₗ ⦃ rel-P = [≡]-binaryRelator ⦄ ⦄

unmap : ⦃ _ : Equiv{ℓₑ₁}(A) ⦄ ⦃ _ : Equiv{ℓₑ₂}(B) ⦄ → (f : A → B) ⦃ _ : Function(f) ⦄ → PredSet{ℓ}(B) → PredSet(A)
(unmap f(Y)) ∋ x = f(x) ∈ Y
preserve-equiv (unmap f x) = [∘]-unaryRelator

map : ⦃ _ : Equiv{ℓₑ₁}(A) ⦄ ⦃ _ : Equiv{ℓₑ₂}(B) ⦄ → (f : A → B) → PredSet{ℓ}(A) → PredSet(B)
map f(S) ∋ y = ∃(x ↦ (x ∈ S) ∧ (f(x) ≡ₑ y))
preserve-equiv (map f S) = [∃]-unaryRelator ⦃ rel-P = [∧]-unaryRelator ⦃ rel-Q = binary-unaryRelatorₗ ⦃ rel-P = [≡]-binaryRelator ⦄ ⦄ ⦄

map₂ : ⦃ _ : Equiv{ℓₑ₁}(A₁) ⦄ ⦃ _ : Equiv{ℓₑ₂}(A₂) ⦄ ⦃ _ : Equiv{ℓₑ₃}(B) ⦄ → (_▫_ : A₁ → A₂ → B) → PredSet{ℓ₁}(A₁) → PredSet{ℓ₂}(A₂) → PredSet(B)
map₂(_▫_) S₁ S₂ ∋ y = ∃{Obj = _ ⨯ _}(\{(x₁ , x₂) → (x₁ ∈ S₁) ∧ (x₂ ∈ S₂) ∧ ((x₁ ▫ x₂) ≡ₑ y)})
preserve-equiv (map₂ (_▫_) S₁ S₂) = [∃]-unaryRelator ⦃ rel-P = [∧]-unaryRelator ⦃ rel-P = [∧]-unaryRelator ⦄ ⦃ rel-Q = binary-unaryRelatorₗ ⦃ rel-P = [≡]-binaryRelator ⦄ ⦄ ⦄

-- Set-set relations.
module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  record _⊆_ (A : PredSet{ℓ₁}(T)) (B : PredSet{ℓ₂}(T)) : Stmt{Lvl.of(T) Lvl.⊔ ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : ∀{x} → (x ∈ A) → (x ∈ B)

  record _⊇_ (A : PredSet{ℓ₁}(T)) (B : PredSet{ℓ₂}(T)) : Stmt{Lvl.of(T) Lvl.⊔ ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : ∀{x} → (x ∈ A) ← (x ∈ B)

  record _≡_ (A : PredSet{ℓ₁}(T)) (B : PredSet{ℓ₂}(T)) : Stmt{Lvl.of(T) Lvl.⊔ ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : ∀{x} → (x ∈ A) ↔ (x ∈ B)

  instance
    [≡]-reflexivity : Reflexivity(_≡_ {ℓ})
    Reflexivity.proof [≡]-reflexivity = intro [↔]-reflexivity

  instance
    [≡]-symmetry : Symmetry(_≡_ {ℓ})
    Symmetry.proof [≡]-symmetry (intro xy) = intro([↔]-symmetry xy)

  [≡]-transitivity-raw : ∀{A : PredSet{ℓ₁}(T)}{B : PredSet{ℓ₂}(T)}{C : PredSet{ℓ₃}(T)} → (A ≡ B) → (B ≡ C) → (A ≡ C)
  [≡]-transitivity-raw (intro xy) (intro yz) = intro([↔]-transitivity xy yz)

  instance
    [≡]-transitivity : Transitivity(_≡_ {ℓ})
    Transitivity.proof [≡]-transitivity (intro xy) (intro yz) = intro([↔]-transitivity xy yz)

  instance
    [≡]-equivalence : Equivalence(_≡_ {ℓ})
    [≡]-equivalence = intro

  instance
    [≡]-equiv : Equiv(PredSet{ℓ}(T))
    Equiv._≡_ ([≡]-equiv {ℓ}) x y = x ≡ y
    Equiv.equivalence [≡]-equiv = [≡]-equivalence

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  instance
    -- Note: The purpose of this module is to satisfy this property for arbitrary equivalences.
    [∋]-binaryRelator : BinaryRelator(_∋_ {ℓ}{T = T})
    BinaryRelator.substitution [∋]-binaryRelator (intro pₛ) pₑ p = [↔]-to-[→] pₛ(substitute₁(_) pₑ p)

  instance
    [∋]-unaryRelatorₗ : ∀{a : T} → UnaryRelator(A ↦ _∋_ {ℓ} A a)
    [∋]-unaryRelatorₗ = BinaryRelator.left [∋]-binaryRelator

-- TODO: There are level problems here that I am not sure how to solve. The big union of a set of sets are not of the same type as the inner sets. So, for example it would be useful if (⋃ As : PredSet{ℓₒ Lvl.⊔ Lvl.𝐒(ℓ₁)}(T)) and (A : PredSet{ℓ₁}(T)) for (A ∈ As) had the same type/levels when (As : PredSet{Lvl.𝐒(ℓ₁)}(PredSet{ℓ₁}(T))) so that they become comparable. But here, the result of big union is a level greater.
module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  -- ⋃_ : PredSet{Lvl.𝐒(ℓ₁)}(PredSet{ℓ₁}(T)) → PredSet{ℓₒ Lvl.⊔ Lvl.𝐒(ℓ₁)}(T)
  ⋃ : PredSet{ℓ₁}(PredSet{ℓ₂}(T)) → PredSet(T)
  (⋃ As) ∋ x = ∃(A ↦ (A ∈ As) ∧ (x ∈ A))
  UnaryRelator.substitution (preserve-equiv (⋃ As)) xy = [∃]-map-proof (Tuple.mapRight (substitute₁(_) xy))

  ⋂ : PredSet{ℓ₁}(PredSet{ℓ₂}(T)) → PredSet(T)
  (⋂ As) ∋ x = ∀{A} → (A ∈ As) → (x ∈ A)
  UnaryRelator.substitution (preserve-equiv (⋂ As)) xy = substitute₁(_) xy ∘_

-- Indexed set operations.
module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  ⋃ᵢ : ∀{I : Type{ℓ₁}} → (I → PredSet{ℓ₂}(T)) → PredSet{ℓ₁ Lvl.⊔ ℓ₂}(T)
  (⋃ᵢ Ai) ∋ x = ∃(i ↦ x ∈ Ai(i))
  UnaryRelator.substitution (preserve-equiv (⋃ᵢ Ai)) xy = [∃]-map-proof (\{i} → substitute₁(_) ⦃ preserve-equiv(Ai(i)) ⦄ xy)

  ⋂ᵢ : ∀{I : Type{ℓ₁}} → (I → PredSet{ℓ₂}(T)) → PredSet{ℓ₁ Lvl.⊔ ℓ₂}(T)
  (⋂ᵢ Ai) ∋ x = ∀ₗ(i ↦ x ∈ Ai(i))
  UnaryRelator.substitution (preserve-equiv (⋂ᵢ Ai)) xy p {i} = substitute₁(_) ⦃ preserve-equiv(Ai(i)) ⦄ xy p

  -- When the indexed union is indexed by a boolean, it is the same as the small union.
  ⋃ᵢ-of-boolean : ∀{A B : PredSet{ℓ}(T)} → ((⋃ᵢ{I = Bool}(if_then B else A)) ≡ (A ∪ B))
  ∃.witness (_⨯_.left (_≡_.proof ⋃ᵢ-of-boolean) ([∨]-introₗ p)) = 𝐹
  ∃.proof   (_⨯_.left (_≡_.proof ⋃ᵢ-of-boolean) ([∨]-introₗ p)) = p
  ∃.witness (_⨯_.left (_≡_.proof ⋃ᵢ-of-boolean) ([∨]-introᵣ p)) = 𝑇
  ∃.proof   (_⨯_.left (_≡_.proof ⋃ᵢ-of-boolean) ([∨]-introᵣ p)) = p
  _⨯_.right (_≡_.proof ⋃ᵢ-of-boolean) ([∃]-intro 𝐹 ⦃ p ⦄) = [∨]-introₗ p
  _⨯_.right (_≡_.proof ⋃ᵢ-of-boolean) ([∃]-intro 𝑇 ⦃ p ⦄) = [∨]-introᵣ p

  -- When the indexed intersection is indexed by a boolean, it is the same as the small intersection.
  ⋂ᵢ-of-boolean : ∀{A B : PredSet{ℓ}(T)} → ((⋂ᵢ{I = Bool}(if_then B else A)) ≡ (A ∩ B))
  _⨯_.left (_≡_.proof ⋂ᵢ-of-boolean) p {𝐹} = [∧]-elimₗ p
  _⨯_.left (_≡_.proof ⋂ᵢ-of-boolean) p {𝑇} = [∧]-elimᵣ p
  _⨯_.left  (_⨯_.right (_≡_.proof ⋂ᵢ-of-boolean) p) = p{𝐹}
  _⨯_.right (_⨯_.right (_≡_.proof ⋂ᵢ-of-boolean) p) = p{𝑇}

module _
  ⦃ equiv : Equiv{ℓₑ}(T) ⦄
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  where

  ⋃ᵢ-of-bijection : ∀{f : B → PredSet{ℓ}(T)} ⦃ func-f : Function(f)⦄ → (([∃]-intro g) : A ≍ B) → (⋃ᵢ{I = A}(f ∘ g) ≡ ⋃ᵢ{I = B}(f))
  ∃.witness (_⨯_.left (_≡_.proof (⋃ᵢ-of-bijection {f = f} ([∃]-intro g ⦃ bij-g ⦄))) ([∃]-intro b ⦃ p ⦄)) = inv g ⦃ bijective-to-invertible ⦄ (b)
  ∃.proof (_⨯_.left (_≡_.proof (⋃ᵢ-of-bijection {f = f} ([∃]-intro g ⦃ bij-g ⦄))) ([∃]-intro b ⦃ p ⦄)) = substitute₂(_∋_) (symmetry(_≡_) (congruence₁(f) (inverse-right(g)(inv g ⦃ bijective-to-invertible ⦄) ⦃ [∧]-elimᵣ([∃]-proof bijective-to-invertible) ⦄))) (reflexivity(_≡ₑ_)) p
  ∃.witness (_⨯_.right (_≡_.proof (⋃ᵢ-of-bijection {f = f} ([∃]-intro g ⦃ bij-g ⦄))) ([∃]-intro a ⦃ p ⦄)) = g(a)
  ∃.proof (_⨯_.right (_≡_.proof (⋃ᵢ-of-bijection {f = f} ([∃]-intro g ⦃ bij-g ⦄))) ([∃]-intro b ⦃ p ⦄)) = p

  ⋂ᵢ-of-bijection : ∀{f : B → PredSet{ℓ}(T)} ⦃ func-f : Function(f)⦄ → (([∃]-intro g) : A ≍ B) → (⋂ᵢ{I = A}(f ∘ g) ≡ ⋂ᵢ{I = B}(f))
  _⨯_.left (_≡_.proof (⋂ᵢ-of-bijection {f = f} ([∃]-intro g ⦃ bij-g ⦄)) {x}) p {b} = p{g(b)}
  _⨯_.right (_≡_.proof (⋂ᵢ-of-bijection {f = f} ([∃]-intro g ⦃ bij-g ⦄)) {x}) p {b} = substitute₂(_∋_) (congruence₁(f) (inverse-right(g)(inv g ⦃ bijective-to-invertible ⦄) ⦃ [∧]-elimᵣ([∃]-proof bijective-to-invertible) ⦄)) (reflexivity(_≡ₑ_)) (p{inv g ⦃ bijective-to-invertible ⦄ (b)})

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  instance
    singleton-function : ∀{A : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(A) ⦄ → Function{A = A}(•_)
    _≡_.proof (Function.congruence singleton-function {x} {y} xy) {a} = [↔]-intro (_🝖 symmetry(_≡ₑ_) xy) (_🝖 xy)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import MLib.Prelude
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures

module MLib.Matrix.Plus {c ℓ} (struct : Struct bimonoidCode c ℓ) {m n : ℕ} where

open import MLib.Matrix.Core
open import MLib.Matrix.Equality struct

open FunctionProperties

-- Pointwise addition --

infixl 6 _⊕_

_⊕_ : Matrix S m n → Matrix S m n → Matrix S m n
(A ⊕ B) i j = A i j ⟨ + ⟩ B i j

⊕-cong : Congruent₂ _⊕_
⊕-cong p q = λ i j → S.cong + (p i j) (q i j)

⊕-assoc : ⦃ props : Has₁ (associative on +) ⦄ → Associative _⊕_
⊕-assoc ⦃ props ⦄ A B C i j = from props (associative on +) (A i j) (B i j) (C i j)

0● : Matrix S m n
0● _ _ = ⟦ 0# ⟧

⊕-identityˡ : ⦃ props : Has₁ (0# is leftIdentity for +) ⦄ → LeftIdentity 0● _⊕_
⊕-identityˡ ⦃ props ⦄ A i j = from props (0# is leftIdentity for +) (A i j)

⊕-identityʳ : ⦃ props : Has₁ (0# is rightIdentity for +) ⦄ → RightIdentity 0● _⊕_
⊕-identityʳ ⦃ props ⦄ A i j = from props (0# is rightIdentity for +) (A i j)

⊕-comm : ⦃ props : Has₁ (commutative on +) ⦄ → Commutative _⊕_
⊕-comm ⦃ props ⦄ A B i j = from props (commutative on +) (A i j) (B i j)


text:
{-

    Practical Relational Algebra
            Toon Nolten
              based on
          The Power Of Pi

-}
module relational-algebra where

open import Data.Empty
open import Data.Unit hiding (_≤_)
open import Data.Bool
open import Data.Nat
open import Data.Integer hiding (show)
open import Data.List
open import Data.Char hiding (_==_) renaming (show to charToString)
open import Data.Vec hiding (_++_; lookup; map; foldr; _>>=_)
open import Data.String using (String; toVec; _==_; strictTotalOrder)
                        renaming (_++_ to _∥_)
open import Data.Product using (_×_; _,_; proj₁)
open import Coinduction
open import IO

open import Relation.Binary
open StrictTotalOrder Data.String.strictTotalOrder renaming (compare to str_cmp)

data Order : Set where
  LT EQ GT : Order

module InsertionSort where
  insert : {A : Set} → (A → A → Order) → A → List A → List A
  insert _   e []       = e ∷ []
  insert cmp e (l ∷ ls) with cmp e l
  ... | GT = l ∷ insert cmp e ls
  ... | _  = e ∷ l ∷ ls

  sort : {A : Set} → (A → A → Order) → List A → List A
  sort cmp = foldr (insert cmp) []
open InsertionSort using (insert; sort)

-- Universe U exists of type U and el : U → Set
data U : Set where
  CHAR NAT BOOL : U
  VEC  : U → ℕ → U

el : U → Set
el CHAR      = Char
el NAT       = ℕ
el (VEC u n) = Vec (el u) n
el BOOL      = Bool

parens : String → String
parens str = "(" ∥ str ∥ ")"

show : {u : U} → el u → String
show {CHAR         } c        = charToString c
show {NAT          } zero     = "Zero"
show {NAT          } (suc k)  = "Succ " ∥ parens (show k)
show {VEC u zero   } Nil      = "Nil"
show {VEC u (suc k)} (x ∷ xs) = parens (show x) ∥ " ∷ " ∥ parens (show xs)
show {BOOL         } true     = "True"
show {BOOL         } false    = "False"

_=ᴺ_ : ℕ → ℕ → Bool
zero  =ᴺ zero  = true
suc m =ᴺ suc n = (m =ᴺ n)
_     =ᴺ _     = false

_≤ᴺ_ : ℕ → ℕ → Order
zero  ≤ᴺ zero  = EQ
zero  ≤ᴺ _     = LT
_     ≤ᴺ zero  = GT
suc a ≤ᴺ suc b = a ≤ᴺ b

_=ᵁ_ : U → U → Bool
CHAR    =ᵁ CHAR      = true
NAT     =ᵁ NAT       = true
BOOL    =ᵁ BOOL      = true
VEC u x =ᵁ VEC u' x' = (u =ᵁ u') ∧ (x =ᴺ x')
_       =ᵁ _         = false

_≤ᵁ_ : U → U → Order
CHAR ≤ᵁ CHAR = EQ
CHAR ≤ᵁ _ = LT
_ ≤ᵁ CHAR = GT
NAT ≤ᵁ NAT = EQ
NAT ≤ᵁ _ = LT
_ ≤ᵁ NAT = GT
BOOL ≤ᵁ BOOL = EQ
BOOL ≤ᵁ _ = LT
_ ≤ᵁ BOOL = GT
VEC a x ≤ᵁ VEC b y with a ≤ᵁ b
... | LT = LT
... | EQ = x ≤ᴺ y
... | GT = GT

So : Bool → Set
So true  = ⊤
So false = ⊥

data SqlValue : Set where
  SqlString  : String → SqlValue
  SqlChar    : Char   → SqlValue
  SqlBool    : Bool   → SqlValue
  SqlInteger : ℤ      → SqlValue
--{-# COMPILED_DATA SqlValue SqlValue SqlString SqlChar SqlBool SqlInteger #-}

module OrderedSchema where
  SchemaDescription = List (List SqlValue)

  Attribute : Set
  Attribute = String × U

  -- Compare on type if names are equal.
  -- SQL DB's probably don't allow columns with the same name
  -- but nothing prevents us from writing a Schema that does,
  -- this is necessary to make our sort return a unique answer.
  attr_cmp : Attribute → Attribute → Order
  attr_cmp (nm₁ , U₁) (nm₂ , U₂) with str_cmp nm₁ nm₂ | U₁ ≤ᵁ U₂
  ... | tri< _ _ _ | _     = LT
  ... | tri≈ _ _ _ | U₁≤U₂ = U₁≤U₂
  ... | tri> _ _ _ | _     = GT

  data Schema : Set where
    sorted : List Attribute → Schema

  mkSchema : List Attribute → Schema
  mkSchema xs = sorted (sort attr_cmp xs)

  expandSchema : Attribute → Schema → Schema
  expandSchema x (sorted xs) = sorted (insert attr_cmp x xs)

  schemify : SchemaDescription → Schema
  schemify sdesc = {!!}

  disjoint : Schema → Schema → Bool
  disjoint (sorted []      ) (_              ) = true
  disjoint (_              ) (sorted []      ) = true
  disjoint (sorted (x ∷ xs)) (sorted (y ∷ ys)) with attr_cmp x y
  ... | LT = disjoint (sorted xs      ) (sorted (y ∷ ys))
  ... | EQ = false
  ... | GT = disjoint (sorted (x ∷ xs)) (sorted ys      )

  sub : Schema → Schema → Bool
  sub (sorted []      ) (_              ) = true
  sub (sorted (x ∷ _) ) (sorted []      ) = false
  sub (sorted (x ∷ xs)) (sorted (X ∷ Xs)) with attr_cmp x X
  ... | LT = false
  ... | EQ = sub (sorted xs      ) (sorted Xs)
  ... | GT = sub (sorted (x ∷ xs)) (sorted Xs)

  same' : List Attribute → List Attribute → Bool
  same' ([]              ) ([]              ) = true
  same' ((nm₁ , ty₁) ∷ xs) ((nm₂ , ty₂) ∷ ys) =
    (nm₁ == nm₂) ∧ (ty₁ =ᵁ ty₂) ∧ same' xs ys
  same' (_               ) (_               ) = false

  same : Schema → Schema → Bool
  same (sorted xs) (sorted ys) = same' xs ys

  occurs : String → Schema → Bool
  occurs nm (sorted s) = any (_==_ nm) (map (proj₁) s)

  lookup' : (nm : String) → (s : List Attribute)
              → So (occurs nm (sorted s)) → U
  lookup' _  []                   ()
  lookup' nm ((name , type) ∷ s') p with nm == name
  ... | true  = type
  ... | false = lookup' nm s' p

  lookup : (nm : String) → (s : Schema) → So (occurs nm s) → U
  lookup nm (sorted s) = lookup' nm s

  append : (s s' : Schema) → Schema
  append (sorted s) (sorted s') = mkSchema (s ++ s')
open OrderedSchema using (Schema; mkSchema; expandSchema; schemify;
                          disjoint; sub; same; occurs; lookup;
                          append)

data Row : Schema → Set where
  EmptyRow : Row (mkSchema [])
  ConsRow  : ∀ {name u s} → el u → Row s → Row (expandSchema (name , u) s)

Table : Schema → Set
Table s = List (Row s)

DatabasePath = String
TableName    = String

postulate
  Connection : Set
  connectSqlite3 : DatabasePath → IO Connection
  describe_table : TableName → Connection → IO (List (List SqlValue))
-- {-# COMPILED_TYPE Connection Connection #-}
-- {-# COMPILED connectSqlite3 connectSqlite3 #-}
-- {-# COMPILED describe_table describe_table #-}

data Handle : Schema → Set where
  conn : Connection → (s : Schema) → Handle s

-- Connect currently ignores differences between
-- the expected schema and the actual schema.
-- According to tpop this should result in
-- "a *runtime exception* in the *IO* monad."
-- Agda does not have exceptions(?)
--  -> postulate error with a compiled pragma?
connect : DatabasePath → TableName → (s : Schema) → IO (Handle s)
connect DB table schema_expect =
  ♯ (connectSqlite3 DB) >>=
    (λ sqlite_conn →
      ♯ (♯ (describe_table table sqlite_conn) >>=
      (λ description →
        ♯ (♯ (return (schemify description)) >>=
        (λ schema_actual →
          ♯ (♯ (return (same schema_expect schema_actual)) >>=
          (λ { true  → ♯ (return (conn sqlite_conn schema_expect));
               false → ♯ (return (conn sqlite_conn schema_expect)) })))))))

data Expr : Schema → U → Set where
  equal    : ∀ {u s} → Expr s u → Expr s u → Expr s BOOL
  lessThan : ∀ {u s} → Expr s u → Expr s u → Expr s BOOL
  _!_      : (s : Schema) → (nm : String) → {p : So (occurs nm s)}
               → Expr s (lookup nm s p)

data RA : Schema → Set where
  Read    : ∀ {s} → Handle s → RA s
  Union   : ∀ {s} → RA s → RA s → RA s
  Diff    : ∀ {s} → RA s → RA s → RA s
  Product : ∀ {s s'} → {_ : So (disjoint s s')} → RA s → RA s'
              → RA (append s s')
  Project : ∀ {s} → (s' : Schema) → {_ : So (sub s' s)} → RA s → RA s'
  Select  : ∀ {s} → Expr s BOOL → RA s → RA s
  -- ...
{-
  As we mentioned previously, we have taken a very minimal set of relational
  algebra operators. It should be fairly straightforward to add operators
  for the many other operators in relational algebra, such as the

  natural join, θ-join, equijoin, renaming, or division,

  using the same techniques. Alternatively, you can define many of these
  operations in terms of the operations we have implemented in the RA data type.
-}

-- We could:
postulate
  toSQL : ∀ {s} → RA s → String

-- We can do much better:
postulate
  query : {s : Schema} → RA s → IO (List (Row s))
{-
  The *query* function uses *toSQL* to produce a query, and passes this to the
  database server. When the server replies, however, we know exactly how to
  parse the response: we know the schema of the table resulting from our query,
  and can use this to parse the database server's response in a type-safe
  manner. The type checker can then statically check that the program uses the
  returned list in a way consistent with its type.
-}

Cars : Schema
Cars = mkSchema (("Model" , VEC CHAR 20) ∷ ("Time" , VEC CHAR 6)
                 ∷ ("Wet" , BOOL) ∷ [])

zonda : Row Cars
zonda = ConsRow (toVec "Pagani Zonda C12 F  ")
        (ConsRow (toVec "1:18.4")
        (ConsRow false EmptyRow))

Models : Schema
Models = mkSchema (("Model" , VEC CHAR 20) ∷ [])

models : Handle Cars → RA Models
models h = Project Models (Read h)

wet : Handle Cars → RA Models
wet h = Project Models (Select (Cars ! "Wet") (Read h))

{- Discussion
   ==========

   There are many, many aspects of this proposal that can be improved. Some
   attributes of a schema contain *NULL*-values; we should close our universe
   under *Maybe* accordingly. Some database servers silently truncate strings
   longer than 255 characters. We would do well to ensure statically that this
   never happens. Our goal, however, was not to provide a complete model of all
   of SQL's quirks and idiosyncrasies: we want to show how a language with
   dependent types can schine where Haskell struggles.
     Our choice of *Schema* data type suffers from the usual disadvantages of
   using a list to represent a set: our *Schema* data type may contain
   duplicates and the order of the elements matters. The first problem is easy
   to solve. Using an implicit proof argument in the *Cons* case, we can define
   a data type for lists that do not contain duplicates. The type of *Cons* then
   becomes:
     Cons : (nm : String) → (u : U) → (s : Schema) → {_ : So (not (elem nm s))}
                → Schema
   The second point is a bit trickier. The real solution would involve quotient
   types to make the order of the elements unobservable. As Agda does not
   support quotient types, however, the best we can do is parameterise our
   constructors by an additional proof argument, when necessary. For example,
   the *Union* constructor could be defined as follows:
     Union : ∀ {s s'} → {_ : So (permute s s')} → RA s → RA s' → RA s
   Instead of requiring that both arguments of *Union* are indexed by the same
   schema, we should only require that the two schemas are equal up to a
   permutation of the elements. Alternatively, we could represent the *Schema*
   using a data structure that fixes the order in which its constituent
   elements occur, such as a trie or sorted list.
     Finally, we would like to return to our example table. We chose to model
   the lap time as a fixed-length string ─ clearly, a triple of integers would
   be a better representation. Unfortunately, most database servers only
   support a handful of built-in types, such as strings, numbers, bits. There
   is no way to extend these primitive types. This problem is sometimes
   referred to as the *object-relational impedance mismatch*. We believe the
   generic programming techniques and views from the previous sections can be
   used to marshall data between a low-level representation in the database
   and the high-level representation in our programming language.
-}

max_stars_repo_name: toonn/agda-casestt

max_issues_repo_name: toonn/agda-casestt

max_forks_repo_name: toonn/agda-casestt


text:
{-# OPTIONS --without-K --safe #-}

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U
open import Definition.Typed
open import Definition.Typed.Weakening
open import Agda.Primitive

open import Tools.Product
open import Tools.Embedding
import Tools.PropositionalEquality as PE

-- The different cases of the logical relation are spread out through out
-- this file. This is due to them having different dependencies.

-- We will refer to expressions that satisfies the logical relation as reducible.

-- Reducibility of Neutrals:

-- Neutral type
record _⊩ne_ (Γ : Con Term) (A : Term) : Set where
  constructor ne
  field
    K   : Term
    D   : Γ ⊢ A :⇒*: K
    neK : Neutral K
    K≡K : Γ ⊢ K ~ K ∷ U

-- Neutral type equality
record _⊩ne_≡_/_ (Γ : Con Term) (A B : Term) ([A] : Γ ⊩ne A) : Set where
  constructor ne₌
  open _⊩ne_ [A]
  field
    M   : Term
    D′  : Γ ⊢ B :⇒*: M
    neM : Neutral M
    K≡M : Γ ⊢ K ~ M ∷ U

-- Neutral term in WHNF
record _⊩neNf_∷_ (Γ : Con Term) (k A : Term) : Set where
  inductive
  constructor neNfₜ
  field
    neK  : Neutral k
    ⊢k   : Γ ⊢ k ∷ A
    k≡k  : Γ ⊢ k ~ k ∷ A

-- Neutral term
record _⊩ne_∷_/_ (Γ : Con Term) (t A : Term) ([A] : Γ ⊩ne A) : Set where
  inductive
  constructor neₜ
  open _⊩ne_ [A]
  field
    k   : Term
    d   : Γ ⊢ t :⇒*: k ∷ K
    nf  : Γ ⊩neNf k ∷ K

-- Neutral term equality in WHNF
record _⊩neNf_≡_∷_ (Γ : Con Term) (k m A : Term) : Set where
  inductive
  constructor neNfₜ₌
  field
    neK  : Neutral k
    neM  : Neutral m
    k≡m  : Γ ⊢ k ~ m ∷ A

-- Neutral term equality
record _⊩ne_≡_∷_/_ (Γ : Con Term) (t u A : Term) ([A] : Γ ⊩ne A) : Set where
  constructor neₜ₌
  open _⊩ne_ [A]
  field
    k m : Term
    d   : Γ ⊢ t :⇒*: k ∷ K
    d′  : Γ ⊢ u :⇒*: m ∷ K
    nf  : Γ ⊩neNf k ≡ m ∷ K

-- Reducibility of natural numbers:

-- Natural number type
_⊩ℕ_ : (Γ : Con Term) (A : Term) → Set
Γ ⊩ℕ A = Γ ⊢ A :⇒*: ℕ

-- Natural number type equality
data _⊩ℕ_≡_ (Γ : Con Term) (A B : Term) : Set where
  ℕ₌ : Γ ⊢ B ⇒* ℕ → Γ ⊩ℕ A ≡ B

mutual
  -- Natural number term
  data _⊩ℕ_∷ℕ (Γ : Con Term) (t : Term) : Set where
    ℕₜ : (n : Term) (d : Γ ⊢ t :⇒*: n ∷ ℕ) (n≡n : Γ ⊢ n ≅ n ∷ ℕ)
         (prop : Natural-prop Γ n)
       → Γ ⊩ℕ t ∷ℕ

  -- WHNF property of natural number terms
  data Natural-prop (Γ : Con Term) : (n : Term) → Set where
    sucᵣ  : ∀ {n} → Γ ⊩ℕ n ∷ℕ → Natural-prop Γ (suc n)
    zeroᵣ : Natural-prop Γ zero
    ne    : ∀ {n} → Γ ⊩neNf n ∷ ℕ → Natural-prop Γ n

mutual
  -- Natural number term equality
  data _⊩ℕ_≡_∷ℕ (Γ : Con Term) (t u : Term) : Set where
    ℕₜ₌ : (k k′ : Term) (d : Γ ⊢ t :⇒*: k  ∷ ℕ) (d′ : Γ ⊢ u :⇒*: k′ ∷ ℕ)
          (k≡k′ : Γ ⊢ k ≅ k′ ∷ ℕ)
          (prop : [Natural]-prop Γ k k′) → Γ ⊩ℕ t ≡ u ∷ℕ

  -- WHNF property of Natural number term equality
  data [Natural]-prop (Γ : Con Term) : (n n′ : Term) → Set where
    sucᵣ  : ∀ {n n′} → Γ ⊩ℕ n ≡ n′ ∷ℕ → [Natural]-prop Γ (suc n) (suc n′)
    zeroᵣ : [Natural]-prop Γ zero zero
    ne    : ∀ {n n′} → Γ ⊩neNf n ≡ n′ ∷ ℕ → [Natural]-prop Γ n n′

-- Natural extraction from term WHNF property
natural : ∀ {Γ n} → Natural-prop Γ n → Natural n
natural (sucᵣ x) = sucₙ
natural zeroᵣ = zeroₙ
natural (ne (neNfₜ neK ⊢k k≡k)) = ne neK

-- Natural extraction from term equality WHNF property
split : ∀ {Γ a b} → [Natural]-prop Γ a b → Natural a × Natural b
split (sucᵣ x) = sucₙ , sucₙ
split zeroᵣ = zeroₙ , zeroₙ
split (ne (neNfₜ₌ neK neM k≡m)) = ne neK , ne neM

-- Type levels

data TypeLevel : Set where
  ⁰ : TypeLevel
  ¹ : TypeLevel

data _<_ : (i j : TypeLevel) → Set where
  0<1 : ⁰ < ¹

toLevel : TypeLevel → Level
toLevel ⁰ = lzero
toLevel ¹ = lsuc lzero

-- Logical relation

record LogRelKit (ℓ : Level) : Set (lsuc (lsuc ℓ)) where
  constructor Kit
  field
    _⊩U : (Γ : Con Term) → Set (lsuc ℓ)
    _⊩Π_ : (Γ : Con Term) → Term → Set (lsuc ℓ)

    _⊩_ : (Γ : Con Term) → Term → Set (lsuc ℓ)
    _⊩_≡_/_ : (Γ : Con Term) (A B : Term) → Γ ⊩ A → Set ℓ
    _⊩_∷_/_ : (Γ : Con Term) (t A : Term) → Γ ⊩ A → Set ℓ
    _⊩_≡_∷_/_ : (Γ : Con Term) (t u A : Term) → Γ ⊩ A → Set ℓ

module LogRel (l : TypeLevel) (rec : ∀ {l′} → l′ < l → LogRelKit (toLevel l)) where

  record _⊩¹U (Γ : Con Term) : Set (lsuc (lsuc (toLevel l))) where
    constructor Uᵣ
    field
      l′ : TypeLevel
      l< : l′ < l
      ⊢Γ : ⊢ Γ

  -- Universe type equality
  record _⊩¹U≡_ (Γ : Con Term) (B : Term) : Set (lsuc (toLevel l)) where
    constructor U₌
    field
      B≡U : B PE.≡ U

  -- Universe term
  record _⊩¹U_∷U/_ {l′} (Γ : Con Term) (t : Term) (l< : l′ < l) : Set (lsuc (toLevel l)) where
    constructor Uₜ
    open LogRelKit (rec l<)
    field
      A     : Term
      d     : Γ ⊢ t :⇒*: A ∷ U
      typeA : Type A
      A≡A   : Γ ⊢ A ≅ A ∷ U
      [t]   : Γ ⊩ t

  -- Universe term equality
  record _⊩¹U_≡_∷U/_ {l′} (Γ : Con Term) (t u : Term) (l< : l′ < l) : Set (lsuc (toLevel l)) where
    constructor Uₜ₌
    open LogRelKit (rec l<)
    field
      A B   : Term
      d     : Γ ⊢ t :⇒*: A ∷ U
      d′    : Γ ⊢ u :⇒*: B ∷ U
      typeA : Type A
      typeB : Type B
      A≡B   : Γ ⊢ A ≅ B ∷ U
      [t]   : Γ ⊩ t
      [u]   : Γ ⊩ u
      [t≡u] : Γ ⊩ t ≡ u / [t]

  RedRel : Set (lsuc (lsuc (lsuc (toLevel l))))
  RedRel = Con Term → Term → (Term → Set (lsuc (toLevel l))) → (Term → Set (lsuc (toLevel l))) → (Term → Term → Set (lsuc (toLevel l))) → Set (lsuc (lsuc (toLevel l)))

  record _⊩⁰_/_ (Γ : Con Term) (A : Term) (_⊩_▸_▸_▸_ : RedRel) : Set (lsuc (lsuc (toLevel l))) where
    inductive
    eta-equality
    constructor LRPack
    field
      ⊩Eq : Term → Set (lsuc (toLevel l))
      ⊩Term : Term → Set (lsuc (toLevel l))
      ⊩EqTerm : Term → Term → Set (lsuc (toLevel l))
      ⊩LR : Γ ⊩ A ▸ ⊩Eq ▸ ⊩Term ▸ ⊩EqTerm

  _⊩⁰_≡_/_ : {R : RedRel} (Γ : Con Term) (A B : Term) → Γ ⊩⁰ A / R → Set (lsuc (toLevel l))
  Γ ⊩⁰ A ≡ B / LRPack ⊩Eq ⊩Term ⊩EqTerm ⊩Red = ⊩Eq B

  _⊩⁰_∷_/_ : {R : RedRel} (Γ : Con Term) (t A : Term) → Γ ⊩⁰ A / R → Set (lsuc (toLevel l))
  Γ ⊩⁰ t ∷ A / LRPack ⊩Eq ⊩Term ⊩EqTerm ⊩Red = ⊩Term t

  _⊩⁰_≡_∷_/_ : {R : RedRel} (Γ : Con Term) (t u A : Term) → Γ ⊩⁰ A / R → Set (lsuc (toLevel l))
  Γ ⊩⁰ t ≡ u ∷ A / LRPack ⊩Eq ⊩Term ⊩EqTerm ⊩Red = ⊩EqTerm t u

  record _⊩¹Π_/_ (Γ : Con Term) (A : Term) (R : RedRel) : Set (lsuc (lsuc (toLevel l))) where
    inductive
    eta-equality
    constructor Πᵣ
    field
      F : Term
      G : Term
      D : Γ ⊢ A :⇒*: Π F ▹ G
      ⊢F : Γ ⊢ F
      ⊢G : Γ ∙ F ⊢ G
      A≡A : Γ ⊢ Π F ▹ G ≅ Π F ▹ G
      [F] : ∀ {ρ Δ} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ) → Δ ⊩⁰ U.wk ρ F / R
      [G] : ∀ {ρ Δ a}
          → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          → Δ ⊩⁰ a ∷ U.wk ρ F / [F] [ρ] ⊢Δ
          → Δ ⊩⁰ U.wk (lift ρ) G [ a ] / R
      G-ext : ∀ {ρ Δ a b}
            → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
            → ([a] : Δ ⊩⁰ a ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
            → ([b] : Δ ⊩⁰ b ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
            → Δ ⊩⁰ a ≡ b ∷ U.wk ρ F / [F] [ρ] ⊢Δ
            → Δ ⊩⁰ U.wk (lift ρ) G [ a ] ≡ U.wk (lift ρ) G [ b ] / [G] [ρ] ⊢Δ [a]

  record _⊩¹Π_≡_/_ {R : RedRel} (Γ : Con Term) (A B : Term) ([A] : Γ ⊩¹Π A / R) : Set (lsuc (toLevel l)) where
    inductive
    eta-equality
    constructor Π₌
    open _⊩¹Π_/_ [A]
    field
      F′     : Term
      G′     : Term
      D′     : Γ ⊢ B ⇒* Π F′ ▹ G′
      A≡B    : Γ ⊢ Π F ▹ G ≅ Π F′ ▹ G′
      [F≡F′] : ∀ {ρ Δ}
             → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
             → Δ ⊩⁰ U.wk ρ F ≡ U.wk ρ F′ / [F] [ρ] ⊢Δ
      [G≡G′] : ∀ {ρ Δ a}
             → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
             → ([a] : Δ ⊩⁰ a ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
             → Δ ⊩⁰ U.wk (lift ρ) G [ a ] ≡ U.wk (lift ρ) G′ [ a ] / [G] [ρ] ⊢Δ [a]

  -- Term of Π-type
  _⊩¹Π_∷_/_ : {R : RedRel} (Γ : Con Term) (t A : Term) ([A] : Γ ⊩¹Π A / R) → Set (lsuc (toLevel l))
  Γ ⊩¹Π t ∷ A / Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext =
    ∃ λ f → Γ ⊢ t :⇒*: f ∷ Π F ▹ G
          × Function f
          × Γ ⊢ f ≅ f ∷ Π F ▹ G
          × (∀ {ρ Δ a b}
            → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
              ([a] : Δ ⊩⁰ a ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
              ([b] : Δ ⊩⁰ b ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
              ([a≡b] : Δ ⊩⁰ a ≡ b ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
            → Δ ⊩⁰ U.wk ρ f ∘ a ≡ U.wk ρ f ∘ b ∷ U.wk (lift ρ) G [ a ] / [G] [ρ] ⊢Δ [a])
          × (∀ {ρ Δ a} → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
            → ([a] : Δ ⊩⁰ a ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
            → Δ ⊩⁰ U.wk ρ f ∘ a ∷ U.wk (lift ρ) G [ a ] / [G] [ρ] ⊢Δ [a])
  -- Issue: Agda complains about record use not being strictly positive.
  --        Therefore we have to use ×

  -- Term equality of Π-type
  _⊩¹Π_≡_∷_/_ : {R : RedRel} (Γ : Con Term) (t u A : Term) ([A] : Γ ⊩¹Π A / R) → Set (lsuc (toLevel l))
  Γ ⊩¹Π t ≡ u ∷ A / Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext =
    let [A] = Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext
    in  ∃₂ λ f g →
        Γ ⊢ t :⇒*: f ∷ Π F ▹ G
    ×   Γ ⊢ u :⇒*: g ∷ Π F ▹ G
    ×   Function f
    ×   Function g
    ×   Γ ⊢ f ≅ g ∷ Π F ▹ G
    ×   Γ ⊩¹Π t ∷ A / [A]
    ×   Γ ⊩¹Π u ∷ A / [A]
    ×   (∀ {ρ Δ a} → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
        → ([a] : Δ ⊩⁰ a ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
        → Δ ⊩⁰ U.wk ρ f ∘ a ≡ U.wk ρ g ∘ a ∷ U.wk (lift ρ) G [ a ] / [G] [ρ] ⊢Δ [a])
  -- Issue: Same as above.

  -- Logical relation definition
  data _⊩LR_▸_▸_▸_ : RedRel where
    LRU : ∀ {Γ} (⊢Γ : ⊢ Γ) → (l' : TypeLevel) → (l< : l' < l) → Γ ⊩LR U
      ▸ (λ B → Γ ⊩¹U≡ B)
      ▸ (λ t → Γ ⊩¹U t ∷U/ l<)
      ▸ (λ t u → Γ ⊩¹U t ≡ u ∷U/ l<)
    LRℕ : ∀ {Γ A} → Γ ⊩ℕ A → Γ ⊩LR A
      ▸ (λ B → ι′ (Γ ⊩ℕ A ≡ B))
      ▸ (λ t → ι′ (Γ ⊩ℕ t ∷ℕ))
      ▸ (λ t u → ι′ (Γ ⊩ℕ t ≡ u ∷ℕ))
    LRne : ∀ {Γ A} → (neA : Γ ⊩ne A) → Γ ⊩LR A
      ▸ (λ B → ι′ (Γ ⊩ne A ≡ B / neA))
      ▸ (λ t → ι′ (Γ ⊩ne t ∷ A / neA))
      ▸ (λ t u → ι′ (Γ ⊩ne t ≡ u ∷ A / neA))
    LRΠ : ∀ {Γ A} → (ΠA : Γ ⊩¹Π A / _⊩LR_▸_▸_▸_) → Γ ⊩LR A
      ▸ (λ B → Γ ⊩¹Π A ≡ B / ΠA)
      ▸ (λ t → Γ ⊩¹Π t ∷ A / ΠA)
      ▸ (λ t u → Γ ⊩¹Π t ≡ u ∷ A / ΠA)
    LRemb : ∀ {Γ A l′} (l< : l′ < l) (let open LogRelKit (rec l<)) ([A] : Γ ⊩ A) → Γ ⊩LR A
      ▸ (λ B → ι (Γ ⊩ A ≡ B / [A]))
      ▸ (λ t → ι (Γ ⊩ t ∷ A / [A]))
      ▸ (λ t u → ι (Γ ⊩ t ≡ u ∷ A / [A]))

  _⊩¹_ : (Γ : Con Term) → (A : Term) → Set (lsuc (lsuc (toLevel l)))
  Γ ⊩¹ A = Γ ⊩⁰ A / _⊩LR_▸_▸_▸_

  _⊩¹_≡_/_ : (Γ : Con Term) (A B : Term) → Γ ⊩¹ A → Set (lsuc (toLevel l))
  Γ ⊩¹ A ≡ B / [A] = Γ ⊩⁰ A ≡ B / [A]

  _⊩¹_∷_/_ : (Γ : Con Term) (t A : Term) → Γ ⊩¹ A → Set (lsuc (toLevel l))
  Γ ⊩¹ t ∷ A / [A] = Γ ⊩⁰ t ∷ A / [A]

  _⊩¹_≡_∷_/_ : (Γ : Con Term) (t u A : Term) → Γ ⊩¹ A → Set (lsuc (toLevel l))
  Γ ⊩¹ t ≡ u ∷ A / [A] = Γ ⊩⁰ t ≡ u ∷ A / [A]

open LogRel public using (Uᵣ; Πᵣ; Π₌; U₌ ; Uₜ; Uₜ₌ ; LRU ; LRℕ ; LRne ; LRΠ ; LRemb ; LRPack)

pattern Πₜ f d funcF f≡f [f] [f]₁ = f , d , funcF , f≡f , [f] , [f]₁
pattern Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g] = f , g , d , d′ , funcF , funcG , f≡g , [f] , [g] , [f≡g]
pattern ℕᵣ a = LRPack _ _ _ (LRℕ a)
pattern emb′ a b = LRPack _ _ _ (LRemb a b)
pattern Uᵣ′ a b c = LRPack _ _ _ (LRU c a b)
pattern ne′ a b c d = LRPack _ _ _ (LRne (ne a b c d))
pattern Πᵣ′ a b c d e f g h i = LRPack _ _ _ (LRΠ (Πᵣ a b c d e f g h i))

kit₀ : LogRelKit (lsuc (lzero))
kit₀ = Kit _⊩¹U (λ Γ A → Γ ⊩¹Π A / _⊩LR_▸_▸_▸_) _⊩¹_ _⊩¹_≡_/_ _⊩¹_∷_/_ _⊩¹_≡_∷_/_ where open LogRel ⁰ (λ ())

logRelRec : ∀ l {l′} → l′ < l → LogRelKit (toLevel l)
logRelRec ⁰ = λ ()
logRelRec ¹ 0<1 = kit₀

kit : ∀ (l : TypeLevel) → LogRelKit (lsuc (toLevel l))
kit l = Kit _⊩¹U (λ Γ A → Γ ⊩¹Π A / _⊩LR_▸_▸_▸_) _⊩¹_ _⊩¹_≡_/_ _⊩¹_∷_/_ _⊩¹_≡_∷_/_ where open LogRel l (logRelRec l)

-- a bit of repetition in "kit ¹" definition, would work better with Fin 2 for
-- TypeLevel because you could recurse.

record _⊩′⟨_⟩U (Γ : Con Term) (l : TypeLevel) : Set where
  constructor Uᵣ
  field
    l′ : TypeLevel
    l< : l′ < l
    ⊢Γ : ⊢ Γ

_⊩′⟨_⟩Π_ : (Γ : Con Term) (l : TypeLevel) → Term → Set (lsuc (lsuc (toLevel l)))
Γ ⊩′⟨ l ⟩Π A = Γ ⊩Π A where open LogRelKit (kit l)

_⊩⟨_⟩_ : (Γ : Con Term) (l : TypeLevel) → Term → Set (lsuc (lsuc (toLevel l)))
Γ ⊩⟨ l ⟩ A = Γ ⊩ A where open LogRelKit (kit l)

_⊩⟨_⟩_≡_/_ : (Γ : Con Term) (l : TypeLevel) (A B : Term) → Γ ⊩⟨ l ⟩ A → Set (lsuc (toLevel l))
Γ ⊩⟨ l ⟩ A ≡ B / [A] = Γ ⊩ A ≡ B / [A] where open LogRelKit (kit l)

_⊩⟨_⟩_∷_/_ : (Γ : Con Term) (l : TypeLevel) (t A : Term) → Γ ⊩⟨ l ⟩ A → Set (lsuc (toLevel l))
Γ ⊩⟨ l ⟩ t ∷ A / [A] = Γ ⊩ t ∷ A / [A] where open LogRelKit (kit l)

_⊩⟨_⟩_≡_∷_/_ : (Γ : Con Term) (l : TypeLevel) (t u A : Term) → Γ ⊩⟨ l ⟩ A → Set (lsuc (toLevel l))
Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A] = Γ ⊩ t ≡ u ∷ A / [A] where open LogRelKit (kit l)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
{-# OPTIONS --verbose=10 #-}

module leafsF where

  open import Data.Nat
  open import Data.Vec
  open import Agda.Builtin.Sigma
  open import Data.Product
  open import Data.Fin using (fromℕ)

  open import trees
  open import optics
  open import lemmas

  leafsTreeF : {A : Set} -> (t : Tree A) -> Vec A (#leafs t) × (Vec A (#leafs t) -> Tree A)
  leafsTreeF empty = ([] , λ _ -> empty)
  -- leafsTreeF (node empty root empty) = (root ∷ [] , λ { (hd ∷ []) -> node empty hd empty })
  leafsTreeF {A} (node t₁ x t₂) with t₁ | t₂
  ...                              | empty | empty = (x ∷ [] , λ { (hd ∷ []) -> node empty hd empty })
  leafsTreeF _ | node t11 x1 t12 | t2 with leafsTreeF (node t11 x1 t12) | leafsTreeF t2
  ...                                                  | (g₁ , p₁)     | (g₂ , p₂) =
      -- (g₁ ++ g₂ , λ v -> node (p₁ (take n₁ v)) x (p₂ (drop n₁ v)))
      ({!!} , λ v -> node (p₁ {!!}) x1 (p₂ {!!}))
      where
        n₁ = #leafs (node t11 x1 t12)
        n₂ = #leafs t2
  leafsTreeF (node t₁ x t₂)                   | _ | (node _ _ _) with leafsTreeF t₁ | leafsTreeF t₂
  ...                                                    | (g₁ , p₁)     | (g₂ , p₂) =
      -- (g₁ ++ g₂ , λ v -> node (p₁ (take n₁ v)) x (p₂ (drop n₁ v)))
      ({!!} , λ v -> node (p₁ {!!}) x (p₂ {!!}))
      where
        n₁ = #leafs t₁
        n₂ = #leafs t₂

  module tests where
    tree1 : Tree ℕ
    tree1 = node (node empty 1 empty) 3 empty

    open Traversal

max_stars_repo_name: hablapps/safeoptics

max_issues_repo_name: hablapps/safeoptics

max_forks_repo_name: hablapps/safeoptics


text:
{-# OPTIONS --no-sized-types #-}

postulate
  Size : Set
  _^   : Size -> Size
  ∞    : Size

{-# BUILTIN SIZE Size  #-}
{-# BUILTIN SIZESUC _^ #-}
{-# BUILTIN SIZEINF ∞  #-}

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {size ^}
  suc  : {size : Size} -> Nat {size} -> Nat {size ^}

weak : {i : Size} -> Nat {i} -> Nat {∞}
weak x = x

-- Should give error without sized types.

-- .i != ∞ of type Size
-- when checking that the expression x has type Nat

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cubical #-}

module Properties where

open import Data.Fin renaming (zero to Fzero; suc to Fsuc) hiding (_+_; _≟_)
open import Data.Nat
open import Data.Nat.DivMod using (_mod_; _div_; m≡m%n+[m/n]*n)
open import Data.Nat.Properties using (+-comm)
open import Data.Product
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable using (False)
open ≡-Reasoning

open import Pitch

RelAbs : (n : Pitch) → (relativeToAbsolute ∘ absoluteToRelative) n ≡ n
RelAbs (pitch zero) = refl
RelAbs (pitch (suc n)) =
  begin
    (relativeToAbsolute ∘ absoluteToRelative) (pitch (suc n))
  ≡⟨ refl ⟩
    relativeToAbsolute (pitchClass ((suc n) mod chromaticScaleSize) ,
                        octave ((suc n) div chromaticScaleSize))
  ≡⟨ refl ⟩
    pitch (((suc n) div chromaticScaleSize) * chromaticScaleSize +
           (toℕ ((suc n) mod chromaticScaleSize)))
  ≡⟨ cong pitch
          (+-comm (((suc n) div chromaticScaleSize) * chromaticScaleSize)
                  (toℕ ((suc n) mod chromaticScaleSize))) ⟩
    pitch ((toℕ ((suc n) mod chromaticScaleSize)) +
           (((suc n) div chromaticScaleSize) * chromaticScaleSize))
  ≡⟨ cong pitch (sym {!!}) ⟩
  -- ≡⟨ cong pitch (sym (m≡m%n+[m/n]*n n chromaticScaleSize)) ⟩
    pitch (suc n)
  ∎

{-
absRelAbs (pitch (+_     zero))    = refl
absRelAbs (pitch (+_     (suc n))) = let x = absRelAbs (pitch (+ n)) in {!!}
absRelAbs (pitch (-[1+_] zero))    = refl
absRelAbs (pitch (-[1+_] (suc n))) = {!!}
-}

AbsRel : (n : PitchOctave) → (absoluteToRelative ∘ relativeToAbsolute) n ≡ n
AbsRel (pitchClass p , octave o) =
  begin
    (absoluteToRelative ∘ relativeToAbsolute) (pitchClass p , octave o)
  ≡⟨ refl ⟩
    absoluteToRelative (pitch (o * chromaticScaleSize + (toℕ p)))
  ≡⟨ refl ⟩
    (pitchClass ((o * chromaticScaleSize + (toℕ p)) mod chromaticScaleSize) ,
                 octave ((o * chromaticScaleSize + (toℕ p)) div chromaticScaleSize))
  ≡⟨ {!!} ⟩
    (pitchClass p , octave o)
  ∎

{-
relAbsRel (relativePitch zero    , octave (+_     zero))    = refl
relAbsRel (relativePitch zero    , octave (+_     (suc n))) = {!!}
relAbsRel (relativePitch zero    , octave (-[1+_] zero))    = refl
relAbsRel (relativePitch zero    , octave (-[1+_] (suc n))) = {!!}
relAbsRel (relativePitch (suc n) , octave (+_     zero))    = {!!}
relAbsRel (relativePitch (suc n) , octave (+_     (suc o))) = {!!}
relAbsRel (relativePitch (suc n) , octave (-[1+_] zero))    = {!!}
relAbsRel (relativePitch (suc n) , octave (-[1+_] (suc o))) = {!!}
-}

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
open import Agda.Builtin.IO
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit

private
  n : Nat
  n = 7

{-# COMPILE GHC n as n #-}

postulate
  main : IO ⊤

{-# COMPILE GHC main = print n #-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Also works for parts of operators.
module NotInScope where

postulate
  X : Set
  if_then_else_ : X -> X -> X -> X
  x : X

bad = if x thenn x else x

-- The error message should /not/ claim that "if" is out of scope.


text:
-- It would be nice if this worked. The constraint we can't solve is
--   P x y = ? (x, y)
-- Solution: extend the notion of Miller patterns to include record
-- constructions.
--
-- Andreas, 2012-02-27 works now! (see issues 376 and 456)
module UncurryMeta where

data Unit : Set where
  unit : Unit

record R : Set where
  field
    x : Unit
    y : Unit

_,_ : Unit -> Unit -> R
x , y = record {x = x; y = y}

data P : Unit -> Unit -> Set where
  mkP : forall x y -> P x y

data D : (R -> Set) -> Set1 where
  d : {F : R -> Set} -> (forall x y -> F (x , y)) -> D F

unD : {F : R -> Set} -> D F -> Unit
unD (d _) = unit

test : Unit
test = unD (d mkP)


text:
-- Category of indexed families
module SOAS.Families.Core {T : Set} where

open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Sorting {T}

-- | Unsorted

-- Sets indexed by a context
Family : Set₁
Family = Ctx → Set

-- Indexed functions between families
_⇾_ : Family → Family → Set
X ⇾ Y = ∀{Γ : Ctx} → X Γ → Y Γ
infixr 10 _⇾_

-- Category of indexed families of sets and indexed functions between them
𝔽amilies : Category 1ℓ 0ℓ 0ℓ
𝔽amilies = categoryHelper record
  { Obj = Family
  ; _⇒_ = _⇾_
  ; _≈_ = λ {X}{Y} f g → ∀{Γ : Ctx}{x : X Γ} → f x ≡ g x
  ; id = id
  ; _∘_ = λ g f → g ∘ f
  ; assoc = refl
  ; identityˡ = refl
  ; identityʳ = refl
  ; equiv = record { refl = refl ; sym = λ p → sym p ; trans = λ p q → trans p q }
  ; ∘-resp-≈ = λ where {f = f} p q → trans (cong f q) p
  }
module 𝔽am = Category 𝔽amilies

-- | Sorted

-- Category of sorted families
𝔽amiliesₛ : Category 1ℓ 0ℓ 0ℓ
𝔽amiliesₛ = 𝕊orted 𝔽amilies
module 𝔽amₛ = Category 𝔽amiliesₛ

-- Type of sorted families
Familyₛ : Set₁
Familyₛ = 𝔽amₛ.Obj

-- Maps between sorted families
_⇾̣_ : Familyₛ → Familyₛ → Set
_⇾̣_ = 𝔽amₛ._⇒_
infixr 10 _⇾̣_

-- Turn sorted family into unsorted by internally quantifying over the sort
∀[_] : Familyₛ → Family
∀[ 𝒳 ] Γ = {τ : T} → 𝒳 τ Γ

-- Maps between Familyₛ functors
_⇾̣₂_ : (Familyₛ → Familyₛ) → (Familyₛ → Familyₛ) → Set₁
(𝓧 ⇾̣₂ 𝓨) = {𝒵 : Familyₛ} → 𝓧 𝒵 ⇾̣ 𝓨 𝒵

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas