text:
-- Type interpretation and soundness of typing.

-- Proof of strong normalization for well-typed terms.

module Soundness where

open import Library
open import Terms
open import Substitution
open import SN
open import SN.AntiRename
open import DeclSN using (sn; fromSN)
open import SAT3

-- Type interpretation

⟦_⟧ : (a : Ty) → SAT a
⟦ base  ⟧  =  ⟦⊥⟧
⟦ a →̂ b ⟧  =  ⟦ a ⟧  ⟦→⟧ ⟦ b ⟧

-- Context interpretation (semantic substitutions)

⟦_⟧C : ∀ Γ → ∀ {Δ} (σ : Subst Γ Δ) → Set
⟦ Γ ⟧C σ = ∀ {a} (x : Var Γ a) → σ x ∈ ⟦ a ⟧

Ext : ∀ {a Δ Γ} {t : Tm Δ a} → (𝒕 : t ∈ (⟦ a ⟧)) →
      ∀ {σ : Subst Γ Δ} (θ : ⟦ Γ ⟧C σ) → ⟦ a ∷ Γ ⟧C (t ∷s σ)
Ext {a} 𝒕 θ (zero)  = 𝒕
Ext {a} 𝒕 θ (suc x) = θ x

Rename : ∀ {Δ Δ'} → (ρ : Ren Δ Δ') →
         ∀ {Γ}{σ : Subst Γ Δ} (θ : ⟦ Γ ⟧C σ) →
         ⟦ Γ ⟧C (ρ •s σ)
Rename ρ θ {a} x = ↿ SAT.satRename ⟦ a ⟧ ρ (⇃ θ x)

sound : ∀ {a Γ} (t : Tm Γ a) {Δ} {σ : Subst Γ Δ} → (θ : ⟦ Γ ⟧C σ) → subst σ t ∈ (⟦ a ⟧)
sound (var x) θ = θ x
sound (abs t) {σ = σ} θ = ⟦abs⟧ {𝓐 = ⟦ _ ⟧} {𝓑 = ⟦ _ ⟧} (λ ρ {u} 𝑢 →
  let open ≡-Reasoning
      eq : subst (u ∷s (ρ •s σ)) t ≡ subst0 u (subst (lifts ρ) (subst (lifts σ) t))
      eq = begin

             subst (u ∷s (ρ •s σ)) t

           ≡⟨ subst-ext (cons-to-sgs u _) t ⟩

              subst (sgs u •s lifts (ρ •s σ)) t

           ≡⟨ subst-∙ _ _ t ⟩

             subst0 u (subst (lifts (ρ •s σ)) t)

           ≡⟨ ≡.cong (subst0 u) (subst-ext (lifts-∙ ρ σ) t) ⟩

             subst0 u (subst (lifts ρ •s lifts σ) t)

           ≡⟨ ≡.cong (subst0 u) (subst-∙ (lifts ρ) (lifts σ) t) ⟩

             subst0 u (subst (lifts ρ) (subst (lifts σ) t))
           ∎
  in (≡.subst (_∈ ⟦ _ ⟧) eq (↿ (⇃ sound t (Ext (↿ (⇃ 𝑢)) ((Rename ρ θ)))))))

sound (app t u) θ = ↿ (⇃ ⟦app⟧ {𝓐 = ⟦ _ ⟧} {𝓑 = ⟦ _ ⟧} (sound t θ) (↿ (⇃ sound u θ)))

-- Identity environment.

id-θ : ∀{Γ} → ⟦ Γ ⟧C ids
id-θ {Γ} {a} x = ⟦var⟧ ⟦ a ⟧ x

-- Any well-typed term inhabits its semantic type.

sound' : ∀ {a Γ} (t : Tm Γ a) → t ∈ ⟦ a ⟧
sound' t rewrite ≡.sym (subst-id {vt = `Tm} t) = sound t id-θ

-- Any well-typed term is strongly normalizing.

strong-normalization :  ∀ a {Γ} (t : Tm Γ a) → sn t
strong-normalization a t = fromSN (satSN ⟦ a ⟧ (⇃ sound' t))

-- Q.E.D.

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
{-# OPTIONS --safe #-}
module Cubical.Homotopy.Hopf where

open import Cubical.Homotopy.HSpace

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Function
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Data.Int hiding (_·_)

open import Cubical.HITs.Pushout.Flattening
open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn hiding (joinS¹S¹→S³)
open import Cubical.HITs.Susp
open import Cubical.HITs.S1
open import Cubical.HITs.S2
open import Cubical.HITs.S3
open import Cubical.HITs.PropositionalTruncation
  renaming (rec to pRec ; elim to pElim)
open import Cubical.HITs.Join
open import Cubical.HITs.Interval
  renaming ( zero to I0 ; one to I1 )

open Iso
open HSpace
open AssocHSpace

private
  retEq≡secEq : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B)
                  → (x : _) → secEq e (e .fst x) ≡ cong (e .fst) (retEq e x)
  retEq≡secEq {A = A} =
    EquivJ (λ B e → (x : _) → secEq e (e .fst x) ≡ cong (e .fst) (retEq e x))
           λ _ → refl

module Hopf {ℓ : Level} {A : Pointed ℓ} {e : HSpace A}
            (e-ass : AssocHSpace e) (conA : ((x y : typ A) → ∥ x ≡ y ∥)) where
  isEquiv-μ : (x : typ A) → isEquiv (λ z → (μ e z x))
  isEquiv-μ x = pRec (isPropIsEquiv _)
                     (J (λ x _ → isEquiv (λ z → μ e z x))
                       (subst isEquiv (funExt (λ z → sym (μᵣ e z)))
                                      (idIsEquiv (typ A))))
                     (conA (pt A) x)

  isEquiv-μ' : (x : typ A) → isEquiv (μ e x)
  isEquiv-μ' x =
    pRec (isPropIsEquiv _)
          (J (λ x _ → isEquiv (μ e x))
            (subst isEquiv (funExt (λ x → sym (μₗ e x))) (idIsEquiv (typ A))))
          (conA (pt A) x)

  μ-eq : (x : typ A) → typ A ≃ typ A
  μ-eq x = (λ z → μ e z x) , (isEquiv-μ x)

  μ-eq' : (x : typ A) → typ A ≃ typ A
  μ-eq' x = μ e x , isEquiv-μ' x

  Hopf : Susp (typ A) → Type ℓ
  Hopf north = typ A
  Hopf south = typ A
  Hopf (merid a i₁) = ua (μ-eq a) i₁

  TotalSpaceHopfPush : Type _
  TotalSpaceHopfPush =
    Pushout {A = typ A × typ A} fst λ x → μ e (fst x) (snd x)

  TotalSpaceHopfPush→TotalSpace :
    TotalSpaceHopfPush → Σ[ x ∈ Susp (typ A) ] Hopf x
  TotalSpaceHopfPush→TotalSpace (inl x) = north , x
  TotalSpaceHopfPush→TotalSpace (inr x) = south , x
  TotalSpaceHopfPush→TotalSpace (push (x , y) i₁) =
    merid y i₁ , ua-gluePt (μ-eq y) i₁ x

  joinIso₁ : Iso (TotalSpaceHopfPush) (join (typ A) (typ A))
  joinIso₁ = theIso
    where
    F : TotalSpaceHopfPush → join (typ A) (typ A)
    F (inl x) = inl x
    F (inr x) = inr x
    F (push (a , x) i) = push a (μ e a x) i

    G : join (typ A) (typ A) → TotalSpaceHopfPush
    G (inl x) = inl x
    G (inr x) = inr x
    G (push a b i) =
      (push (a , invEq (μ-eq' a) b) ∙ cong inr (secEq (μ-eq' a) b)) i

    s : section F G
    s (inl x) = refl
    s (inr x) = refl
    s (push a b i) j =
      hcomp (λ k → λ { (i = i0) → inl a
                      ; (i = i1) → inr (secEq (μ-eq' a) b (j ∨ k))
                      ; (j = i0) → F (compPath-filler
                                       (push (a , invEq (μ-eq' a) b))
                                       (cong inr (secEq (μ-eq' a) b)) k i)
                      ; (j = i1) → push a b i})
        (hcomp (λ k → λ { (i = i0) → inl a
                      ; (i = i1) → inr (secEq (μ-eq' a) b (~ k ∨ j))
                      ; (j = i0) → push a (secEq (μ-eq' a) b (~ k)) i
                      ; (j = i1) → push a b i})
               (push a b i))

    r : retract F G
    r (inl x) = refl
    r (inr x) = refl
    r (push (x , y) i) j =
      hcomp (λ k → λ { (i = i0) → inl x
                      ; (i = i1) → inr (μ e x y)
                      ; (j = i0) → (push (x , invEq (μ-eq' x) (μ e x y))
                                  ∙ (λ i₁ → inr (retEq≡secEq (μ-eq' x) y (~ k) i₁))) i
                      ; (j = i1) → push (x , y) i})
         (hcomp (λ k → λ { (i = i0) → inl x
                      ; (i = i1) → inr (μ e x (retEq (μ-eq' x) y k))
                      ; (j = i1) → push (x , retEq (μ-eq' x) y k) i})
                ((push (x , invEq (μ-eq' x) (μ e x y))) i))

    theIso : Iso TotalSpaceHopfPush (join (typ A) (typ A))
    fun theIso = F
    inv theIso = G
    rightInv theIso = s
    leftInv theIso = r

  isEquivTotalSpaceHopfPush→TotalSpace :
    isEquiv TotalSpaceHopfPush→TotalSpace
  isEquivTotalSpaceHopfPush→TotalSpace =
    isoToIsEquiv theIso
    where
    inv' : _ → _
    inv' (north , y) = inl y
    inv' (south , y) = inr y
    inv' (merid a i , y) =
      hcomp (λ k → λ { (i = i0) → push (y , a) (~ k)
                      ; (i = i1) → inr y})
            (inr (ua-unglue (μ-eq a) i y))
      where

      pp : PathP (λ i → ua (μ-eq a) i → TotalSpaceHopfPush)
                 inl inr
      pp = ua→ {e = μ-eq a} {B = λ _ → TotalSpaceHopfPush} λ b → push (b , a)

    sect : (x : _) → TotalSpaceHopfPush→TotalSpace (inv' x) ≡ x
    sect (north , x) = refl
    sect (south , x) = refl
    sect (merid a i , y) j =
      hcomp (λ k → λ { (i = i0) → merid a (~ k ∧ ~ j)
                                  , ua-gluePt (μ-eq a) (~ k ∧ ~ j) y
                      ; (i = i1) → south , y
                      ; (j = i0) →
                        TotalSpaceHopfPush→TotalSpace
                         (hfill (λ k → λ { (i = i0) → push (y , a) (~ k)
                                          ; (i = i1) → inr y})
                                (inS (inr (ua-unglue (μ-eq a) i y)))
                                k)
                      ; (j = i1) → merid a i , y})
            ((merid a (i ∨ ~ j)) , lem (μ-eq a) i j y)
      where
      lem : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B) →
                PathP (λ i → PathP (λ j → (y : ua e i) → ua e (i ∨ ~ j))
                 (λ y → ua-unglue e i y)
                 λ y → y)
                 (λ j y → ua-gluePt e (~ j) y)
                 refl
      lem {A = A} {B = B} =
        EquivJ (λ B e → PathP (λ i → PathP (λ j → (y : ua e i) → ua e (i ∨ ~ j))
          (λ y → ua-unglue e i y)
           λ y → y)
           (λ j y → ua-gluePt e (~ j) y)
           refl)
           λ i j a → ua-gluePt (idEquiv B) (i ∨ ~ j) (ua-unglue (idEquiv B) i a)

    retr : retract TotalSpaceHopfPush→TotalSpace inv'
    retr (inl x) = refl
    retr (inr x) = refl
    retr (push (x , y) i) j =
      hcomp (λ k → λ { (i = i0) → push (x , y) (~ k)
                      ; (i = i1) → inr (μ e x y)
                      ; (j = i1) → push (x , y) (i ∨ ~ k)})
            (inr (μ e x y))

    theIso : Iso TotalSpaceHopfPush (Σ (Susp (typ A)) Hopf)
    fun theIso = TotalSpaceHopfPush→TotalSpace
    inv theIso = inv'
    rightInv theIso = sect
    leftInv theIso = retr

  IsoTotalSpaceJoin : Iso (Σ[ x ∈ Susp (typ A) ] Hopf x) (join (typ A) (typ A))
  IsoTotalSpaceJoin =
    compIso (equivToIso (invEquiv (_ , isEquivTotalSpaceHopfPush→TotalSpace)))
            joinIso₁

  induced : TotalSpaceHopfPush → Susp (typ A)
  induced = fst ∘ TotalSpaceHopfPush→TotalSpace

  ua-lem : (x y z : typ A) → (i j : I) → ua (μ-eq y) i
  ua-lem x y z i j =
    fill (λ k → ua (μ-eq y) i)
         (λ j → λ { (i = i0) → μ e z x
                  ; (i = i1) → μ-assoc e-ass z x y j})
          (inS (ua-gluePt (μ-eq y) i (μ e z x)))
          j

  TotalSpaceHopfPush→≃Hopf : (x : TotalSpaceHopfPush) → typ A ≃ Hopf (induced x)
  TotalSpaceHopfPush→≃Hopf (inl x) = μ-eq x
  TotalSpaceHopfPush→≃Hopf (inr x) = μ-eq x
  TotalSpaceHopfPush→≃Hopf (push (x , y) i₁) = pp x y i₁
    where
    pp : (x y : _) → PathP (λ i → typ A ≃ ua (μ-eq y) i) (μ-eq x) (μ-eq (μ e x y))
    pp x y = ΣPathP (P , help)
      where
      P : PathP (λ z → typ A → ua (μ-eq y) z) (fst (μ-eq x))
                (fst (μ-eq (μ e x y)))
      P i z = ua-lem x y z i i1

      abstract
        help : PathP (λ i₂ → isEquiv (P i₂)) (snd (μ-eq x))
                     (snd (μ-eq (μ e x y)))
        help = toPathP (isPropIsEquiv _ _ _)

  Push→TotalSpaceHopf : (a : typ A) (x : TotalSpaceHopfPush)
    → Σ[ x ∈ Susp (typ A) ] Hopf x
  Push→TotalSpaceHopf a x = (induced x) , fst (TotalSpaceHopfPush→≃Hopf x) a

  Push→TotalSpaceHopf-equiv : (a : typ A) → isEquiv (Push→TotalSpaceHopf a)
  Push→TotalSpaceHopf-equiv a = pRec (isPropIsEquiv _)
                    (J (λ a _ → isEquiv (Push→TotalSpaceHopf a))
                      (subst isEquiv (sym main)
                        isEquivTotalSpaceHopfPush→TotalSpace))
                    (conA (pt A) a)
    where
    lem₁ : (x : _) → fst ((Push→TotalSpaceHopf (pt A)) x)
                    ≡ fst (TotalSpaceHopfPush→TotalSpace x)
    lem₁ (inl x) = refl
    lem₁ (inr x) = refl
    lem₁ (push a i) = refl

    lem₂ : (x : _)
      → PathP (λ i → Hopf (lem₁ x i))
               (snd ((Push→TotalSpaceHopf (pt A)) x))
               (snd (TotalSpaceHopfPush→TotalSpace x))
    lem₂ (inl x) = μₗ e x
    lem₂ (inr x) = μₗ e x
    lem₂ (push (x , y) i) j =
      hcomp (λ k → λ {(i = i0) → μₗ e x j
                     ; (i = i1) → μ-assoc-filler e-ass x y j k
                     ; (j = i0) → ua-lem x y (pt A) i k
                     ; (j = i1) → ua-gluePt (μ-eq y) i x})
            (ua-gluePt (μ-eq y) i (μₗ e x j))

    main : Push→TotalSpaceHopf (pt A) ≡ TotalSpaceHopfPush→TotalSpace
    main i x = (lem₁ x i) , (lem₂ x i)

  TotalSpaceHopfPush² : Type _
  TotalSpaceHopfPush² = Pushout {A = TotalSpaceHopfPush} (λ _ → tt) induced

  P : TotalSpaceHopfPush² → Type _
  P (inl x) = typ A
  P (inr x) = Hopf x
  P (push a i) = ua (TotalSpaceHopfPush→≃Hopf a) i

  TotalSpacePush² : Type _
  TotalSpacePush² = Σ[ x ∈ TotalSpaceHopfPush² ] P x

  TotalSpacePush²' : Type _
  TotalSpacePush²' =
    Pushout {A = typ A × TotalSpaceHopfPush}
            {C = Σ[ x ∈ Susp (typ A) ] Hopf x}
            fst
            λ x → Push→TotalSpaceHopf (fst x) (snd x)

  IsoTotalSpacePush²TotalSpacePush²' : Iso TotalSpacePush² TotalSpacePush²'
  IsoTotalSpacePush²TotalSpacePush²' =
    compIso iso₂ (compIso (equivToIso fl.flatten) iso₁)
    where
    module fl =
      FlatteningLemma (λ _ → tt) induced (λ x → typ A)
                      Hopf TotalSpaceHopfPush→≃Hopf

    iso₁ : Iso (Pushout fl.Σf fl.Σg) TotalSpacePush²'
    fun iso₁ (inl x) = inl (snd x)
    fun iso₁ (inr x) = inr x
    fun iso₁ (push a i) = push ((snd a) , (fst a)) i
    inv iso₁ (inl x) = inl (tt , x)
    inv iso₁ (inr x) = inr x
    inv iso₁ (push a i) = push (snd a , fst a) i
    rightInv iso₁ (inl x) = refl
    rightInv iso₁ (inr x) = refl
    rightInv iso₁ (push a i) = refl
    leftInv iso₁ (inl x) = refl
    leftInv iso₁ (inr x) = refl
    leftInv iso₁ (push a i) = refl

    iso₂ : Iso TotalSpacePush² (Σ (Pushout (λ _ → tt) induced) fl.E)
    fun iso₂ (inl x , y) = inl x , y
    fun iso₂ (inr x , y) = inr x , y
    fun iso₂ (push a i , y) = push a i , y
    inv iso₂ (inl x , y) = inl x , y
    inv iso₂ (inr x , y) = inr x , y
    inv iso₂ (push a i , y) = push a i , y
    rightInv iso₂ (inl x , snd₁) = refl
    rightInv iso₂ (inr x , snd₁) = refl
    rightInv iso₂ (push a i , snd₁) = refl
    leftInv iso₂ (inl x , snd₁) = refl
    leftInv iso₂ (inr x , snd₁) = refl
    leftInv iso₂ (push a i , snd₁) = refl

  F : TotalSpacePush²'
     → (Pushout {A = typ A × Σ (Susp (typ A)) Hopf} fst snd)
  F (inl x) = inl x
  F (inr x) = inr x
  F (push (x , y) i) = push (x , Push→TotalSpaceHopf x y) i

  G : (Pushout {A = typ A × Σ (Susp (typ A)) Hopf} fst snd)
    → TotalSpacePush²'
  G (inl x) = inl x
  G (inr x) = inr x
  G (push (x , y) i) =
    hcomp (λ k → λ { (i = i0) → inl x
                    ; (i = i1)
                     → inr (secEq (_ , Push→TotalSpaceHopf-equiv x) y k)})
      (push (x , invEq (_ , Push→TotalSpaceHopf-equiv x) y) i)

  IsoTotalSpacePush²'ΣPush : Iso TotalSpacePush²'
           (Pushout {A = typ A × Σ (Susp (typ A)) Hopf} fst snd)
  fun IsoTotalSpacePush²'ΣPush = F
  inv IsoTotalSpacePush²'ΣPush = G
  rightInv IsoTotalSpacePush²'ΣPush (inl x) = refl
  rightInv IsoTotalSpacePush²'ΣPush (inr x) = refl
  rightInv IsoTotalSpacePush²'ΣPush (push (x , y) i) j =
    hcomp (λ k → λ { (i = i0) → inl x
                    ; (i = i1)
                     → inr (secEq (_ , Push→TotalSpaceHopf-equiv x) y k)
                    ; (j = i0) → F (
                         hfill (λ k →
                           λ { (i = i0) → inl x
                             ; (i = i1)
                              → inr (secEq (_
                                    , Push→TotalSpaceHopf-equiv x) y k)})
                          (inS (push (x
                                    , invEq (_
                                     , Push→TotalSpaceHopf-equiv x) y) i)) k)
                    ; (j = i1)
                     → push (x
                           , (secEq (_
                            , Push→TotalSpaceHopf-equiv x) y k)) i})
          (push (x , (secEq (_ , Push→TotalSpaceHopf-equiv x) y i0)) i)
  leftInv IsoTotalSpacePush²'ΣPush (inl x) = refl
  leftInv IsoTotalSpacePush²'ΣPush (inr x) = refl
  leftInv IsoTotalSpacePush²'ΣPush (push (x , y) i) j =
    hcomp (λ k → λ { (i = i0) → inl x
                    ; (i = i1) → inr (secEq (Push→TotalSpaceHopf x
                                           , Push→TotalSpaceHopf-equiv x)
                                        (Push→TotalSpaceHopf x y) (j ∨ k))
                    ; (j = i1) → push (x , y) i})
          (hcomp (λ k → λ { (i = i0) → inl x
                           ; (i = i1) → inr (retEq≡secEq
                                              (Push→TotalSpaceHopf x
                                             , Push→TotalSpaceHopf-equiv x)
                                               y (~ k) j)
                           ; (j = i1) → push (x , y) i
                           ; (j = i0) → push (x , invEq
                                               (Push→TotalSpaceHopf x
                                              , Push→TotalSpaceHopf-equiv x)
                                               (Push→TotalSpaceHopf x y)) i})
            (push (x , retEq (Push→TotalSpaceHopf x
                            , Push→TotalSpaceHopf-equiv x) y j) i))

  joinIso₂ : Iso TotalSpacePush² (join (typ A) (join (typ A) (typ A)))
  joinIso₂ =
    compIso IsoTotalSpacePush²TotalSpacePush²'
              (compIso IsoTotalSpacePush²'ΣPush
                (compIso (equivToIso (joinPushout≃join _ _))
                  (pathToIso (cong (join (typ A))
                             (isoToPath IsoTotalSpaceJoin)))))

-- Direct construction of Hopf fibration for S¹
module S¹Hopf where
  Border : (x : S¹) → (j : I) → Partial (j ∨ ~ j) (Σ Type₀ (λ T → T ≃ S¹))
  Border x j (j = i0) = S¹ , (x ·_) , rotIsEquiv x
  Border x j (j = i1) = S¹ , idEquiv S¹

  -- Hopf fibration using SuspS¹
  HopfSuspS¹ : SuspS¹ → Type₀
  HopfSuspS¹ north = S¹
  HopfSuspS¹ south = S¹
  HopfSuspS¹ (merid x j) = Glue S¹ (Border x j)

  -- Hopf fibration using S²
  -- TODO : prove that it is equivalent to HopfSuspS¹
  HopfS² : S² → Type₀
  HopfS² base = S¹
  HopfS² (surf i j) = Glue S¹ (λ { (i = i0) → _ , idEquiv S¹
                                 ; (i = i1) → _ , idEquiv S¹
                                 ; (j = i0) → _ , idEquiv S¹
                                 ; (j = i1) → _ , _ , rotIsEquiv (loop i) } )

  -- Hopf fibration using more direct definition of the rot equivalence
  -- TODO : prove that it is equivalent to HopfSuspS¹
  HopfS²' : S² → Type₀
  HopfS²' base = S¹
  HopfS²' (surf i j) = Glue S¹ (λ { (i = i0) → _ , rotLoopEquiv i0
                                  ; (i = i1) → _ , rotLoopEquiv i0
                                  ; (j = i0) → _ , rotLoopEquiv i0
                                  ; (j = i1) → _ , rotLoopEquiv i } )

  -- Total space of the fibration
  TotalHopf : Type₀
  TotalHopf = Σ SuspS¹ HopfSuspS¹

  -- Forward direction
  filler-1 : I → (j : I) → (y : S¹) → Glue S¹ (Border y j) → join S¹ S¹
  filler-1 i j y x = hfill (λ t → λ { (j = i0) → inl (rotInv-1 x y t)
                                    ; (j = i1) → inr x })
                           (inS (push ((unglue (j ∨ ~ j) x) · invLooper y) (unglue (j ∨ ~ j) x) j)) i

  TotalHopf→JoinS¹S¹ : TotalHopf → join S¹ S¹
  TotalHopf→JoinS¹S¹ (north , x) = inl x
  TotalHopf→JoinS¹S¹ (south , x) = inr x
  TotalHopf→JoinS¹S¹ (merid y j , x) = filler-1 i1 j y x

  -- Backward direction
  JoinS¹S¹→TotalHopf : join S¹ S¹ → TotalHopf
  JoinS¹S¹→TotalHopf (inl x) = (north , x)
  JoinS¹S¹→TotalHopf (inr x) = (south , x)
  JoinS¹S¹→TotalHopf (push y x j) =
    (merid (invLooper y · x) j
    , glue (λ { (j = i0) → y ; (j = i1) → x }) (rotInv-2 x y j))

  -- Now for the homotopies, we will need to fill squares indexed by x y : S¹ with value in S¹
  -- Some will be extremeley tough, but happen to be easy when x = y = base
  -- therefore, we fill them for x = y = base and then use the connectedness of S¹ × S¹ and
  -- the discreteness of ΩS¹ to get general fillers.

  -- To proceed with that strategy, we first need a lemma :
  -- the sections of the trivial fibration λ (_ : S¹) (_ : S¹) → Int are constant

  -- this should be generalized to a constant fibration over a connected space with
  -- discrete fiber
  fibℤ : S¹ → S¹ → Type₀
  fibℤ _ _ = ℤ

  S¹→HSet : (A : Type₀) (p : isSet A) (F : S¹ → A) (x : S¹) → F base ≡ F x
  S¹→HSet A p F base = refl {x = F base}
  S¹→HSet A p F (loop i) = f' i
    where
    f : PathP (λ i → F base ≡ F (loop i)) refl (cong F loop)
    f i = λ j → F (loop (i ∧ j))
    L : cong F loop ≡ refl
    L = p (F base) (F base) (f i1) refl
    f' : PathP (λ i → F base ≡ F (loop i)) (refl {x = F base}) (refl {x = F base})
    f' = transport (λ i → PathP (λ j → F base ≡ F (loop j)) refl (L i)) f

  constant-loop : (F : S¹ → S¹ → ℤ) → (x y : S¹) → F base base ≡ F x y
  constant-loop F x y = L0 ∙ L1
    where
    p : isSet (S¹ → ℤ)
    p = isSetΠ (λ _ → isSetℤ)
    L : F base ≡ F x
    L = S¹→HSet (S¹ → ℤ) p F x
    L0 : F base base ≡ F x base
    L0 i = L i base
    L1 : F x base ≡ F x y
    L1 = S¹→HSet ℤ isSetℤ (F x) y

  discretefib : (F : S¹ → S¹ → Type₀) → Type₀
  discretefib F = (a : (x y : S¹) → F x y) →
          (b : (x y : S¹) → F x y) →
          (a base base ≡ b base base) →
          (x y : S¹) → a x y ≡ b x y

  discretefib-fibℤ : discretefib fibℤ
  discretefib-fibℤ a b h x y i =
    hcomp (λ t → λ { (i = i0) → constant-loop a x y t
                   ; (i = i1) → constant-loop b x y t })
          (h i)

  -- first homotopy

  assocFiller-3-aux : I → I → I → I → S¹
  assocFiller-3-aux x y j i =
    hfill (λ t → λ { (i = i0) → rotInv-1 (loop y) (loop (~ y) · loop x) t
                   ; (i = i1) → rotInv-3 (loop y) (loop x) t
                   ; (x = i0) (y = i0) → base
                   ; (x = i0) (y = i1) → base
                   ; (x = i1) (y = i0) → base
                   ; (x = i1) (y = i1) → base })
          (inS ((rotInv-2 (loop x) (loop y) i) · (invLooper (loop (~ y) · loop x)))) j

  -- assocFiller-3-endpoint is used only in the type of the next function, to specify the
  -- second endpoint.
  -- However, I only need the first endpoint, but I cannot specify only one of them as is.
  -- TODO : use cubical extension types when available to remove assocFiller-3-endpoint
  assocFiller-3-endpoint : (x : S¹) → (y : S¹) → y ≡ y
  assocFiller-3-endpoint base base i = base
  assocFiller-3-endpoint (loop x) base i = assocFiller-3-aux x i0 i1 i
  assocFiller-3-endpoint base (loop y) i = assocFiller-3-aux i0 y i1 i
  assocFiller-3-endpoint (loop x) (loop y) i = assocFiller-3-aux x y i1 i

  assocFiller-3 : (x : S¹) → (y : S¹) →
                  PathP (λ j → rotInv-1 y (invLooper y · x) j ≡ rotInv-3 y x j)
                        (λ i → ((rotInv-2 x y i) · (invLooper (invLooper y · x))))
                        (assocFiller-3-endpoint x y)
  assocFiller-3 base base j i = base
  assocFiller-3 (loop x) base j i = assocFiller-3-aux x i0 j i
  assocFiller-3 base (loop y) j i = assocFiller-3-aux i0 y j i
  assocFiller-3 (loop x) (loop y) j i = assocFiller-3-aux x y j i

  assoc-3 : (_ y : S¹) → basedΩS¹ y
  assoc-3 x y i = assocFiller-3 x y i1 i

  fibℤ≡fibAssoc-3 : fibℤ ≡ (λ _ y → basedΩS¹ y)
  fibℤ≡fibAssoc-3 i = λ x y → basedΩS¹≡ℤ y (~ i)

  discretefib-fibAssoc-3 : discretefib (λ _ y → basedΩS¹ y)
  discretefib-fibAssoc-3 =
    transp (λ i → discretefib (fibℤ≡fibAssoc-3 i)) i0 discretefib-fibℤ

  assocConst-3 : (x y : S¹) → assoc-3 x y ≡ refl
  assocConst-3 x y = discretefib-fibAssoc-3 assoc-3 (λ _ _ → refl) refl x y

  assocSquare-3 : I → I → S¹ → S¹ → S¹
  assocSquare-3 i j x y = hcomp (λ t → λ { (i = i0) → assocFiller-3 x y j i0
                                         ; (i = i1) → assocFiller-3 x y j i1
                                         ; (j = i0) → assocFiller-3 x y i0 i
                                         ; (j = i1) → assocConst-3 x y t i })
                              (assocFiller-3 x y j i)

  filler-3 : I → I → S¹ → S¹ → join S¹ S¹
  filler-3 i j y x =
    hcomp (λ t → λ { (i = i0) → filler-1 t j (invLooper y · x)
                                             (glue (λ { (j = i0) → y ; (j = i1) → x })
                                                   (rotInv-2 x y j))
                   ; (i = i1) → push (rotInv-3 y x t) x j
                   ; (j = i0) → inl (assocSquare-3 i t x y)
                   ; (j = i1) → inr x })
          (push ((rotInv-2 x y (i ∨ j)) · (invLooper (invLooper y · x))) (rotInv-2 x y (i ∨ j)) j)

  JoinS¹S¹→TotalHopf→JoinS¹S¹ : ∀ x → TotalHopf→JoinS¹S¹ (JoinS¹S¹→TotalHopf x) ≡ x
  JoinS¹S¹→TotalHopf→JoinS¹S¹ (inl x) i = inl x
  JoinS¹S¹→TotalHopf→JoinS¹S¹ (inr x) i = inr x
  JoinS¹S¹→TotalHopf→JoinS¹S¹ (push y x j) i = filler-3 i j y x

  -- Second homotopy

  -- This HIT is the total space of the Hopf fibration but the ends of SuspS¹ have not been
  -- glued together yet — which makes it into a cylinder.
  -- This allows to write compositions that do not properly match at the endpoints. However,
  -- I suspect it is unnecessary. TODO : do without PseudoHopf

  PseudoHopf : Type₀
  PseudoHopf = (S¹ × Interval) × S¹

  PseudoHopf-π1 : PseudoHopf → S¹
  PseudoHopf-π1 ((y , _) , _) = y

  PseudoHopf-π2 : PseudoHopf → S¹
  PseudoHopf-π2 (_ , x) = x

  assocFiller-4-aux : I → I → I → I → S¹
  assocFiller-4-aux x y j i =
    hfill (λ t → λ { (i = i0) → ((invLooper (loop y · loop x · loop (~ y))) · (loop y · loop x))
                                · (rotInv-1 (loop x) (loop y) t)
                   ; (i = i1) → (rotInv-4 (loop y) (loop y · loop x) (~ t)) · loop x
                   ; (x = i0) (y = i0) → base
                   ; (x = i0) (y = i1) → base
                   ; (x = i1) (y = i0) → base
                   ; (x = i1) (y = i1) → base })
          (inS (rotInv-2 (loop y · loop x) (loop y · loop x · loop (~ y)) i)) j

  -- See assocFiller-3-endpoint
  -- TODO : use cubical extension types when available to remove assocFiller-4-endpoint
  assocFiller-4-endpoint : (x y : S¹) → basedΩS¹ (((invLooper (y · x · invLooper y)) · (y · x)) · x)
  assocFiller-4-endpoint base base i = base
  assocFiller-4-endpoint (loop x) base i = assocFiller-4-aux x i0 i1 i
  assocFiller-4-endpoint base (loop y) i = assocFiller-4-aux i0 y i1 i
  assocFiller-4-endpoint (loop x) (loop y) i = assocFiller-4-aux x y i1 i

  assocFiller-4 : (x y : S¹) →
                  PathP (λ j → ((invLooper (y · x · invLooper y)) · (y · x)) · (rotInv-1 x y j) ≡ (rotInv-4 y (y · x) (~ j)) · x)
                        (λ i → (rotInv-2 (y · x) (y · x · invLooper y) i))
                        (assocFiller-4-endpoint x y)
  assocFiller-4 base base j i = base
  assocFiller-4 (loop x) base j i = assocFiller-4-aux x i0 j i
  assocFiller-4 base (loop y) j i = assocFiller-4-aux i0 y j i
  assocFiller-4 (loop x) (loop y) j i = assocFiller-4-aux x y j i

  assoc-4 : (x y : S¹) → basedΩS¹ (((invLooper (y · x · invLooper y)) · (y · x)) · x)
  assoc-4 x y i = assocFiller-4 x y i1 i

  fibℤ≡fibAssoc-4 : fibℤ ≡ (λ x y → basedΩS¹ (((invLooper (y · x · invLooper y)) · (y · x)) · x))
  fibℤ≡fibAssoc-4 i = λ x y → basedΩS¹≡ℤ (((invLooper (y · x · invLooper y)) · (y · x)) · x) (~ i)

  discretefib-fibAssoc-4 : discretefib (λ x y → basedΩS¹ (((invLooper (y · x · invLooper y)) · (y · x)) · x))
  discretefib-fibAssoc-4 =
    transp (λ i → discretefib (fibℤ≡fibAssoc-4 i)) i0 discretefib-fibℤ

  assocConst-4 : (x y : S¹) → assoc-4 x y ≡ refl
  assocConst-4 x y = discretefib-fibAssoc-4 assoc-4 (λ _ _ → refl) refl x y

  assocSquare-4 : I → I → S¹ → S¹ → S¹
  assocSquare-4 i j x y =
    hcomp (λ t → λ { (i = i0) → assocFiller-4 x y j i0
                   ; (i = i1) → assocFiller-4 x y j i1
                   ; (j = i0) → assocFiller-4 x y i0 i
                   ; (j = i1) → assocConst-4 x y t i })
          (assocFiller-4 x y j i)

  filler-4-0 : (_ j : I) → (y : S¹) → Glue S¹ (Border y j) → PseudoHopf
  filler-4-0 i j y x =
    let x' = unglue (j ∨ ~ j) x in
    hfill (λ t → λ { (j = i0) → ((invLooper (y · x · invLooper y) · (y · x) , I0)
                                , invLooper (y · x · invLooper y) · (y · x) · (rotInv-1 x y t))
                   ; (j = i1) → ((invLooper (x · invLooper y) · x , I1) , x) })
          (inS ((invLooper (x' · invLooper y) · x' , seg j) , rotInv-2 x' (x' · invLooper y) j)) i

  filler-4-1 : (_ j : I) → (y : S¹) → Glue S¹ (Border y j) → PseudoHopf
  filler-4-1 i j y x =
    let x' = unglue (j ∨ ~ j) x in
    hfill (λ t → λ { (j = i0) → ((invLooper (y · x · invLooper y) · (y · x) , I0)
                                , (rotInv-4 y (y · x) (~ t)) · x)
                   ; (j = i1) → ((invLooper (x · invLooper y) · x , I1) , x) })
          (inS ((invLooper (x' · invLooper y) · x' , seg j) , unglue (j ∨ ~ j) x)) i

  filler-4-2 : (_ j : I) → (y : S¹) → Glue S¹ (Border y j) → TotalHopf
  filler-4-2 i j y x =
    let x' = unglue (j ∨ ~ j) x in
    hcomp (λ t → λ { (i = i0) → JoinS¹S¹→TotalHopf (filler-1 t j y x)
                   ; (i = i1) → (merid (PseudoHopf-π1 (filler-4-0 t j y x)) j
                                , glue (λ { (j = i0) → rotInv-1 x y t ; (j = i1) → x })
                                       (PseudoHopf-π2 (filler-4-0 t j y x)))
                   ; (j = i0) → (north , rotInv-1 x y t)
                   ; (j = i1) → (south , x) })
          (merid (invLooper (x' · invLooper y) · x') j
          , glue (λ { (j = i0) → y · x · invLooper y ; (j = i1) → x }) (rotInv-2 x' (x' · invLooper y) j))

  filler-4-3 : (_ j : I) → (y : S¹) → Glue S¹ (Border y j) → PseudoHopf
  filler-4-3 i j y x =
    let x' = unglue (j ∨ ~ j) x in
    hcomp (λ t → λ { (i = i0) → filler-4-0 t j y x
                   ; (i = i1) → filler-4-1 t j y x
                   ; (j = i0) → ((invLooper (y · x · invLooper y) · (y · x) , I0) , assocSquare-4 i t x y)
                   ; (j = i1) → ((invLooper (x · invLooper y) · x , I1) , x) })
          ((invLooper (x' · invLooper y) · x' , seg j) , rotInv-2 x' (x' · invLooper y) (i ∨ j))

  filler-4-4 : (_ j : I) → (y : S¹) → Glue S¹ (Border y j) → PseudoHopf
  filler-4-4 i j y x =
    let x' = unglue (j ∨ ~ j) x in
    hcomp (λ t → λ { (i = i0) → filler-4-1 t j y x
                   ; (i = i1) → ((y , seg j) , unglue (j ∨ ~ j) x)
                   ; (j = i0) → ((rotInv-4 y (y · x) i , I0)
                                , (rotInv-4 y (y · x) (i ∨ ~ t)) · x)
                   ; (j = i1) → ((rotInv-4 y x i , I1) , x) })
          ((rotInv-4 y x' i , seg j) , x')

  filler-4-5 : (_ j : I) → (y : S¹) → Glue S¹ (Border y j) → TotalHopf
  filler-4-5 i j y x =
    hcomp (λ t → λ { (i = i0) → filler-4-2 (~ t) j y x
                   ; (i = i1) → (merid (PseudoHopf-π1 (filler-4-4 t j y x)) j
                                , glue (λ { (j = i0) → x ; (j = i1) → x })
                                       (PseudoHopf-π2 (filler-4-4 t j y x)))
                   ; (j = i0) → (north , x)
                   ; (j = i1) → (south , x) })
          (merid (PseudoHopf-π1 (filler-4-3 i j y x)) j
          , glue (λ { (j = i0) → x ; (j = i1) → x }) (PseudoHopf-π2 (filler-4-3 i j y x)))

  TotalHopf→JoinS¹S¹→TotalHopf : ∀ x → JoinS¹S¹→TotalHopf (TotalHopf→JoinS¹S¹ x) ≡ x
  TotalHopf→JoinS¹S¹→TotalHopf (north , x) i = (north , x)
  TotalHopf→JoinS¹S¹→TotalHopf (south , x) i = (south , x)
  TotalHopf→JoinS¹S¹→TotalHopf (merid y j , x) i = filler-4-5 i j y x

  JoinS¹S¹≡TotalHopf : join S¹ S¹ ≡ TotalHopf
  JoinS¹S¹≡TotalHopf = isoToPath (iso JoinS¹S¹→TotalHopf
                                      TotalHopf→JoinS¹S¹
                                      TotalHopf→JoinS¹S¹→TotalHopf
                                      JoinS¹S¹→TotalHopf→JoinS¹S¹)

  S³≡TotalHopf : S³ ≡ TotalHopf
  S³≡TotalHopf = S³≡joinS¹S¹ ∙ JoinS¹S¹≡TotalHopf

  open Iso
  IsoS³TotalHopf : Iso (S₊ 3) TotalHopf
  fun IsoS³TotalHopf x = JoinS¹S¹→TotalHopf (S³→joinS¹S¹ (inv IsoS³S3 x))
  inv IsoS³TotalHopf x = fun IsoS³S3 (joinS¹S¹→S³ (TotalHopf→JoinS¹S¹ x))
  rightInv IsoS³TotalHopf x =
       cong (JoinS¹S¹→TotalHopf ∘ S³→joinS¹S¹)
            (leftInv IsoS³S3 (joinS¹S¹→S³ (TotalHopf→JoinS¹S¹ x)))
    ∙∙ cong JoinS¹S¹→TotalHopf
            (joinS¹S¹→S³→joinS¹S¹ (TotalHopf→JoinS¹S¹ x))
    ∙∙ TotalHopf→JoinS¹S¹→TotalHopf x
  leftInv IsoS³TotalHopf x =
       cong (fun IsoS³S3 ∘ joinS¹S¹→S³)
            (JoinS¹S¹→TotalHopf→JoinS¹S¹ (S³→joinS¹S¹ (inv IsoS³S3 x)))
    ∙∙ cong (fun IsoS³S3) (S³→joinS¹S¹→S³ (inv IsoS³S3 x))
    ∙∙ Iso.rightInv IsoS³S3 x

ext: agda

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{- Voevodsky's proof that univalence implies funext -}

{-# OPTIONS --cubical --safe #-}

module Cubical.Experiments.FunExtFromUA where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything

variable
 ℓ ℓ' : Level
_∼_ : {X : Type ℓ} {A : X → Type ℓ'} → (f g : (x : X) → A x) → Type (ℓ-max ℓ ℓ')
f ∼ g = ∀ x → f x ≡ g x

funext : ∀ ℓ ℓ' → Type (ℓ-suc(ℓ-max ℓ ℓ'))
funext ℓ ℓ' = {X : Type ℓ} {Y : Type ℓ'} {f g : X → Y} → f ∼ g → f ≡ g

elimEquivFun' : ∀ {ℓ} (P : (A B : Type ℓ) → (A → B) → Type ℓ)
              → (r : (B : Type ℓ) → P B B (λ x → x))
              → (A B : Type ℓ) → (e : A ≃ B) → P A B (e .fst)
elimEquivFun' P r A B = elimEquivFun B (λ A → P A B) (r B) A

pre-comp-is-equiv : (X Y : Type ℓ) (f : X → Y) (Z : Type ℓ)
                  → isEquiv f
                  → isEquiv (λ (g : Y → Z) → g ∘ f)
pre-comp-is-equiv {ℓ} X Y f Z e = elimEquivFun' P r X Y (f , e)
 where
  P : (X Y : Type ℓ) → (X → Y) → Type ℓ
  P X Y f = isEquiv (λ (g : Y → Z) → g ∘ f)
  r : (B : Type ℓ) → P B B (λ x → x)
  r B = idIsEquiv (B → Z)

leftCancellable : {X : Type ℓ} {Y : Type ℓ'} → (X → Y) → Type (ℓ-max ℓ ℓ')
leftCancellable f = ∀ {x x'} → f x ≡ f x' → x ≡ x'

equivLC : {X : Type ℓ} {Y : Type ℓ'} (f : X → Y) → isEquiv f → leftCancellable f
equivLC f e {x} {x'} p i = hcomp (λ j → \ {(i = i0) → secEq (f , e) x j ;
                                           (i = i1) → secEq (f , e) x' j})
                                 (invEq (f , e) (p i))

univalence-gives-funext : funext ℓ' ℓ
univalence-gives-funext {ℓ'} {ℓ} {X} {Y} {f₀} {f₁} = γ
 where
  Δ = Σ[ y₀ ∈ Y ] Σ[ y₁ ∈ Y ] y₀ ≡ y₁

  δ : Y → Δ
  δ y = (y , y , refl)

  π₀ π₁ : Δ → Y
  π₀ (y₀ , y₁ , p) = y₀
  π₁ (y₀ , y₁ , p) = y₁

  δ-is-equiv : isEquiv δ
  δ-is-equiv = isoToIsEquiv (iso δ π₀ ε η)
   where
    η : (y : Y) → π₀ (δ y) ≡ y
    η y = refl
    ε : (d : Δ) → δ (π₀ d) ≡ d
    ε (y₀ , y₁ , p) i = y₀ , p i , λ j → p (i ∧ j)

  φ : (Δ → Y) → (Y → Y)
  φ π = π ∘ δ

  e : isEquiv φ
  e = pre-comp-is-equiv Y Δ δ Y δ-is-equiv

  p : φ π₀ ≡ φ π₁
  p = refl

  q : π₀ ≡ π₁
  q = equivLC φ e p

  g : (h : f₀ ∼ f₁) (π : Δ → Y) (x : X) → Y
  g = λ h π x → π (f₀ x , f₁ x , h x)

  γ : f₀ ∼ f₁ → f₀ ≡ f₁
  γ h = cong (g h) q

  γ' : f₀ ∼ f₁ → f₀ ≡ f₁
  γ' h = f₀                              ≡⟨ refl ⟩
         (λ x → f₀ x)                    ≡⟨ refl ⟩
         (λ x → π₀ (f₀ x , f₁ x , h x))  ≡⟨ cong (g h) q ⟩
         (λ x → π₁ (f₀ x , f₁ x , h x))  ≡⟨ refl ⟩
         (λ x → f₁ x)                    ≡⟨ refl ⟩
         f₁                              ∎

{- Experiment testing univalence via funext -}

private

  data ℕ : Type₀ where
   zero : ℕ
   succ : ℕ → ℕ

  f g : ℕ → ℕ

  f n = n

  g zero = zero
  g (succ n) = succ (g n)

  h : (n : ℕ) → f n ≡ g n
  h zero = refl
  h (succ n) = cong succ (h n)

  p : f ≡ g
  p = univalence-gives-funext h

  five : ℕ
  five = succ (succ (succ (succ (succ zero))))

  a : Σ ℕ (λ n → f n ≡ five)
  a = five , refl

  b : Σ ℕ (λ n → g n ≡ five)
  b = subst (λ - → Σ ℕ (λ n → - n ≡ five)) p a

  c : fst b ≡ five
  c = refl

{- It works, fast. -}

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
{-# OPTIONS --cubical #-}
module _ where

-- Test case by Ulf Norell, 16/09/2020

open import Agda.Primitive.Cubical    renaming (primIMin to _∧_)
open import Agda.Builtin.Cubical.Path using (_≡_)

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

record Pos : Set where
  constructor 1+_
  field unpos : Nat

open Pos

Pos→Nat : Pos → Nat
Pos→Nat (1+ n) = suc n

variable
  A : Set
  x : A

refl : x ≡ x
refl {x = x} i = x

id : Pos → Pos
id n = n

-- (i ∧ j) in the system caused a mishandling of de Bruijn indexes.
foo : (n : Pos) (i j : I) → Nat
foo n i j = primHComp
              (λ k → primPOr (i ∧ j)                (i ∧ j)
                             (λ _ → suc (n .unpos)) (λ _ → suc (n .unpos)))
              (suc (n .unpos))

-- The test triggers normalization to make sure the `primHComp` in
-- `foo` reduces properly.
                             --  v  foil syntactic equality check
test : ∀ n i j → foo n i j ≡ foo (id n) i j
test n i j = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Inductively defined beta-eta-equality
------------------------------------------------------------------------

import Level
open import Data.Universe

module README.DependentlyTyped.Beta-Eta
  (Uni₀ : Universe Level.zero Level.zero)
  where

open import Data.Product renaming (curry to c)
open import Function hiding (_∋_)
import README.DependentlyTyped.Term as Term; open Term Uni₀
import README.DependentlyTyped.Term.Substitution as S; open S Uni₀
import Relation.Binary.PropositionalEquality as P

open P.≡-Reasoning

-- βη-equality.

infixl 9 _·_
infix  4 _≈_
infixr 2 _≈⟨_⟩_

data _≈_ : ∀ {Γ₁ σ₁} → Γ₁ ⊢ σ₁ → ∀ {Γ₂ σ₂} → Γ₂ ⊢ σ₂ → Set where

  -- β and η.

  β : ∀ {Γ sp₁ sp₂} {σ : IType Γ (π sp₁ sp₂)}
      (t₁ : Γ ▻ fst σ ⊢ snd σ) (t₂ : Γ ⊢ fst σ) →
      ƛ t₁ · t₂ ≈ t₁ /⊢ sub t₂
  η : ∀ {Γ sp₁ sp₂ σ} (t : Γ ⊢ (π sp₁ sp₂ , σ)) →
      ƛ ((t /⊢ wk[ fst σ ]) · var zero) ≈ t

  -- The relation is an equivalence (reflexivity is proved below).

  sym    : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁}
             {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂}
           (t₁≈t₂ : t₁ ≈ t₂) → t₂ ≈ t₁
  _≈⟨_⟩_ : ∀ {Γ₁ σ₁} (t₁ : Γ₁ ⊢ σ₁)
             {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂}
             {Γ₃ σ₃} {t₃ : Γ₃ ⊢ σ₃}
           (t₁≈t₂ : t₁ ≈ t₂) (t₂≈t₃ : t₂ ≈ t₃) → t₁ ≈ t₃

  -- The relation is a congruence.

  var : ∀ {Γ₁ σ₁} {x₁ : Γ₁ ∋ σ₁}
          {Γ₂ σ₂} {x₂ : Γ₂ ∋ σ₂}
        (x₁≅x₂ : x₁ ≅-∋ x₂) → var x₁ ≈ var x₂
  ƛ   : ∀ {Γ₁ σ₁ τ₁} {t₁ : Γ₁ ▻ σ₁ ⊢ τ₁}
          {Γ₂ σ₂ τ₂} {t₂ : Γ₂ ▻ σ₂ ⊢ τ₂}
        (t₁≈t₂ : t₁ ≈ t₂) → ƛ t₁ ≈ ƛ t₂
  _·_ : ∀ {Γ₁ sp₁₁ sp₂₁ σ₁}
          {t₁₁ : Γ₁ ⊢ π sp₁₁ sp₂₁ , σ₁} {t₂₁ : Γ₁ ⊢ fst σ₁}
          {Γ₂ sp₁₂ sp₂₂ σ₂}
          {t₁₂ : Γ₂ ⊢ π sp₁₂ sp₂₂ , σ₂} {t₂₂ : Γ₂ ⊢ fst σ₂}
        (t₁₁≈t₁₂ : t₁₁ ≈ t₁₂) (t₂₁≈t₂₂ : t₂₁ ≈ t₂₂) →
        t₁₁ · t₂₁ ≈ t₁₂ · t₂₂

-- Reflexivity.

infix 3 _□

_□ : ∀ {Γ σ} (t : Γ ⊢ σ) → t ≈ t
var x   □ = var P.refl
ƛ t     □ = ƛ (t □)
t₁ · t₂ □ = (t₁ □) · (t₂ □)

abstract

  -- βη-equal terms have the same semantics.

  ≈-sound : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁} {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
            t₁ ≈ t₂ → ⟦ t₁ ⟧ ≅-Value ⟦ t₂ ⟧
  ≈-sound (β t₁ t₂) = begin
    [ c ⟦ t₁ ⟧ ˢ ⟦ t₂ ⟧ ]  ≡⟨ corresponds (app (sub t₂)) t₁ ⟩
    [ ⟦ t₁ /⊢ sub t₂ ⟧  ]  ∎
  ≈-sound (η t) = begin
    [ c (⟦ t /⊢ wk ⟧     ˢ lookup zero) ]  ≡⟨ curry-cong $ ˢ-cong (P.sym $ corresponds (app wk) t)
                                                                  (P.refl {x = [ lookup zero ]}) ⟩
    [ c ((⟦ t ⟧ /̂Val ŵk) ˢ lookup zero) ]  ≡⟨ P.refl ⟩
    [ ⟦ t ⟧                             ]  ∎
  ≈-sound (sym t₁≈t₂)           = P.sym $ ≈-sound t₁≈t₂
  ≈-sound (t₁ ≈⟨ t₁≈t₂ ⟩ t₂≈t₃) = P.trans (≈-sound t₁≈t₂) (≈-sound t₂≈t₃)
  ≈-sound (var P.refl)          = P.refl
  ≈-sound (ƛ t₁≈t₂)             = curry-cong (≈-sound t₁≈t₂)
  ≈-sound (t₁₁≈t₁₂ · t₂₁≈t₂₂)   = ˢ-cong (≈-sound t₁₁≈t₁₂) (≈-sound t₂₁≈t₂₂)

  -- βη-equal terms have identical contexts.

  ≈-⇒-≅-Ctxt : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁} {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
               t₁ ≈ t₂ → Γ₁ ≅-Ctxt Γ₂
  ≈-⇒-≅-Ctxt t₁≈t₂ = P.cong [Value].Γ $ ≈-sound t₁≈t₂

  -- βη-equal terms have identical types.

  ≈-⇒-≅-Type : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁} {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
               t₁ ≈ t₂ → σ₁ ≅-Type σ₂
  ≈-⇒-≅-Type {t₁ = t₁} {t₂ = t₂} t₁≈t₂
    with ⟦ t₂ ⟧ | ≈-sound t₁≈t₂
  ... | .(⟦ t₁ ⟧) | P.refl = P.refl

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
-- Andreas, 2012-10-19 issue #719 blame correct module
-- Andreas, 2017-07-28 point to correct binding site ("as A")

module Issue719 where

  import Common.Size as A
  module M where

  private open module A = M

-- WAS:
-- Duplicate definition of module A. Previous definition of module A
-- at .../Common/Size.agda:7,15-19
-- when scope checking the declaration
--   open module A = M

-- EXPECTED:
-- Duplicate definition of module A. Previous definition of module A
-- at .../Issue719.agda:6,25-26
-- when scope checking the declaration
--   open module A = M

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Categories.Category.Core using (Category)

module Categories.Diagram.Coequalizer {o ℓ e} (𝒞 : Category o ℓ e) where

open Category 𝒞
open HomReasoning
open Equiv

open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞

open import Level
open import Function using (_$_)

private
  variable
    A B C : Obj
    h i j k : A ⇒ B

record IsCoequalizer {E} (f g : A ⇒ B) (arr : B ⇒ E) : Set (o ⊔ ℓ ⊔ e) where
  field
    equality   : arr ∘ f ≈ arr ∘ g
    coequalize : {h : B ⇒ C} → h ∘ f ≈ h ∘ g → E ⇒ C
    universal  : {h : B ⇒ C} {eq : h ∘ f ≈ h ∘ g} → h ≈ coequalize eq ∘ arr
    unique     : {h : B ⇒ C} {i : E ⇒ C} {eq : h ∘ f ≈ h ∘ g} → h ≈ i ∘ arr → i ≈ coequalize eq

  unique′ : (eq eq′ : h ∘ f ≈ h ∘ g) → coequalize eq ≈ coequalize eq′
  unique′ eq eq′ = unique universal

  id-coequalize : id ≈ coequalize equality
  id-coequalize = unique (⟺ identityˡ)

  coequalize-resp-≈ : ∀ {eq :  h ∘ f ≈ h ∘ g} {eq′ : i ∘ f ≈ i ∘ g} →
    h ≈ i → coequalize eq ≈ coequalize eq′
  coequalize-resp-≈ {h = h} {i = i} {eq = eq} {eq′ = eq′} h≈i = unique $ begin
    i                   ≈˘⟨ h≈i ⟩
    h                   ≈⟨ universal ⟩
    coequalize eq ∘ arr ∎

  coequalize-resp-≈′ : (eq :  h ∘ f ≈ h ∘ g) → (eq′ : i ∘ f ≈ i ∘ g) →
    h ≈ i → j ≈ coequalize eq → k ≈ coequalize eq′ → j ≈ k
  coequalize-resp-≈′ {j = j} {k = k} eq eq′ h≈i eqj eqk = begin
    j              ≈⟨ eqj ⟩
    coequalize eq  ≈⟨ coequalize-resp-≈ h≈i ⟩
    coequalize eq′ ≈˘⟨ eqk ⟩
    k              ∎

-- This could be proved via duality, but is easier to just write by hand,
-- as it makes the dependency graph a lot cleaner.
IsCoequalizer⇒Epi : IsCoequalizer h i j → Epi j
IsCoequalizer⇒Epi coeq _ _ eq =
  coequalize-resp-≈′ (extendˡ equality) (extendˡ equality) eq (unique refl) (unique refl)
  where
    open IsCoequalizer coeq

record Coequalizer (f g : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
  field
    {obj} : Obj
    arr   : B ⇒ obj
    isCoequalizer : IsCoequalizer f g arr

  open IsCoequalizer isCoequalizer public

Coequalizer⇒Epi : (e : Coequalizer h i) → Epi (Coequalizer.arr e)
Coequalizer⇒Epi coeq = IsCoequalizer⇒Epi isCoequalizer
  where
    open Coequalizer coeq

-- Proving this via duality arguments is kind of annoying, as ≅ does not behave nicely in
-- concert with op.
up-to-iso : (coe₁ coe₂ : Coequalizer h i) → Coequalizer.obj coe₁ ≅ Coequalizer.obj coe₂
up-to-iso coe₁ coe₂ = record
  { from = repack coe₁ coe₂
  ; to = repack coe₂ coe₁
  ; iso = record
    { isoˡ = repack-cancel coe₂ coe₁
    ; isoʳ = repack-cancel coe₁ coe₂
    }
  }
  where
    open Coequalizer

    repack : (coe₁ coe₂ : Coequalizer h i) → obj coe₁ ⇒ obj coe₂
    repack coe₁ coe₂ = coequalize coe₁ (equality coe₂)

    repack∘ : (coe₁ coe₂ coe₃ : Coequalizer h i) → repack coe₂ coe₃ ∘ repack coe₁ coe₂ ≈ repack coe₁ coe₃
    repack∘ coe₁ coe₂ coe₃ = unique coe₁ (⟺ (glueTrianglesˡ (⟺ (universal coe₂)) (⟺ (universal coe₁)))) -- unique e₃ (⟺ (glueTrianglesʳ (⟺ (universal e₃)) (⟺ (universal e₂))))

    repack-cancel : (e₁ e₂ : Coequalizer h i) → repack e₁ e₂ ∘ repack e₂ e₁ ≈ id
    repack-cancel coe₁ coe₂ = repack∘ coe₂ coe₁ coe₂ ○ ⟺ (id-coequalize coe₂)

IsCoequalizer⇒Coequalizer : IsCoequalizer h i k → Coequalizer h i
IsCoequalizer⇒Coequalizer {k = k} is-coe = record
  { arr = k
  ; isCoequalizer = is-coe
  }

max_stars_repo_name: maxsnew/agda-categories

max_issues_repo_name: maxsnew/agda-categories

max_forks_repo_name: maxsnew/agda-categories


text:
module Numeral.Natural.Relation.Order.Proofs where

import Lvl
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Induction
open import Numeral.Natural.Relation.Order
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Relator
import      Structure.Relator.Names as Names
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Operator.Properties
open import Structure.Relator.Ordering
open import Structure.Relator.Properties
open import Structure.Relator.Properties.Proofs
open import Syntax.Transitivity
open import Type.Properties.MereProposition
open import Type

-- TODO: A method for pattern matching: https://stackoverflow.com/questions/20682013/agda-why-am-i-unable-to-pattern-match-on-refl

instance
  [≤]-succ-injectivity : ∀{x y} → Injective(succ{x}{y})
  Injective.proof [≤]-succ-injectivity [≡]-intro = [≡]-intro

instance
  [≤]-mereProposition : ∀{x y} → MereProposition(x ≤ y)
  MereProposition.uniqueness [≤]-mereProposition {min}    {min}    = [≡]-intro
  MereProposition.uniqueness [≤]-mereProposition {succ x} {succ y} = congruence₁(succ) (MereProposition.uniqueness [≤]-mereProposition {x}{y})

instance
  [≤]-minimum = \{y} → _≤_.min {y}
  [≤]-with-[𝐒] = \{x}{y} ⦃ xy ⦄ → _≤_.succ {x}{y} xy
[<]-minimum = \{y} → succ([≤]-minimum {y})

[≡]-to-[≤] : ∀{x y : ℕ} → (x ≡ y) → (x ≤ y)
[≡]-to-[≤] {𝟎}   {_}    _         = [≤]-minimum
[≡]-to-[≤] {𝐒(x)}{𝐒(y)} [≡]-intro = succ([≡]-to-[≤] {x}{y} [≡]-intro)

[≡]-to-[≥] : ∀{x y : ℕ} → (x ≡ y) → (x ≥ y)
[≡]-to-[≥] = [≡]-to-[≤] ∘ symmetry(_≡_)

[≰]-to-[≢] : ∀{x y : ℕ} → (x ≰ y) → (x ≢ y)
[≰]-to-[≢] = contrapositiveᵣ [≡]-to-[≤]

[≱]-to-[≢] : ∀{x y : ℕ} → (x ≱ y) → (x ≢ y)
[≱]-to-[≢] = contrapositiveᵣ [≡]-to-[≥]

[≤][0]ᵣ : ∀{x : ℕ} → (x ≤ 0) → (x ≡ 0)
[≤][0]ᵣ {𝟎}    (_) = [≡]-intro
[≤][0]ᵣ {𝐒(_)} ()

[≤][0]ᵣ-negation : ∀{x : ℕ} → (𝐒(x) ≰ 0)
[≤][0]ᵣ-negation ()

[≤]-successor : ∀{x y : ℕ} → (x ≤ y) → (x ≤ 𝐒(y))
[≤]-successor {𝟎}   {_}    (_) = [≤]-minimum
[≤]-successor {𝐒(x)}{𝟎}    ()
[≤]-successor {𝐒(x)}{𝐒(y)} (succ proof) = succ([≤]-successor {x}{y} (proof))

[≤]-predecessor : ∀{x y : ℕ} → (𝐒(x) ≤ y) → (x ≤ y)
[≤]-predecessor {x}   {𝟎}    ()
[≤]-predecessor {𝟎}   {𝐒(y)} (_) = [≤]-minimum
[≤]-predecessor {𝐒(x)}{𝐒(y)} (succ proof) = succ([≤]-predecessor {x}{y} (proof))

[≤]-without-[𝐒] : ∀{x y : ℕ} → (𝐒(x) ≤ 𝐒(y)) → (x ≤ y)
[≤]-without-[𝐒] (succ proof) = proof

[≤][𝐒]ₗ : ∀{x : ℕ} → ¬(𝐒(x) ≤ x)
[≤][𝐒]ₗ {𝟎}    (1≤0)    = [≤][0]ᵣ-negation{0}(1≤0)
[≤][𝐒]ₗ {𝐒(n)} (SSn≤Sn) = [≤][𝐒]ₗ {n} ([≤]-without-[𝐒] {𝐒(n)}{n} (SSn≤Sn))

instance
  [≤]-reflexivity : Reflexivity (_≤_)
  Reflexivity.proof([≤]-reflexivity) = [≡]-to-[≤] [≡]-intro

instance
  [≤]-transitivity : Transitivity (_≤_)
  Transitivity.proof([≤]-transitivity) = proof where
    proof : Names.Transitivity (_≤_)
    proof {𝟎}   {_}   {_} (_)(_) = [≤]-minimum
    proof {𝐒(a)}{𝐒(b)}{𝐒(c)} (succ proofₗ) (succ proofᵣ ) =
      succ(proof {a}{b}{c} (proofₗ) (proofᵣ))

instance
  [≤]-antisymmetry : Antisymmetry (_≤_) (_≡_)
  Antisymmetry.proof([≤]-antisymmetry) = proof where
    proof : Names.Antisymmetry (_≤_) (_≡_)
    proof {𝟎}    {𝟎}    (_) (_) = [≡]-intro
    proof {𝐒(_)} {𝟎}    ()
    proof {𝟎}    {𝐒(_)} (_) ()
    proof {𝐒(a)} {𝐒(b)} (succ proofₗ) (succ proofᵣ) =
      [≡]-with(𝐒) (proof {a}{b} proofₗ proofᵣ)

instance
  [≤]-totality : ConverseTotal(_≤_)
  ConverseTotal.proof([≤]-totality) = proof where
    proof : Names.ConverseTotal(_≤_)
    proof {𝟎}   {𝟎}    = [∨]-introₗ ([≡]-to-[≤] [≡]-intro)
    proof {𝐒(a)}{𝟎}    = [∨]-introᵣ ([≤]-minimum)
    proof {𝟎}   {𝐒(b)} = [∨]-introₗ ([≤]-minimum)
    proof {𝐒(a)}{𝐒(b)} = [∨]-elim ([∨]-introₗ ∘ (proof ↦ [≤]-with-[𝐒] {a}{b} ⦃ proof ⦄)) ([∨]-introᵣ ∘ (proof ↦ [≤]-with-[𝐒] {b}{a} ⦃ proof ⦄)) (proof {a}{b})

instance
  [≤]-weakPartialOrder : Weak.PartialOrder (_≤_) (_≡_)
  [≤]-weakPartialOrder = record{}

instance
  [≤]-weakTotalOrder : Weak.TotalOrder (_≤_) (_≡_)
  [≤]-weakTotalOrder = record{}

instance
  [≥]-reflexivity : Reflexivity (_≥_)
  Reflexivity.proof([≥]-reflexivity) = Reflexivity.proof([≤]-reflexivity)

instance
  [≥]-transitivity : Transitivity (_≥_)
  Transitivity.proof([≥]-transitivity) = swap(Transitivity.proof([≤]-transitivity))

instance
  [≥]-antisymmetry : Antisymmetry (_≥_) (_≡_)
  Antisymmetry.proof([≥]-antisymmetry) = swap(Antisymmetry.proof([≤]-antisymmetry))

instance
  [≥]-totality : ConverseTotal(_≥_)
  ConverseTotal.proof([≥]-totality) = ConverseTotal.proof([≤]-totality)

instance
  [≥]-weakPartialOrder : Weak.PartialOrder (_≥_) (_≡_)
  [≥]-weakPartialOrder = record{}

instance
  [≥]-weakTotalOrder : Weak.TotalOrder (_≥_) (_≡_)
  [≥]-weakTotalOrder = record{}

[≥]-to-[≮] : ∀{a b : ℕ} → (a ≮ b) ← (a ≥ b)
[≥]-to-[≮] {a}{b} (b≤a) (𝐒a≤b) = [≤][𝐒]ₗ (transitivity(_≤_) {𝐒(a)}{b}{a} (𝐒a≤b) (b≤a))

[≤]-to-[≯] : ∀{a b : ℕ} → (a ≯ b) ← (a ≤ b)
[≤]-to-[≯] {a}{b} (a≤b) (𝐒b≤a) = [≥]-to-[≮] {b}{a} (a≤b) (𝐒b≤a)

[>]-to-[≰] : ∀{a b : ℕ} → (a ≰ b) ← (a > b)
[>]-to-[≰] {a}{b} (𝐒b≤a) (a≤b) = [≤]-to-[≯] (a≤b) (𝐒b≤a)

[<]-to-[≱] : ∀{a b : ℕ} → (a ≱ b) ← (a < b)
[<]-to-[≱] {a}{b} (𝐒a≤b) (b≤a) = [≥]-to-[≮] (b≤a) (𝐒a≤b)

[<]-to-[≢] : ∀{a b : ℕ} → (a < b) → (a ≢ b)
[<]-to-[≢] = [≱]-to-[≢] ∘ [<]-to-[≱]

[>]-to-[≢] : ∀{a b : ℕ} → (a > b) → (a ≢ b)
[>]-to-[≢] = [≰]-to-[≢] ∘ [>]-to-[≰]

[<][0]ᵣ : ∀{x : ℕ} → (x ≮ 0)
[<][0]ᵣ = [≤][0]ᵣ-negation

instance
  [<]-irreflexivity : Irreflexivity (_<_)
  Irreflexivity.proof([<]-irreflexivity) = [≤][𝐒]ₗ

instance
  [<]-transitivity : Transitivity (_<_)
  Transitivity.proof([<]-transitivity) {x}{y}{z} (l) (r) = Transitivity.proof([≤]-transitivity) {𝐒(x)} {𝐒(y)} {z} ([≤]-successor (l)) (r)

instance
  [<]-asymmetry : Asymmetry (_<_)
  Asymmetry.proof([<]-asymmetry) (l) (r) = Irreflexivity.proof([<]-irreflexivity) (Transitivity.proof([<]-transitivity) (l) (r))

instance
  [<]-converseTrichotomy : ConverseTrichotomy(_<_)(_≡_)
  ConverseTrichotomy.proof [<]-converseTrichotomy = p where
    p : Names.ConverseTrichotomy(_<_)(_≡_)
    p {𝟎}   {𝟎}   = [∨]-introₗ ([∨]-introᵣ [≡]-intro)
    p {𝟎}   {𝐒 y} = [∨]-introₗ ([∨]-introₗ [≤]-with-[𝐒])
    p {𝐒 x} {𝟎}   = [∨]-introᵣ [≤]-with-[𝐒]
    p {𝐒 x} {𝐒 y} with p {x} {y}
    ... | [∨]-introₗ ([∨]-introₗ (succ xy)) = [∨]-introₗ ([∨]-introₗ (succ (succ xy)))
    ... | [∨]-introₗ ([∨]-introᵣ [≡]-intro) = [∨]-introₗ ([∨]-introᵣ [≡]-intro)
    ... | [∨]-introᵣ (succ xy)              = [∨]-introᵣ (succ (succ xy))

instance
  [<]-strictPartialOrder : Strict.PartialOrder (_<_)
  [<]-strictPartialOrder = record{}

instance
  [<]-strictTotalOrder : Strict.TotalOrder (_<_)(_≡_)
  [<]-strictTotalOrder = record{}

instance
  [>]-irreflexivity : Irreflexivity (_>_)
  Irreflexivity.proof([>]-irreflexivity) = Irreflexivity.proof([<]-irreflexivity)

instance
  [>]-transitivity : Transitivity (_>_)
  Transitivity.proof([>]-transitivity) = swap(Transitivity.proof([<]-transitivity))

instance
  [>]-asymmetry : Asymmetry (_>_)
  Asymmetry.proof([>]-asymmetry) = swap(Asymmetry.proof([<]-asymmetry))

instance
  [>]-strictOrder : Strict.PartialOrder (_>_)
  [>]-strictOrder = record{}

[<]-of-[𝐒] : ∀{x : ℕ} → (x < 𝐒(x))
[<]-of-[𝐒] = reflexivity(_≤_)

[<]-of-[𝟎][𝐒] : ∀{x : ℕ} → (𝟎 < 𝐒(x))
[<]-of-[𝟎][𝐒] {𝟎} = [<]-of-[𝐒]
[<]-of-[𝟎][𝐒] {𝐒 x} = succ([≤]-minimum)

instance
  [≤]-of-[𝐒] : ∀{x : ℕ} → (x ≤ 𝐒(x))
  [≤]-of-[𝐒] = [≤]-successor(reflexivity(_≤_))

[<][≢]-equivalence : ∀{x} → (x > 0) ↔ (x ≢ 0)
[<][≢]-equivalence {x} = [↔]-intro (l{x}) (r{x}) where
  l : ∀{x} → (x > 0) ← (x ≢ 0)
  l{𝟎}    (x≢𝟎)  = [⊥]-elim((x≢𝟎)([≡]-intro))
  l{𝐒(x)} (𝐒x≢𝟎) = succ([≤]-minimum)

  r : ∀{x} → (x > 0) → (x ≢ 0)
  r{𝟎}    ()
  r{𝐒(x)} (𝟏≤𝐒x) (𝐒x≡𝟎) with [≡]-substitutionᵣ (𝐒x≡𝟎) {expr ↦ 1 ≤ expr} (𝟏≤𝐒x)
  ... | ()

[≤]-to-[<][≡] : ∀{a b : ℕ} → (a ≤ b) → (a < b)∨(a ≡ b)
[≤]-to-[<][≡] {𝟎}   {𝟎}    ([≤]-minimum)    = [∨]-introᵣ([≡]-intro)
[≤]-to-[<][≡] {𝟎}   {𝐒(b)} ([≤]-minimum)    = [∨]-introₗ([<]-minimum)
[≤]-to-[<][≡] {𝐒(a)}{𝐒(b)} (succ(a≤b)) with [≤]-to-[<][≡] {a}{b} (a≤b)
... | [∨]-introₗ(a<b) = [∨]-introₗ(succ(a<b))
... | [∨]-introᵣ(a≡b) = [∨]-introᵣ([≡]-with(𝐒) (a≡b))

[≮][≢]-to-[≰] : ∀{a b : ℕ} → (a ≮ b) → (a ≢ b) → (a ≰ b)
[≮][≢]-to-[≰] (a≮b) (a≢b) (a≤b) with [≤]-to-[<][≡] (a≤b)
... | [∨]-introₗ (a<b) = a≮b a<b
... | [∨]-introᵣ (a≡b) = a≢b a≡b

[<][≡]-to-[≤] : ∀{a b : ℕ} → (a < b)∨(a ≡ b) → (a ≤ b)
[<][≡]-to-[≤] {a}   {.a}   ([∨]-introᵣ([≡]-intro)) = [≡]-to-[≤] ([≡]-intro)
[<][≡]-to-[≤] {a}   {b}    ([∨]-introₗ(a<b))       = [≤]-predecessor (a<b)

instance
  [<][≤]-sub : (_<_) ⊆₂ (_≤_)
  [<][≤]-sub = intro [≤]-predecessor

instance
  [>][≥]-sub : (_>_) ⊆₂ (_≥_)
  [>][≥]-sub = intro(sub₂(_<_)(_≤_))

[≰]-to-[≮] : ∀{x y : ℕ} → (x ≰ y) → (x ≮ y)
[≰]-to-[≮] = contrapositiveᵣ (sub₂(_<_)(_≤_))

[≥]-to-[>][≡] : ∀{a b : ℕ} → (a ≥ b) → (a > b)∨(a ≡ b)
[≥]-to-[>][≡] {a}{b} (proof) with [≤]-to-[<][≡] {b}{a} (proof)
... | [∨]-introₗ(a<b) = [∨]-introₗ(a<b)
... | [∨]-introᵣ(b≡a) = [∨]-introᵣ(symmetry(_≡_) (b≡a))

[<]-trichotomy : ∀{x y} → (x < y) ∨ (x ≡ y) ∨ (x > y)
[<]-trichotomy {x}{y} with converseTotal(_≤_) ⦃ [≤]-totality ⦄
[<]-trichotomy {x}{y} | [∨]-introₗ x≤y with [≤]-to-[<][≡] {x}{y} x≤y
[<]-trichotomy {x}{y} | [∨]-introₗ x≤y | [∨]-introₗ x<y = [∨]-introₗ ([∨]-introₗ x<y)
[<]-trichotomy {x}{y} | [∨]-introₗ x≤y | [∨]-introᵣ x≡y = [∨]-introₗ ([∨]-introᵣ x≡y)
[<]-trichotomy {x}{y} | [∨]-introᵣ y≤x with [≥]-to-[>][≡] {x}{y} y≤x
[<]-trichotomy {x}{y} | [∨]-introᵣ y≤x | [∨]-introₗ y<x = [∨]-introᵣ y<x
[<]-trichotomy {x}{y} | [∨]-introᵣ y≤x | [∨]-introᵣ y≡x = [∨]-introₗ ([∨]-introᵣ y≡x)

[≤][>]-dichotomy : ∀{x y} → (x ≤ y) ∨ (x > y)
[≤][>]-dichotomy {x}{y} with [<]-trichotomy {x}{y}
[≤][>]-dichotomy {x} {y} | [∨]-introₗ ([∨]-introₗ x<y) = [∨]-introₗ(sub₂(_<_)(_≤_) x<y)
[≤][>]-dichotomy {x} {y} | [∨]-introₗ ([∨]-introᵣ x≡y) = [∨]-introₗ(sub₂(_≡_)(_≤_) x≡y)
[≤][>]-dichotomy {x} {y} | [∨]-introᵣ x>y              = [∨]-introᵣ(x>y)

[<][≥]-dichotomy : ∀{x y} → (x < y) ∨ (x ≥ y)
[<][≥]-dichotomy {x}{y} = [∨]-symmetry([≤][>]-dichotomy {y}{x})

[≯][≢]-to-[≱] : ∀{a b : ℕ} → (a ≯ b) → (a ≢ b) → (a ≱ b)
[≯][≢]-to-[≱] (a≯b) (a≢b) (a≥b) with [≥]-to-[>][≡] (a≥b)
... | [∨]-introₗ (a>b) = a≯b a>b
... | [∨]-introᵣ (a≡b) = a≢b a≡b

[>][≡]-to-[≥] : ∀{a b : ℕ} → (a > b)∨(a ≡ b) → (a ≥ b)
[>][≡]-to-[≥] {a}{b} ([∨]-introₗ(a<b)) = [<][≡]-to-[≤] {b}{a} ([∨]-introₗ(a<b))
[>][≡]-to-[≥] {a}{b} ([∨]-introᵣ(b≡a)) = [<][≡]-to-[≤] {b}{a} ([∨]-introᵣ(symmetry(_≡_)(b≡a)))

[>]-to-[≥] : ∀{a b : ℕ} → (a > b) → (a ≥ b)
[>]-to-[≥] {a}{b} (a<b) = [<][≡]-to-[≤] {b}{a} ([∨]-introₗ(a<b))

[≱]-to-[≯] : ∀{x y : ℕ} → (x ≱ y) → (x ≯ y)
[≱]-to-[≯] = contrapositiveᵣ [>]-to-[≥]

[≮][≯]-to-[≡] : ∀{a b : ℕ} → (a ≮ b) → (a ≯ b) → (a ≡ b)
[≮][≯]-to-[≡] {a}{b} (a≮b) (a≯b) with [<]-trichotomy {a}{b}
... | [∨]-introₗ ([∨]-introₗ a<b) = [⊥]-elim(a≮b a<b)
... | [∨]-introₗ ([∨]-introᵣ a≡b) = a≡b
... | [∨]-introᵣ b<a              = [⊥]-elim(a≯b b<a)

[≮][≢][≯]-not : ∀{a b : ℕ} → (a ≮ b) → (a ≢ b) → (a ≯ b) → ⊥
[≮][≢][≯]-not {a}{b} (a≮b) (a≢b) (a≯b) with [<]-trichotomy {a}{b}
... | [∨]-introₗ ([∨]-introₗ a<b) = a≮b a<b
... | [∨]-introₗ ([∨]-introᵣ a≡b) = a≢b a≡b
... | [∨]-introᵣ b<a              = a≯b b<a

[≰][≯]-not : ∀{a b : ℕ} → (a ≰ b) → (a ≯ b) → ⊥
[≰][≯]-not {a}{b} (a≰b) (a≯b) = [≮][≢][≯]-not ([≰]-to-[≮] a≰b) ([≰]-to-[≢] a≰b) (a≯b)

[≮][≱]-not : ∀{a b : ℕ} → (a ≮ b) → (a ≱ b) → ⊥
[≮][≱]-not {a}{b} (a≮b) (a≱b) = [≮][≢][≯]-not (a≮b) ([≱]-to-[≢] a≱b) ([≱]-to-[≯] a≱b)

[<]-non-zero-existence : ∀{a b : ℕ} → (a < b) → (𝟎 < b)
[<]-non-zero-existence (succ _) = [<]-of-[𝟎][𝐒]

[≢]-to-[<]-of-0ᵣ : ∀{n} → (n ≢ 0) → (0 < n)
[≢]-to-[<]-of-0ᵣ {𝟎}   p with () ← p [≡]-intro
[≢]-to-[<]-of-0ᵣ {𝐒 n} p = succ min

[≤][≢]-to-[<] : ∀{a b : ℕ} → (a ≤ b) → (a ≢ b) → (a < b)
[≤][≢]-to-[<] {.𝟎}     {b}      min       ne = [≢]-to-[<]-of-0ᵣ (ne ∘ symmetry(_≡_))
[≤][≢]-to-[<] {.(𝐒 _)} {.(𝐒 _)} (succ lt) ne = succ([≤][≢]-to-[<] lt (ne ∘ congruence₁(𝐒)))

instance
  [≤][≡]-subtransitivityₗ : Subtransitivityₗ(_≤_)(_≡_)
  [≤][≡]-subtransitivityₗ = subrelation-transitivity-to-subtransitivityₗ

instance
  [≤][≡]-subtransitivityᵣ : Subtransitivityᵣ(_≤_)(_≡_)
  [≤][≡]-subtransitivityᵣ = subrelation-transitivity-to-subtransitivityᵣ

instance
  [≥][≡]-subtransitivityₗ : Subtransitivityₗ(_≥_)(_≡_)
  [≥][≡]-subtransitivityₗ = subrelation-transitivity-to-subtransitivityₗ

instance
  [≥][≡]-subtransitivityᵣ : Subtransitivityᵣ(_≥_)(_≡_)
  [≥][≡]-subtransitivityᵣ = subrelation-transitivity-to-subtransitivityᵣ

instance
  [<][≤]-subtransitivityₗ : Subtransitivityₗ(_≤_)(_<_)
  [<][≤]-subtransitivityₗ = subrelation-transitivity-to-subtransitivityₗ

instance
  [<][≤]-subtransitivityᵣ : Subtransitivityᵣ(_≤_)(_<_)
  [<][≤]-subtransitivityᵣ = subrelation-transitivity-to-subtransitivityᵣ

instance
  [>][≥]-subtransitivityₗ : Subtransitivityₗ(_≥_)(_>_)
  [>][≥]-subtransitivityₗ = subrelation-transitivity-to-subtransitivityₗ

instance
  [>][≥]-subtransitivityᵣ : Subtransitivityᵣ(_≥_)(_>_)
  [>][≥]-subtransitivityᵣ = subrelation-transitivity-to-subtransitivityᵣ

instance
  [>][≡]-subtransitivityₗ : Subtransitivityₗ(_>_)(_≡_)
  Subtransitivityₗ.proof [>][≡]-subtransitivityₗ = substitute₂ₗ(_>_) ∘ symmetry(_≡_)

instance
  [>][≡]-subtransitivityᵣ : Subtransitivityᵣ(_>_)(_≡_)
  Subtransitivityᵣ.proof [>][≡]-subtransitivityᵣ = swap(substitute₂ᵣ(_>_))

instance
  [<][≡]-subtransitivityₗ : Subtransitivityₗ(_<_)(_≡_)
  Subtransitivityₗ.proof [<][≡]-subtransitivityₗ = substitute₂ₗ(_<_) ∘ symmetry(_≡_)

instance
  [<][≡]-subtransitivityᵣ : Subtransitivityᵣ(_<_)(_≡_)
  Subtransitivityᵣ.proof [<][≡]-subtransitivityᵣ = swap(substitute₂ᵣ(_<_))

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:
-- Andreas, 2014-05-17

open import Common.Prelude
open import Common.Equality

postulate
  bla : ∀ x → x ≡ zero
  P   : Nat → Set
  p   : P zero

f : ∀ x → P x
f x rewrite bla {!!} = {!!}

-- Expected: two interaction points!


text:
-- Andreas, 2018-11-03, issue #3364
-- Andreas, 2019-02-23, issue #3457
--
-- Better error when trying to import with new qualified module name.

open import Agda.Builtin.Nat as Builtin.Nat

-- WAS: Error:
-- Not in scope:
--   as at ...
-- when scope checking as

-- NOW: Warning
-- `as' must be followed by an identifier; a qualified name is not allowed here
-- when scope checking the declaration
--   open import Agda.Builtin.Nat as Builtin.Nat

import Agda.Builtin.Sigma as .as

-- `as' must be followed by an identifier
-- when scope checking the declaration
--   import Agda.Builtin.Sigma as .as

import Agda.Builtin.String as _

-- `as' must be followed by an identifier; an underscore is not allowed here
-- when scope checking the declaration
--   import Agda.Builtin.String as _

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
module _ where

record Semiring (A : Set) : Set where
  infixl 6 _+_
  field _+_ : A → A → A

open Semiring {{...}} public

infix 4 _≡_

postulate
  Nat Bool  : Set
  _≡_   : Nat → Nat → Set
  refl  : ∀ {x} → x ≡ x
  to    : ∀ {x} (y : Nat) → x ≡ y
  trans : {x y z : Nat} → x ≡ y → y ≡ z → x ≡ z

  instance _ : Semiring Nat
           _ : Semiring Bool

bad : (a b c : Nat) → a + b ≡ c + a
bad a b c =
  trans (to (a + c)) refl

-- Should complain about a != c when checking refl, not a missing instance Semiring Nat.