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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Id {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
import Definition.Typed.Weakening as Twk
open import Definition.Typed.EqualityRelation
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
import Definition.LogicalRelation.Weakening as Lwk
open import Definition.LogicalRelation.Substitution.Properties
import Definition.LogicalRelation.Substitution.Irrelevance as S
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Weakening
-- open import Definition.LogicalRelation.Substitution.Introductions.Nat
open import Definition.LogicalRelation.Substitution.Introductions.Empty
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.Idlemmas
open import Definition.LogicalRelation.Substitution.Introductions.IdUniv
open import Definition.LogicalRelation.Substitution.Introductions.IdNat
open import Definition.LogicalRelation.Substitution.MaybeEmbed
-- open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.Introductions.Universe

open import Tools.Product
open import Tools.Empty
import Tools.Unit as TU
import Tools.PropositionalEquality as PE
import Data.Nat as Nat

[Id] : ∀ {A t u Γ l lA}
         (⊢Γ : ⊢ Γ)
         ([A] : Γ ⊩⟨ l ⟩ A ^ [ ! , ι lA ])
         ([t] : Γ ⊩⟨ l ⟩ t ∷ A ^ [ ! , ι lA ] / [A])
         ([u] : Γ ⊩⟨ l ⟩ u ∷ A ^ [ ! , ι lA ] / [A])
       → Γ ⊩⟨ l ⟩ Id A t u ^ [ % , ι lA ]
[IdExt] : ∀ {A B t v u w Γ l l' lA}
         (⊢Γ : ⊢ Γ)
         ([A] : Γ ⊩⟨ l ⟩ A ^ [ ! , ι lA ])
         ([B] : Γ ⊩⟨ l' ⟩ B ^ [ ! , ι lA ])
         ([A≡B] : Γ ⊩⟨ l ⟩ A ≡ B ^ [ ! , ι lA ] / [A])
         ([t] : Γ ⊩⟨ l ⟩ t ∷ A ^ [ ! , ι lA ] / [A])
         ([v] : Γ ⊩⟨ l' ⟩ v ∷ B ^ [ ! , ι lA ] / [B])
         ([t≡v] : Γ ⊩⟨ l ⟩ t ≡ v ∷ A ^ [ ! , ι lA ] / [A])
         ([u] : Γ ⊩⟨ l ⟩ u ∷ A ^ [ ! , ι lA ] / [A])
         ([w] : Γ ⊩⟨ l' ⟩ w ∷ B ^ [ ! , ι lA ] / [B])
         ([u≡w] : Γ ⊩⟨ l ⟩ u ≡ w ∷ A ^ [ ! , ι lA ] / [A])
       → Γ ⊩⟨ l ⟩ Id A t u ≡ Id B v w ^ [ % , ι lA ] / [Id] ⊢Γ [A] [t] [u]
[IdExtShape] : ∀ {A B t v u w Γ l l' lA}
         (⊢Γ : ⊢ Γ)
         ([A] : Γ ⊩⟨ l ⟩ A ^ [ ! , ι lA ])
         ([B] : Γ ⊩⟨ l' ⟩ B ^ [ ! , ι lA ])
         (ShapeA : ShapeView Γ l l' A B [ ! , ι lA ] [ ! , ι lA ] [A] [B])
         ([A≡B] : Γ ⊩⟨ l ⟩ A ≡ B ^ [ ! , ι lA ] / [A])
         ([t] : Γ ⊩⟨ l ⟩ t ∷ A ^ [ ! , ι lA ] / [A])
         ([v] : Γ ⊩⟨ l' ⟩ v ∷ B ^ [ ! , ι lA ] / [B])
         ([t≡v] : Γ ⊩⟨ l ⟩ t ≡ v ∷ A ^ [ ! , ι lA ] / [A])
         ([u] : Γ ⊩⟨ l ⟩ u ∷ A ^ [ ! , ι lA ] / [A])
         ([w] : Γ ⊩⟨ l' ⟩ w ∷ B ^ [ ! , ι lA ] / [B])
         ([u≡w] : Γ ⊩⟨ l ⟩ u ≡ w ∷ A ^ [ ! , ι lA ] / [A])
       → Γ ⊩⟨ l ⟩ Id A t u ≡ Id B v w ^ [ % , ι lA ] / [Id] ⊢Γ [A] [t] [u]

[Id] ⊢Γ (ℕᵣ [[ ⊢A , ⊢B , D ]]) [t] [u] = [Id]ℕGen ⊢Γ [[ ⊢A , ⊢B , D ]] [t] [u]

[Id] ⊢Γ (Uᵣ (Uᵣ r ¹ l< () d)) [t] [u]

[Id] {A} {t} {u} {Γ} {ι .¹} {.¹} ⊢Γ (Uᵣ (Uᵣ rU ⁰ emb< PE.refl [[ ⊢A , ⊢B , D ]])) [t] [u] = [Id]UGen {A} {t} {u} {Γ} ⊢Γ (Uᵣ rU ⁰ emb< PE.refl [[ ⊢A , ⊢B , D ]]) [t] [u]

[Id] {A} {t} {u} {Γ} {l} {lA} ⊢Γ (ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K) [t] [u] =
  let
    [A] = ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K
    ⊢tA = escapeTerm {l = l} [A] [t]
    ⊢uA = escapeTerm {l = l} [A] [u]
    [K] = neu {l = l} neK ⊢B K≡K
    [A]′ , [A≡K] = redSubst* D [K]
    [t:K] = convTerm₁ [A]′ [K] [A≡K] (irrelevanceTerm [A] [A]′ [t])
    [u:K] = convTerm₁ [A]′ [K] [A≡K] (irrelevanceTerm [A] [A]′ [u])
    t≡t = escapeTermEq [K] (reflEqTerm [K] [t:K])
    u≡u = escapeTermEq [K] (reflEqTerm [K] [u:K])
  in ne′ (Id K t u) (redSProp (IdRed*Term ⊢tA ⊢uA [[ ⊢A , ⊢B , D ]])) (Idₙ neK) (~-Id K≡K t≡t u≡u)

[Id] {A} {t} {u} {Γ} {l} {lA} ⊢Γ (Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext)
  (f , [[ ⊢t , ⊢f , Df ]] , funf , f≡f , [fext] , [f]) (g , [[ ⊢u , ⊢g , Dg ]] , fung , g≡g , [gext] , [g]) =
  let
    ⊢tA = conv ⊢t (sym (subset* D))
    ⊢uA = conv ⊢u (sym (subset* D))

    [F0] : Γ ⊩⟨ l ⟩ F ^ [ rF , ι lF ]
    [F0] = PE.subst (λ X → Γ ⊩⟨ l ⟩ X ^ [ rF , ι lF ]) (wk-id F) ([F] Twk.id ⊢Γ)

    ⊢idG : Γ ∙ F ^ [ rF , ι lF ] ⊢ Id G (wk1 t ∘ var 0 ^ lA) (wk1 u ∘ var 0 ^ lA) ^ [ % , ι lG ]
    ⊢idG = let
        ⊢t∘0 = PE.subst (λ X → _ ⊢ wk1 t ∘ var 0 ^ _ ∷ X ^ [ ! , ι lG ]) (wkSingleSubstId G)
          (Twk.wkTerm (Twk.step Twk.id) (⊢Γ ∙ ⊢F) ⊢t ∘ⱼ var (⊢Γ ∙ ⊢F) here)
        ⊢u∘0 = PE.subst (λ X → _ ⊢ wk1 u ∘ var 0 ^ _ ∷ X ^ [ ! , ι lG ]) (wkSingleSubstId G)
          (Twk.wkTerm (Twk.step Twk.id) (⊢Γ ∙ ⊢F) ⊢u ∘ⱼ var (⊢Γ ∙ ⊢F) here)
      in univ (Idⱼ (un-univ ⊢G) ⊢t∘0 ⊢u∘0)

    ⊢funext : Γ ⊢ Π F ^ rF ° lF ▹ (Id G ((wk1 t) ∘ (var 0) ^ lA) ((wk1 u) ∘ (var 0) ^ lA)) ° lG ° lA ^ [ % , ι lA ]
    ⊢funext = univ (Πⱼ lF≤ ▹ lG≤ ▹ un-univ ⊢F ▹ un-univ ⊢idG)

    Did : Γ ⊢ Id A t u ⇒* Π F ^ rF ° lF ▹ (Id G ((wk1 t) ∘ (var 0) ^ lA) ((wk1 u) ∘ (var 0) ^ lA)) ° lG ° lA ^ [ % , ι lA ]
    Did =  IdRed* ⊢tA ⊢uA D ⇨* (univ (Id-Π lF≤ lG≤ (un-univ ⊢F) (un-univ ⊢G) ⊢t ⊢u) ⇨ id ⊢funext)

    [idG] : ∀ {ρ Δ a}
          → ([ρ] : Twk._∷_⊆_ ρ Δ Γ) → (⊢Δ : ⊢ Δ)
          → (Δ ⊩⟨ l ⟩ a ∷ wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
          → Δ ⊩⟨ l ⟩ wk (lift ρ) (Id G (wk1 t ∘ var 0 ^ lA) (wk1 u ∘ var 0 ^ lA)) [ a ] ^ [ % , ι lG ]
    [idG] {ρ} {Δ} {a} [ρ] ⊢Δ [a] =
      let
        [t∘a] : Δ ⊩⟨ l ⟩ wk ρ t ∘ a ^ lA ∷ wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [G] [ρ] ⊢Δ [a]
        [t∘a] = proj₁ (redSubst*Term
          (appRed* (escapeTerm ([F] [ρ] ⊢Δ) [a]) (Twk.wkRed*Term [ρ] ⊢Δ Df))
          ([G] [ρ] ⊢Δ [a]) ([f] [ρ] ⊢Δ [a]))
        [u∘a] : Δ ⊩⟨ l ⟩ wk ρ u ∘ a ^ lA ∷ wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [G] [ρ] ⊢Δ [a]
        [u∘a] = proj₁ (redSubst*Term
          (appRed* (escapeTerm ([F] [ρ] ⊢Δ) [a]) (Twk.wkRed*Term [ρ] ⊢Δ Dg))
          ([G] [ρ] ⊢Δ [a]) ([g] [ρ] ⊢Δ [a]))
        [Id] : Δ ⊩⟨ l ⟩ (Id (wk (lift ρ) G [ a ]) (wk ρ t ∘ a ^ lA) (wk ρ u ∘ a ^ lA)) ^ [ % , ι lG ]
        [Id] = [Id] ⊢Δ ([G] [ρ] ⊢Δ [a]) [t∘a] [u∘a]
      in PE.subst₂ (λ X Y → Δ ⊩⟨ l ⟩ (Id _ (X ∘ a ^ lA) (Y ∘ a ^ lA)) ^ [ % , ι lG ]) (PE.sym (irrelevant-subst′ ρ t a)) (PE.sym (irrelevant-subst′ ρ u a)) [Id]

    [idG0] : Γ ∙ F ^ [ rF , ι lF ] ⊩⟨ l ⟩ (Id G (wk1 t ∘ var 0 ^ lA) (wk1 u ∘ var 0 ^ lA)) ^ [ % , ι lG ]
    [idG0] = PE.subst₃ (λ X Y Z → _ ⊩⟨ l ⟩ (Id X (Y ∘ var 0 ^ lA) (Z ∘ var 0 ^ lA)) ^ _)
      (wkSingleSubstId G) (wkSingleSubstId (wk1 t)) (wkSingleSubstId (wk1 u))
      ([idG] {step id} {Γ ∙ F ^ [ rF , ι lF ]} {var 0} (Twk.step Twk.id)
       (⊢Γ ∙ ⊢F) (neuTerm ([F] (Twk.step Twk.id) (⊢Γ ∙ ⊢F)) (var 0)
         (var (⊢Γ ∙ ⊢F) here) (~-var (var (⊢Γ ∙ ⊢F) here))))

    [idGext] : ∀ {ρ Δ a b}
          → ([ρ] : Twk._∷_⊆_ ρ Δ Γ)
          → (⊢Δ : ⊢ Δ)
          → ([a] : Δ ⊩⟨ l ⟩ a ∷ wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
          → ([b] : Δ ⊩⟨ l ⟩ b ∷ wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
          → ([a≡b] : Δ ⊩⟨ l ⟩ a ≡ b ∷ wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
          → Δ ⊩⟨ l ⟩ wk (lift ρ) (Id G (wk1 t ∘ var 0 ^ lA) (wk1 u ∘ var 0 ^ lA)) [ a ] ≡ wk (lift ρ) (Id G (wk1 t ∘ var 0 ^ lA) (wk1 u ∘ var 0 ^ lA)) [ b ] ^ [ % , ι lG ] / [idG] [ρ] ⊢Δ [a]
    [idGext] {ρ} {Δ} {a} {b} [ρ] ⊢Δ [a] [b] [a≡b] =
      let
        [Ga] = [G] [ρ] ⊢Δ [a]
        [Gb] = [G] [ρ] ⊢Δ [b]
        [t∘a] , [ta≡fa] = redSubst*Term
          (appRed* (escapeTerm ([F] [ρ] ⊢Δ) [a]) (Twk.wkRed*Term [ρ] ⊢Δ Df))
          [Ga] ([f] [ρ] ⊢Δ [a])
        [u∘a] , [ua≡ga] = redSubst*Term
          (appRed* (escapeTerm ([F] [ρ] ⊢Δ) [a]) (Twk.wkRed*Term [ρ] ⊢Δ Dg))
          [Ga] ([g] [ρ] ⊢Δ [a])
        [Ga≡Gb] : Δ ⊩⟨ l ⟩ wk (lift ρ) G [ a ] ≡ wk (lift ρ) G [ b ] ^ [ ! , ι lG ] / [Ga]
        [Ga≡Gb] = G-ext [ρ] ⊢Δ [a] [b] [a≡b]
        [t∘b:Gb] , [tb≡fb:Gb] = redSubst*Term
          (appRed* (escapeTerm ([F] [ρ] ⊢Δ) [b]) (Twk.wkRed*Term [ρ] ⊢Δ Df))
          [Gb] ([f] [ρ] ⊢Δ [b])
        [t∘b] : Δ ⊩⟨ l ⟩ wk ρ t ∘ b ^ lA ∷ wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [Ga]
        [t∘b] = convTerm₂ [Ga] [Gb] [Ga≡Gb] [t∘b:Gb]
        [u∘b:Gb] , [ub≡gb:Gb] = redSubst*Term
          (appRed* (escapeTerm ([F] [ρ] ⊢Δ) [b]) (Twk.wkRed*Term [ρ] ⊢Δ Dg))
          [Gb] ([g] [ρ] ⊢Δ [b])
        [u∘b] : Δ ⊩⟨ l ⟩ wk ρ u ∘ b ^ lA ∷ wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [Ga]
        [u∘b] = convTerm₂ [Ga] [Gb] [Ga≡Gb] [u∘b:Gb]
        [ta≡tb] : Δ ⊩⟨ l ⟩ wk ρ t ∘ a ^ lA ≡ wk ρ t ∘ b ^ lA ∷ wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [Ga]
        [ta≡tb] = transEqTerm [Ga] (transEqTerm [Ga] [ta≡fa] ([fext] [ρ] ⊢Δ [a] [b] [a≡b])) (symEqTerm [Ga] (convEqTerm₂ [Ga] [Gb] [Ga≡Gb] [tb≡fb:Gb]))
        [ua≡ub] : Δ ⊩⟨ l ⟩ wk ρ u ∘ a ^ lA ≡ wk ρ u ∘ b ^ lA ∷ wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [Ga]
        [ua≡ub] = transEqTerm [Ga] (transEqTerm [Ga] [ua≡ga] ([gext] [ρ] ⊢Δ [a] [b] [a≡b])) (symEqTerm [Ga] (convEqTerm₂ [Ga] [Gb] [Ga≡Gb] [ub≡gb:Gb]))
        [IdExtG] : Δ ⊩⟨ l ⟩ (Id (wk (lift ρ) G [ a ]) (wk ρ t ∘ a ^ lA) (wk ρ u ∘ a ^ lA)) ≡ (Id (wk (lift ρ) G [ b ]) (wk ρ t ∘ b ^ lA) (wk ρ u ∘ b ^ lA)) ^ [ % , ι lG ] / [Id] ⊢Δ [Ga] [t∘a] [u∘a]
        [IdExtG] = [IdExt] ⊢Δ [Ga] [Gb] [Ga≡Gb] [t∘a] [t∘b:Gb] [ta≡tb] [u∘a] [u∘b:Gb] [ua≡ub]
      in irrelevanceEq″
        (PE.cong₂ (λ X Y → Id _ (X ∘ a ^ lA) (Y ∘ a ^ lA)) (PE.sym (irrelevant-subst′ ρ t a)) (PE.sym (irrelevant-subst′ ρ u a)))
        (PE.cong₂ (λ X Y → Id _ (X ∘ b ^ lA) (Y ∘ b ^ lA)) (PE.sym (irrelevant-subst′ ρ t b)) (PE.sym (irrelevant-subst′ ρ u b)))
        PE.refl PE.refl
        ([Id] ⊢Δ [Ga] [t∘a] [u∘a]) ([idG] [ρ] ⊢Δ [a]) [IdExtG]
  in Πᵣ (Πᵣ rF lF lG lF≤ lG≤ F (Id G ((wk1 t) ∘ (var 0) ^ lA) ((wk1 u) ∘ (var 0) ^ lA))
      [[ univ (Idⱼ (un-univ ⊢A) ⊢tA ⊢uA) , ⊢funext , Did ]]
      ⊢F ⊢idG
      (≅-univ (≅ₜ-Π-cong lF≤ lG≤ ⊢F (≅-un-univ (escapeEqRefl [F0]))
        (≅-un-univ (escapeEqRefl [idG0]))))
      [F] [idG] [idGext])

[Id] ⊢Γ (emb {l′ = ι ⁰} emb< [A]) [t] [u] = emb emb< ([Id] ⊢Γ [A] [t] [u])
[Id] ⊢Γ (emb {l′ = ι ¹} ∞< [A]) [t] [u] = emb ∞< ([Id] ⊢Γ [A] [t] [u])

[IdExtShape] {A} {B} {t} {v} {u} {w} {Γ} {.(ι ¹)} {.(ι ¹)} {lA} ⊢Γ (Uᵣ (Uᵣ rU ⁰ emb< PE.refl d)) (Uᵣ (Uᵣ r₁ ⁰ emb< PE.refl d₁)) (Uᵥ ._ ._) [A≡B] [t] [v] [t≡v] [u] [w] [u≡w] =
  [IdExt]UGen {A} {B} {t} {v} {u} {w} {Γ} ⊢Γ (Uᵣ rU ⁰ emb< PE.refl d) (Uᵣ r₁ ⁰ emb< PE.refl d₁) [A≡B] [t] [v] [t≡v] [u] [w] [u≡w]

[IdExtShape] {A} {B} {t} {v} {u} {w} {Γ} {l} {l'} {lA}  ⊢Γ (ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K) (ne neB) (ne ._ .neB) (ne₌ M [[ ⊢A′ , ⊢B′ ,  D′ ]] neM K≡M) [t] [t′] [t≡t′] [u] [u′] [u≡u′] =
  let
    [A] = (ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K)
    ⊢t′A′ = escapeTerm {l = l'} (ne neB) [t′]
    ⊢u′A′ = escapeTerm {l = l'} (ne neB) [u′]
    A≡K = subset* D
    t≡t′ : Γ ⊢ t ≅ v ∷ K ^ [ ! , ι lA ]
    t≡t′ = ≅-conv (escapeTermEq {l = l} [A] [t≡t′]) A≡K
    u≡u′ = ≅-conv (escapeTermEq {l = l} [A] [u≡u′]) A≡K
  in ne₌ (Id M v w) (univ:⇒*: (IdRed*Term ⊢t′A′ ⊢u′A′ [[ ⊢A′ , ⊢B′ , D′ ]]))
         (Idₙ neM) (~-Id K≡M t≡t′ u≡u′)

[IdExtShape] {A} {B} {t} {v} {u} {w} {Γ} {l} {l'} ⊢Γ (ℕᵣ [[ ⊢A , ⊢B , D ]]) (ℕᵣ [[ ⊢A₁ , ⊢B₁ , D₁ ]]) (ℕᵥ ._ ._) [A≡B] [t] [v] [t≡v] [u] [w] [u≡w] =
  [IdExt]ℕGen {A} {B} {t} {v} {u} {w} {Γ} {l} {l'} ⊢Γ [[ ⊢A , ⊢B , D ]] [[ ⊢A₁ , ⊢B₁ , D₁ ]] [A≡B] [t] [v] [t≡v] [u] [w] [u≡w]

[IdExtShape] {A} {A′} {t} {t′} {u} {u′} {Γ} {l} {l'} {lA} ⊢Γ (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Πᵣ′ rF′ lF′ lG′ lF≤′ lG≤′ F′ G′ [[ ⊢A′ , ⊢B′ , D′ ]] ⊢F′ ⊢G′ A′≡A′ [F′] [G′] G′-ext)
  (Πᵥ .(Πᵣ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext) .(Πᵣ rF′ lF′ lG′ lF≤′ lG≤′ F′ G′ [[ ⊢A′ , ⊢B′ , D′ ]] ⊢F′ ⊢G′ A′≡A′ [F′] [G′] G′-ext))
   (Π₌ F′₀ G′₀ D′₀ A≡B [F≡F′₀] [G≡G′₀])
   [t] [t′] (f₀ , f′₀ , [[ ⊢t , ⊢f₀ , Df₀ ]] , [[ ⊢t′ , ⊢f′₀ , Df′₀ ]] , funf₀ , funf′₀ , f₀≡f′₀ , [t]′ , [t′]′ , [f₀≡f′₀])
   [u] [u′] (g₀ , g′₀ , [[ ⊢u , ⊢g₀ , Dg₀ ]] , [[ ⊢u′ , ⊢g′₀ , Dg′₀ ]] , fung₀ , fung′₀ , g₀≡g′₀ , [u]′ , [u′]′ , [g₀≡g′₀]) =
  let
    F′≡F′₀ , rF′≡rF , lF′≡lF , G′≡G′₀ , lG′≡lG , _ = Π-PE-injectivity (whrDet* (D′ , Whnf.Πₙ) (D′₀ , Whnf.Πₙ))
    [F≡F′] = PE.subst (λ X → ∀ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ) → Δ ⊩⟨ l ⟩ wk ρ F ≡ wk ρ X ^ [ rF , _ ] / [F] [ρ] ⊢Δ) (PE.sym F′≡F′₀) [F≡F′₀]
    [G≡G′] = PE.subst (λ X → ∀ {ρ} {Δ} {a} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ) → ([a] : _) → Δ ⊩⟨ l ⟩ wk (lift ρ) G [ a ] ≡ wk (lift ρ) X [ a ] ^ [ _ , _ ] / [G] [ρ] ⊢Δ [a]) (PE.sym G′≡G′₀) [G≡G′₀]

    f , [[ ⊢t , _ , Df ]] , funf , _ , _ , [f] = [t]
    f₀≡f = whrDet*Term (Df₀ , functionWhnf funf₀) (Df , functionWhnf funf)
    f′ , [[ ⊢t′ , _ , Df′ ]] , funf′ , _ , _ , [f′] = [t′]
    f′₀≡f′ = whrDet*Term (Df′₀ , functionWhnf funf′₀) (Df′ , functionWhnf funf′)
    g , [[ ⊢u , _ , Dg ]] , fung , _ , _ , [g] = [u]
    g₀≡g = whrDet*Term (Dg₀ , functionWhnf fung₀) (Dg , functionWhnf fung)
    g′ , [[ ⊢u′ , _ , Dg′ ]] , fung′ , _ , _ , [g′] = [u′]
    g′₀≡g′ = whrDet*Term (Dg′₀ , functionWhnf fung′₀) (Dg′ , functionWhnf fung′)

    [text] = λ {ρ} {Δ} {a} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ l ⟩ a ∷ wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ) → redSubst*Term
          (appRed* (escapeTerm ([F] [ρ] ⊢Δ) [a]) (Twk.wkRed*Term [ρ] ⊢Δ Df))
          ([G] [ρ] ⊢Δ [a]) ([f] [ρ] ⊢Δ [a])
    [t′ext] = λ {ρ} {Δ} {a} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ l' ⟩ a ∷ wk ρ F′ ^ [ rF′ , ι lF′ ] / [F′] [ρ] ⊢Δ) → redSubst*Term
          (appRed* (escapeTerm ([F′] [ρ] ⊢Δ) [a]) (Twk.wkRed*Term [ρ] ⊢Δ Df′))
          ([G′] [ρ] ⊢Δ [a]) ([f′] [ρ] ⊢Δ [a])
    [uext] = λ {ρ} {Δ} {a} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ l ⟩ a ∷ wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ) → redSubst*Term
          (appRed* (escapeTerm ([F] [ρ] ⊢Δ) [a]) (Twk.wkRed*Term [ρ] ⊢Δ Dg))
          ([G] [ρ] ⊢Δ [a]) ([g] [ρ] ⊢Δ [a])
    [u′ext] = λ {ρ} {Δ} {a} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ l' ⟩ a ∷ wk ρ F′ ^ [ rF′ , ι lF′ ] / [F′] [ρ] ⊢Δ) → redSubst*Term
          (appRed* (escapeTerm ([F′] [ρ] ⊢Δ) [a]) (Twk.wkRed*Term [ρ] ⊢Δ Dg′))
          ([G′] [ρ] ⊢Δ [a]) ([g′] [ρ] ⊢Δ [a])

    [idG] = λ {ρ} {Δ} {a} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) ([a] : Δ ⊩⟨ l ⟩ a ∷ wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ) →
      PE.subst₂ (λ X Y → Δ ⊩⟨ l ⟩ Id (subst (sgSubst a) (wk (lift ρ) G)) (X ∘ a ^ lA) (Y ∘ a ^ lA) ^ [ % , ι lG ])
        (PE.sym (irrelevant-subst′ ρ t a)) (PE.sym (irrelevant-subst′ ρ u a))
        ([Id] ⊢Δ ([G] [ρ] ⊢Δ [a]) (proj₁ ([text] [ρ] ⊢Δ [a])) (proj₁ ([uext] [ρ] ⊢Δ [a])))
    [idG≡idG′] : ∀ {ρ Δ a}
          → ([ρ] : Twk._∷_⊆_ ρ Δ Γ)
          → (⊢Δ : ⊢ Δ)
          → ([a] : Δ ⊩⟨ l ⟩ a ∷ wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
          → Δ ⊩⟨ l ⟩ wk (lift ρ) (Id G (wk1 t ∘ var 0 ^ lA) (wk1 u ∘ var 0 ^ lA)) [ a ] ≡ wk (lift ρ) (Id G′ (wk1 t′ ∘ var 0 ^ lA) (wk1 u′ ∘ var 0 ^ lA)) [ a ] ^ [ % , ι lG ] / [idG] [ρ] ⊢Δ [a]
    [idG≡idG′] {ρ} {Δ} {a} [ρ] ⊢Δ [a] =
      let
        [aF′] = convTerm₁′ (PE.sym rF′≡rF) (PE.cong ι (PE.sym lF′≡lF)) ([F] [ρ] ⊢Δ) ([F′] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ) [a]
        [Ga] = [G] [ρ] ⊢Δ [a]
        [G′a] = [G′] [ρ] ⊢Δ [aF′]
        [Ga≡G′a] : Δ ⊩⟨ l ⟩ wk (lift ρ) G [ a ] ≡ wk (lift ρ) G′ [ a ] ^ [ ! , ι lG ] / [Ga]
        [Ga≡G′a] = [G≡G′] [ρ] ⊢Δ [a]
        [t∘a] , [ta≡fa] = [text] [ρ] ⊢Δ [a]
        [t′∘a] , [t′a≡f′a] = [t′ext] [ρ] ⊢Δ [aF′]
        [fa≡f′a] = PE.subst₂ (λ X Y → Δ ⊩⟨ l ⟩ wk ρ X ∘ a ^ lA ≡ wk ρ Y ∘ a ^ lA ∷ wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [Ga]) f₀≡f f′₀≡f′ ([f₀≡f′₀] [ρ] ⊢Δ [a])
        [ta≡t′a] : Δ ⊩⟨ l ⟩ wk ρ t ∘ a ^ lA ≡ wk ρ t′ ∘ a ^ lA ∷ wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [Ga]
        [ta≡t′a] = transEqTerm [Ga] (transEqTerm [Ga] [ta≡fa] [fa≡f′a]) (symEqTerm [Ga] (convEqTerm₂′ PE.refl (PE.cong ι (PE.sym lG′≡lG)) [Ga] [G′a] [Ga≡G′a] [t′a≡f′a]))
        [u∘a] , [ua≡ga] = [uext] [ρ] ⊢Δ [a]
        [u′∘a] , [u′a≡g′a] = [u′ext] [ρ] ⊢Δ [aF′]
        [ga≡g′a] = PE.subst₂ (λ X Y → Δ ⊩⟨ l ⟩ wk ρ X ∘ a ^ lA ≡ wk ρ Y ∘ a ^ lA ∷ wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [Ga]) g₀≡g g′₀≡g′ ([g₀≡g′₀] [ρ] ⊢Δ [a])
        [ua≡u′a] : Δ ⊩⟨ l ⟩ wk ρ u ∘ a ^ lA ≡ wk ρ u′ ∘ a ^ lA ∷ wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [Ga]
        [ua≡u′a] = transEqTerm [Ga] (transEqTerm [Ga] [ua≡ga] [ga≡g′a]) (symEqTerm [Ga] (convEqTerm₂′ PE.refl (PE.cong ι (PE.sym lG′≡lG)) [Ga] [G′a] [Ga≡G′a] [u′a≡g′a]))
        [G′a]′ = irrelevance′′ PE.refl PE.refl (PE.cong ι lG′≡lG) [G′a]
        [t′∘a]′ = irrelevanceTerm′ PE.refl PE.refl (PE.cong ι lG′≡lG) [G′a] [G′a]′ [t′∘a]
        [u′∘a]′ = irrelevanceTerm′ PE.refl PE.refl (PE.cong ι lG′≡lG) [G′a] [G′a]′ [u′∘a]
        [idG≡idG′]′ : Δ ⊩⟨ l ⟩ Id (wk (lift ρ) G [ a ]) (wk ρ t ∘ a ^ lA) (wk ρ u ∘ a ^ lA) ≡ Id (wk (lift ρ) G′ [ a ]) (wk ρ t′ ∘ a ^ lA) (wk ρ u′ ∘ a ^ lA) ^ [ % , ι lG ] / [Id] ⊢Δ [Ga] [t∘a] [u∘a]
        [idG≡idG′]′ = [IdExt] ⊢Δ [Ga] [G′a]′ [Ga≡G′a] [t∘a] [t′∘a]′ [ta≡t′a] [u∘a] [u′∘a]′ [ua≡u′a]
      in irrelevanceEq″ (PE.cong₂ (λ X Y → Id (wk (lift ρ) G [ a ]) (X ∘ a ^ lA) (Y ∘ a ^ lA)) (PE.sym (irrelevant-subst′ ρ t a)) (PE.sym (irrelevant-subst′ ρ u a)))
        (PE.cong₂ (λ X Y → Id (wk (lift ρ) G′ [ a ]) (X ∘ a ^ lA) (Y ∘ a ^ lA)) (PE.sym (irrelevant-subst′ ρ t′ a)) (PE.sym (irrelevant-subst′ ρ u′ a)))
        PE.refl PE.refl
        ([Id] ⊢Δ [Ga] [t∘a] [u∘a]) ([idG] [ρ] ⊢Δ [a]) [idG≡idG′]′

    [var0] = neuTerm ([F] (Twk.step Twk.id) (⊢Γ ∙ ⊢F)) (var 0) (var (⊢Γ ∙ ⊢F) here) (~-var (var (⊢Γ ∙ ⊢F) here))

    ⊢idG≡idG′₀ : Γ ∙ F ^ [ rF , ι lF ] ⊢ (Id G (wk1 t ∘ var 0 ^ lA) (wk1 u ∘ var 0 ^ lA)) ≅ (Id G′ (wk1 t′ ∘ var 0 ^ lA) (wk1 u′ ∘ var 0 ^ lA)) ^ [ % , ι lG ]
    ⊢idG≡idG′₀ = PE.subst₃ (λ X Y Z → _ ⊢ (Id X (Y ∘ var 0 ^ lA) (Z ∘ var 0 ^ lA)) ≅ _ ^ _)
      (wkSingleSubstId G) (wkSingleSubstId (wk1 t)) (wkSingleSubstId (wk1 u))
      (PE.subst₃ (λ X Y Z → _ ⊢ _ ≅ (Id X (Y ∘ var 0 ^ lA) (Z ∘ var 0 ^ lA)) ^ _)
        (wkSingleSubstId G′) (wkSingleSubstId (wk1 t′)) (wkSingleSubstId (wk1 u′))
        (escapeEq ([idG] (Twk.step Twk.id) (⊢Γ ∙ ⊢F) [var0]) ([idG≡idG′] {step id} {Γ ∙ F ^ [ rF , ι lF ]} {var 0} (Twk.step Twk.id) (⊢Γ ∙ ⊢F) [var0])))

    ⊢F≡F′ = PE.subst₂ (λ X Y → _ ⊢ X ≅ Y ^ _) (wk-id F) (PE.trans (wk-id F′₀) (PE.sym F′≡F′₀))
      (escapeEq ([F] Twk.id ⊢Γ) ([F≡F′₀] Twk.id ⊢Γ))

    [A′] = (Πᵣ′ rF′ lF′ lG′ lF≤′ lG≤′ F′ G′ [[ ⊢A′ , ⊢B′ , D′ ]] ⊢F′ ⊢G′ A′≡A′ [F′] [G′] G′-ext)
    ⊢t′A′ = escapeTerm {l = l'} [A′] [t′]
    ⊢u′A′ = escapeTerm {l = l'} [A′] [u′]

    ⊢t′∘a = PE.subst (λ X → _ ⊢ wk1 t′ ∘ var 0 ^ lA ∷ X ^ [ ! , ι lG′ ]) (wkSingleSubstId G′)
      (Twk.wkTerm (Twk.step Twk.id) (⊢Γ ∙ ⊢F′) ⊢t′ ∘ⱼ var (⊢Γ ∙ ⊢F′) here)
    ⊢u′∘a = PE.subst (λ X → _ ⊢ wk1 u′ ∘ var 0 ^ lA ∷ X ^ [ ! , ι lG′ ]) (wkSingleSubstId G′)
      (Twk.wkTerm (Twk.step Twk.id) (⊢Γ ∙ ⊢F′) ⊢u′ ∘ⱼ var (⊢Γ ∙ ⊢F′) here)
    ⊢funext′ : Γ ⊢ Π F′ ^ rF′ ° lF′ ▹ Id G′ (wk1 t′ ∘ var 0 ^ lA) (wk1 u′ ∘ var 0 ^ lA) ° lG′ ° lA ^ [ % , ι lA ]
    ⊢funext′ = univ (Πⱼ lF≤′ ▹ lG≤′ ▹ un-univ ⊢F′ ▹ Idⱼ (un-univ ⊢G′) ⊢t′∘a ⊢u′∘a)

    Did : Γ ⊢ Id A′ t′ u′ ⇒* Π F′ ^ rF′ ° lF′ ▹ (Id G′ ((wk1 t′) ∘ (var 0) ^ lA) ((wk1 u′) ∘ (var 0) ^ lA)) ° lG′ ° lA ^ [ % , ι lA ]
    Did = IdRed* ⊢t′A′ ⊢u′A′ D′ ⇨* ((univ (Id-Π lF≤′ lG≤′ (un-univ ⊢F′) (un-univ ⊢G′) ⊢t′ ⊢u′)) ⇨ id ⊢funext′)

  in Π₌ F′ (Id G′ ((wk1 t′) ∘ (var 0) ^ lA) ((wk1 u′) ∘ (var 0) ^ lA))
         (PE.subst (λ X → Γ ⊢ Id A′ t′ u′ ⇒* Π F′ ^ rF ° lF ▹ _ ° X ° lA ^ [ % , ι lA ]) lG′≡lG
           (PE.subst (λ X → Γ ⊢ Id A′ t′ u′ ⇒* Π F′ ^ rF ° X ▹ _ ° lG′ ° lA ^ [ % , ι lA ]) lF′≡lF
             (PE.subst (λ X → Γ ⊢ Id A′ t′ u′ ⇒* Π F′ ^ X ° lF′ ▹ _ ° lG′ ° lA ^ [ % , ι lA ]) rF′≡rF Did)))
        (≅-univ (≅ₜ-Π-cong lF≤ lG≤ ⊢F (≅-un-univ ⊢F≡F′) (≅-un-univ ⊢idG≡idG′₀))) [F≡F′] [idG≡idG′]

[IdExtShape] {A} {B} {t} {t′} {u} {u′} {Γ} ⊢Γ (emb emb< [A]) [B] (emb⁰¹ {p = .[A]} ShapeA) [A≡B] [t] [v] [t≡v] [u] [w] [u≡w] =
  [IdExtShape] ⊢Γ [A] [B] ShapeA [A≡B] [t] [v] [t≡v] [u] [w] [u≡w]
[IdExtShape] {A} {B} {t} {t′} {u} {u′} {Γ} ⊢Γ [A] (emb emb< [B]) (emb¹⁰ {q = .[B]} ShapeA) [A≡B] [t] [v] [t≡v] [u] [w] [u≡w] =
  [IdExtShape] ⊢Γ [A] [B] ShapeA [A≡B] [t] [v] [t≡v] [u] [w] [u≡w]
[IdExtShape] {A} {B} {t} {t′} {u} {u′} {Γ} ⊢Γ (emb ∞< [A]) [B] (emb¹∞ {p = .[A]} ShapeA) [A≡B] [t] [v] [t≡v] [u] [w] [u≡w] =
  [IdExtShape] ⊢Γ [A] [B] ShapeA [A≡B] [t] [v] [t≡v] [u] [w] [u≡w]
[IdExtShape] {A} {B} {t} {t′} {u} {u′} {Γ} ⊢Γ [A] (emb ∞< [B]) (emb∞¹ {q = .[B]} ShapeA) [A≡B] [t] [v] [t≡v] [u] [w] [u≡w] =
  [IdExtShape] ⊢Γ [A] [B] ShapeA [A≡B] [t] [v] [t≡v] [u] [w] [u≡w]

[IdExt] {A} {A′} {t} {t′} {u} {u′} {Γ} ⊢Γ [A] [A′] [A≡A′] [t] [t′] [t≡t′] [u] [u′] [u≡u′] =
  [IdExtShape] {A} {A′} {t} {t′} {u} {u′} {Γ} ⊢Γ [A] [A′] (goodCases [A] [A′] [A≡A′]) [A≡A′] [t] [t′] [t≡t′] [u] [u′] [u≡u′]

Idᵛ-min : ∀ {A t u Γ l}
       ([Γ] : ⊩ᵛ Γ)
       ([A] : Γ ⊩ᵛ⟨ ι l ⟩ A ^ [ ! , ι l ] / [Γ])
       ([t] : Γ ⊩ᵛ⟨ ι l ⟩ t ∷ A ^ [ ! , ι l ] / [Γ] / [A])
       ([u] : Γ ⊩ᵛ⟨ ι l ⟩ u ∷ A ^ [ ! , ι l ] / [Γ] / [A])
     → Γ ⊩ᵛ⟨ ι l ⟩ Id A t u ^ [ % , ι l ] / [Γ]
Idᵛ-min [Γ] [A] [t] [u] ⊢Δ [σ] =
  ([Id] ⊢Δ (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ])) (proj₁ ([u] ⊢Δ [σ]))) ,
  (λ [σ′] [σ≡σ′] → [IdExt] ⊢Δ (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([A] ⊢Δ [σ′])) (proj₂ ([A] ⊢Δ [σ]) [σ′] [σ≡σ′])
                             (proj₁ ([t] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ′])) (proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′])
                             (proj₁ ([u] ⊢Δ [σ])) (proj₁ ([u] ⊢Δ [σ′])) (proj₂ ([u] ⊢Δ [σ]) [σ′] [σ≡σ′]))

Idᵛ : ∀ {A t u Γ l}
       ([Γ] : ⊩ᵛ Γ)
       ([A] : Γ ⊩ᵛ⟨ ∞ ⟩ A ^ [ ! , ι l ] / [Γ])
       ([t] : Γ ⊩ᵛ⟨ ∞ ⟩ t ∷ A ^ [ ! , ι l ] / [Γ] / [A])
       ([u] : Γ ⊩ᵛ⟨ ∞ ⟩ u ∷ A ^ [ ! , ι l ] / [Γ] / [A])
     → Γ ⊩ᵛ⟨ ∞ ⟩ Id A t u ^ [ % , ι l ] / [Γ]
Idᵛ [Γ] [A] [t] [u] ⊢Δ [σ] =
  ([Id] ⊢Δ (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ])) (proj₁ ([u] ⊢Δ [σ]))) ,
  (λ [σ′] [σ≡σ′] → [IdExt] ⊢Δ (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([A] ⊢Δ [σ′])) (proj₂ ([A] ⊢Δ [σ]) [σ′] [σ≡σ′])
                             (proj₁ ([t] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ′])) (proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′])
                             (proj₁ ([u] ⊢Δ [σ])) (proj₁ ([u] ⊢Δ [σ′])) (proj₂ ([u] ⊢Δ [σ]) [σ′] [σ≡σ′]))

Idᵗᵛ-min : ∀ {A t u Γ l}
       ([Γ] : ⊩ᵛ Γ)
       ([A] : Γ ⊩ᵛ⟨ ι l ⟩ A ^ [ ! , ι l ] / [Γ])
       ([t] : Γ ⊩ᵛ⟨ ι l ⟩ t ∷ A ^ [ ! , ι l ] / [Γ] / [A])
       ([u] : Γ ⊩ᵛ⟨ ι l ⟩ u ∷ A ^ [ ! , ι l ] / [Γ] / [A])
     → Γ ⊩ᵛ⟨ next l ⟩ Id A t u ∷ SProp l ^ [ ! , next l ] / [Γ] / Uᵛgen (≡is≤ PE.refl) <next [Γ]
Idᵗᵛ-min {A} {t} {u} {_} {l} [Γ] [A] [t] [u] =
  let [U] = Uᵛgen (≡is≤ PE.refl) <next [Γ]
  in un-univᵛ {A = Id A t u} [Γ] [U] (Idᵛ-min {A} {t} {u} [Γ] [A] [t] [u])

Idᵗᵛ : ∀ {A t u Γ l}
       ([Γ] : ⊩ᵛ Γ) →
       let [UA] = maybeEmbᵛ {A = U _} [Γ] (Uᵛ <next [Γ])
           [U] = maybeEmbᵛ {A = SProp _} [Γ] (Uᵛ <next [Γ])
       in ([A] : Γ ⊩ᵛ⟨ ∞ ⟩ A ^ [ ! , ι l ] / [Γ])
          ([t] : Γ ⊩ᵛ⟨ ∞ ⟩ t ∷ A ^ [ ! , ι l ] / [Γ] / [A])
          ([u] : Γ ⊩ᵛ⟨ ∞ ⟩ u ∷ A ^ [ ! , ι l ] / [Γ] / [A])
          ([A]t : Γ ⊩ᵛ⟨ ∞ ⟩ A ∷ Univ ! l ^ [ ! , next l ] / [Γ] / [UA])
          → Γ ⊩ᵛ⟨ ∞ ⟩ Id A t u ∷ SProp l ^ [ ! , next l ] / [Γ] / [U]
Idᵗᵛ {A} {t} {u} {_} {l} [Γ] [A] [t] [u] [A]t =
  let [UA] = maybeEmbᵛ {A = U _} [Γ] (Uᵛ <next [Γ])
      [A]' = univᵛ {A = A} [Γ] (≡is≤ PE.refl) [UA] [A]t
      [t]' = S.irrelevanceTerm {A = A} {t = t} [Γ] [Γ] [A] [A]' [t]
      [u]' = S.irrelevanceTerm {A = A} {t = u} [Γ] [Γ] [A] [A]' [u]
      [Id] = Idᵗᵛ-min {A} {t} {u} [Γ] [A]' [t]' [u]'
  in maybeEmbTermᵛ {l = next l} {A = SProp _} {t = Id A t u} [Γ] (Uᵛgen (≡is≤ PE.refl) <next [Γ]) [Id]

Id-congᵛ-min : ∀ {A A' t t' u u' Γ l}
       ([Γ] : ⊩ᵛ Γ)
       ([A] : Γ ⊩ᵛ⟨ ι l ⟩ A ^ [ ! , ι l ] / [Γ])
       ([t] : Γ ⊩ᵛ⟨ ι l ⟩ t ∷ A ^ [ ! , ι l ] / [Γ] / [A])
       ([u] : Γ ⊩ᵛ⟨ ι l ⟩ u ∷ A ^ [ ! , ι l ] / [Γ] / [A])
       ([A'] : Γ ⊩ᵛ⟨ ι l ⟩ A' ^ [ ! , ι l ] / [Γ])
       ([t'] : Γ ⊩ᵛ⟨ ι l ⟩ t' ∷ A' ^ [ ! , ι l ] / [Γ] / [A'])
       ([u'] : Γ ⊩ᵛ⟨ ι l ⟩ u' ∷ A' ^ [ ! , ι l ] / [Γ] / [A'])
       ([A≡A'] : Γ ⊩ᵛ⟨ ι l ⟩ A ≡ A' ^ [ ! , ι l ] / [Γ] / [A])
       ([t≡t'] : Γ ⊩ᵛ⟨ ι l ⟩ t ≡ t' ∷ A ^ [ ! , ι l ] / [Γ] / [A])
       ([u≡u'] : Γ ⊩ᵛ⟨ ι l ⟩ u ≡ u' ∷ A ^ [ ! , ι l ] / [Γ] / [A])
     → Γ ⊩ᵛ⟨ ι l ⟩ Id A t u ≡ Id A' t' u' ^ [ % , ι l ] / [Γ] / Idᵛ-min {A} {t} {u} [Γ] [A] [t] [u]
Id-congᵛ-min [Γ] [A] [t] [u] [A'] [t'] [u'] [A≡A'] [t≡t'] [u≡u'] ⊢Δ [σ] =
  [IdExt] ⊢Δ (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([A'] ⊢Δ [σ])) ([A≡A'] ⊢Δ [σ])
             (proj₁ ([t] ⊢Δ [σ])) (proj₁ ([t'] ⊢Δ [σ])) ([t≡t'] ⊢Δ [σ])
             (proj₁ ([u] ⊢Δ [σ])) (proj₁ ([u'] ⊢Δ [σ])) ([u≡u'] ⊢Δ [σ])

Id-cong-minᵗᵛ : ∀ {A A' t t' u u' Γ l}
       ([Γ] : ⊩ᵛ Γ)
       ([A] : Γ ⊩ᵛ⟨ ι l ⟩ A ^ [ ! , ι l ] / [Γ])
       ([t] : Γ ⊩ᵛ⟨ ι l ⟩ t ∷ A ^ [ ! , ι l ] / [Γ] / [A])
       ([u] : Γ ⊩ᵛ⟨ ι l ⟩ u ∷ A ^ [ ! , ι l ] / [Γ] / [A])
       ([A'] : Γ ⊩ᵛ⟨ ι l ⟩ A' ^ [ ! , ι l ] / [Γ])
       ([t'] : Γ ⊩ᵛ⟨ ι l ⟩ t' ∷ A' ^ [ ! , ι l ] / [Γ] / [A'])
       ([u'] : Γ ⊩ᵛ⟨ ι l ⟩ u' ∷ A' ^ [ ! , ι l ] / [Γ] / [A'])
       ([A≡A'] : Γ ⊩ᵛ⟨ ι l ⟩ A ≡ A' ^ [ ! , ι l ] / [Γ] / [A])
       ([t≡t'] : Γ ⊩ᵛ⟨ ι l ⟩ t ≡ t' ∷ A ^ [ ! , ι l ] / [Γ] / [A])
       ([u≡u'] : Γ ⊩ᵛ⟨ ι l ⟩ u ≡ u' ∷ A ^ [ ! , ι l ] / [Γ] / [A])
     → Γ ⊩ᵛ⟨ next l ⟩ Id A t u ≡ Id A' t' u' ∷ SProp l ^ [ ! , next l ] / [Γ] / Uᵛgen (≡is≤ PE.refl) <next [Γ]
Id-cong-minᵗᵛ {A} {A'} {t} {t'} {u} {u'} [Γ] [A] [t] [u] [A'] [t'] [u'] [A≡A'] [t≡t'] [u≡u'] =
  let [U] = Uᵛgen (≡is≤ PE.refl) <next [Γ]
  in un-univEqᵛ {A = Id A t u} {B = Id A' t' u'} [Γ] [U]
                (Idᵛ-min {A} {t} {u} [Γ] [A] [t] [u])
                (Idᵛ-min {A'} {t'} {u'} [Γ] [A'] [t'] [u'])
                (Id-congᵛ-min {A} {A'} {t} {t'} {u} {u'} [Γ] [A] [t] [u] [A'] [t'] [u'] [A≡A'] [t≡t'] [u≡u'])

Id-congᵗᵛ : ∀ {A A' t t' u u' Γ l}
       ([Γ] : ⊩ᵛ Γ) →
       let [UA] = maybeEmbᵛ {A = U _} [Γ] (Uᵛ <next [Γ])
           [U] = maybeEmbᵛ {A = SProp _} [Γ] (Uᵛ <next [Γ])
       in ([A] : Γ ⊩ᵛ⟨ ∞ ⟩ A ^ [ ! , ι l ] / [Γ])
          ([t] : Γ ⊩ᵛ⟨ ∞ ⟩ t ∷ A ^ [ ! , ι l ] / [Γ] / [A])
          ([u] : Γ ⊩ᵛ⟨ ∞ ⟩ u ∷ A ^ [ ! , ι l ] / [Γ] / [A])
          ([A]t : Γ ⊩ᵛ⟨ ∞ ⟩ A ∷ Univ ! l ^ [ ! , next l ] / [Γ] / [UA])
          ([A'] : Γ ⊩ᵛ⟨ ∞ ⟩ A' ^ [ ! , ι l ] / [Γ])
          ([t'] : Γ ⊩ᵛ⟨ ∞ ⟩ t' ∷ A' ^ [ ! , ι l ] / [Γ] / [A'])
          ([u'] : Γ ⊩ᵛ⟨ ∞ ⟩ u' ∷ A' ^ [ ! , ι l ] / [Γ] / [A'])
          ([A']t : Γ ⊩ᵛ⟨ ∞ ⟩ A' ∷ Univ ! l ^ [ ! , next l ] / [Γ] / [UA])
          ([A≡A']t : Γ ⊩ᵛ⟨ ∞ ⟩ A ≡ A' ∷ Univ ! l ^ [ ! , next l ] / [Γ] / [UA])
          ([t≡t'] : Γ ⊩ᵛ⟨ ∞ ⟩ t ≡ t' ∷ A ^ [ ! , ι l ] / [Γ] / [A])
          ([u≡u'] : Γ ⊩ᵛ⟨ ∞ ⟩ u ≡ u' ∷ A ^ [ ! , ι l ] / [Γ] / [A])
          → Γ ⊩ᵛ⟨ ∞ ⟩ Id A t u ≡ Id A' t' u' ∷ SProp l ^ [ ! , next l ] / [Γ] / [U]
Id-congᵗᵛ {A} {A'} {t} {t'} {u} {u'} {_} {l} [Γ] [A] [t] [u] [A]t [A'] [t'] [u'] [A']t [A≡A']t [t≡t'] [u≡u'] =
   let [UA] = maybeEmbᵛ {A = U _} [Γ] (Uᵛ <next [Γ])
       [A]' = univᵛ {A = A} [Γ] (≡is≤ PE.refl) [UA] [A]t
       [t]' = S.irrelevanceTerm {A = A} {t = t} [Γ] [Γ] [A] [A]' [t]
       [u]' = S.irrelevanceTerm {A = A} {t = u} [Γ] [Γ] [A] [A]' [u]
       [A']' = univᵛ {A = A'} [Γ] (≡is≤ PE.refl) [UA] [A']t
       [t']' = S.irrelevanceTerm {A = A'} {t = t'} [Γ] [Γ] [A'] [A']' [t']
       [u']' = S.irrelevanceTerm {A = A'} {t = u'} [Γ] [Γ] [A'] [A']' [u']
       [A≡A']' = univEqᵛ {A = A} {B = A'} [Γ] [UA] [A]' [A≡A']t
       [t≡t']' = S.irrelevanceEqTerm {A = A} {t = t} {u = t'} [Γ] [Γ] [A] [A]' [t≡t']
       [u≡u']' = S.irrelevanceEqTerm {A = A} {t = u} {u = u'} [Γ] [Γ] [A] [A]' [u≡u']
       [Id] = Id-cong-minᵗᵛ {A} {A'} {t} {t'} {u} {u'} [Γ] [A]' [t]' [u]' [A']' [t']' [u']' [A≡A']' [t≡t']' [u≡u']'
   in maybeEmbEqTermᵛ {l = next l} {A = SProp _} {t = Id A t u} {u = Id A' t' u'} [Γ] (Uᵛgen (≡is≤ PE.refl) <next [Γ]) [Id]

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

open import Algebra

module Control.Monad.Weighted {ℓ} (rng : Semiring ℓ) where

open import Control.Monad.Weighted.Definition rng public
open import Control.Monad.Weighted.Union      rng using (_∪_) public
open import Control.Monad.Weighted.Cond       rng using (_⋊_) public
open import Control.Monad.Weighted.Monad      rng using (_>>=_; pure; _>>_; _<*>_) public

import Control.Monad.Weighted.Expect using (∫)

module Expect = Control.Monad.Weighted.Expect rng

ext: agda

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import HoTT

module homotopy.TruncationLoopLadder where

  ⊙Ω-Trunc : ∀ {i} {n : ℕ₋₂} (X : Ptd i)
    → ⊙Ω (⊙Trunc (S n) X) ⊙≃ ⊙Trunc n (⊙Ω X)
  ⊙Ω-Trunc X = ≃-to-⊙≃ (Trunc=-equiv [ pt X ] [ pt X ]) idp

  step : ∀ {i j} n {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
    → ⊙CommSquareEquiv
        (⊙Ω-fmap (⊙Trunc-fmap {n = S n} f))
        (⊙Trunc-fmap {n = n} (⊙Ω-fmap f))
        (⊙–> (⊙Ω-Trunc X))
        (⊙–> (⊙Ω-Trunc Y))
  step n (f , idp) =
    ⊙comm-sqr (Trunc=-equiv-nat _ _ _ , idp) , snd (⊙Ω-Trunc _) , snd (⊙Ω-Trunc _)

  rail : ∀ m {i} (X : Ptd i)
    → ⊙Ω^' m (⊙Trunc ⟨ m ⟩ X) ⊙→ ⊙Trunc 0 (⊙Ω^' m X)
  rail O X = ⊙idf _
  rail (S m) X = rail m (⊙Ω X) ⊙∘ ⊙Ω^'-fmap m (⊙–> (⊙Ω-Trunc X))

  ladder : ∀ {i j} m {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
    → ⊙CommSquareEquiv
        (⊙Ω^'-fmap m (⊙Trunc-fmap {n = ⟨ m ⟩} f))
        (⊙Trunc-fmap {n = 0} (⊙Ω^'-fmap m f))
        (rail m X)
        (rail m Y)
  ladder O f = ⊙comm-sqr (⊙∘-unit-l _) , idf-is-equiv _ , idf-is-equiv _
  ladder (S m) f =
    ⊙CommSquareEquiv-∘v (ladder m (⊙Ω-fmap f)) (⊙Ω^'-csemap m (step ⟨ m ⟩ f))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; cong₂)
open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s)
open import Data.Nat.Properties using (≤-total)
open import Data.Fin using (Fin; zero; suc)
open import Data.Product using (∃; ∃-syntax; _×_; _,_)
open import Data.Sum using ([_,_])

open import DeBruijn
open import Substitution using (rename-subst-commute; subst-commute; extensionality)
open import Beta
open import BetaSubstitutivity using (sub-betas)
open import Takahashi

infix 8 _*⁽_⁾

_*⁽_⁾ : ∀ {n} → Term n → ℕ → Term n
M *⁽ zero ⁾  = M
M *⁽ suc k ⁾ = (M *) *⁽ k ⁾

data _—↠⁽_⁾_ : ∀ {n} → Term n → ℕ → Term n → Set where

  _∎ : ∀ {n} (M : Term n)
      --------------
    → M —↠⁽ zero ⁾ M

  _—→⁽⁾⟨_⟩_ : ∀ {n} {N L : Term n} {k : ℕ} (M : Term n)
    → M —→ L
    → L —↠⁽ k ⁾ N
      ---------------
    → M —↠⁽ suc k ⁾ N

lemma3-2 : ∀ {n} {M : Term n}
  → M —↠ M *
lemma3-2 {M = # x}       = # x ∎
lemma3-2 {M = ƛ _}       = —↠-cong-ƛ lemma3-2
lemma3-2 {M = # _ · _}   = —↠-congᵣ           lemma3-2
lemma3-2 {M = _ · _ · _} = —↠-cong   lemma3-2 lemma3-2
lemma3-2 {M = (ƛ M) · N} = (ƛ M) · N —→⟨ —→-β ⟩ sub-betas {M = M} lemma3-2 lemma3-2

lemma3-3 : ∀ {n} {M N : Term n}
  → M —→ N
    --------
  → N —↠ M *
lemma3-3 {M = # _} ()
lemma3-3 {M = ƛ M}         (—→-ƛ M—→M′)  = —↠-cong-ƛ (lemma3-3 M—→M′)
lemma3-3 {M = # _     · N} (—→-ξᵣ N—→N′) = —↠-congᵣ                 (lemma3-3 N—→N′)
lemma3-3 {M = _ · _   · N} (—→-ξᵣ N—→N′) = —↠-cong   lemma3-2       (lemma3-3 N—→N′)
lemma3-3 {M = M₁ · M₂ · _} (—→-ξₗ M—↠M′) = —↠-cong  (lemma3-3 M—↠M′) lemma3-2
lemma3-3 {M = (ƛ M)   · N}  —→-β         = sub-betas {M = M} lemma3-2 lemma3-2
lemma3-3 {M = (ƛ M)   · N} (—→-ξᵣ       {N′ = N′} N—→N′)  = (ƛ M ) · N′ —→⟨ —→-β ⟩ sub-betas {M = M} lemma3-2 (lemma3-3 N—→N′)
lemma3-3 {M = (ƛ M)   · N} (—→-ξₗ (—→-ƛ {M′ = M′} M—→M′)) = (ƛ M′) · N  —→⟨ —→-β ⟩ sub-betas {N = N} (lemma3-3 M—→M′) lemma3-2

_*ˢ : ∀ {n m} → Subst n m → Subst n m
σ *ˢ = λ x → (σ x) *

rename-* : ∀ {n m} (ρ : Rename n m) (M : Term n)
  → rename ρ (M *) ≡ (rename ρ M) *
rename-* ρ (# _)         = refl
rename-* ρ (ƛ M)         = cong ƛ_ (rename-* (ext ρ) M)
rename-* ρ (# _     · N) = cong₂ _·_ refl                   (rename-* ρ N)
rename-* ρ (M₁ · M₂ · N) = cong₂ _·_ (rename-* ρ (M₁ · M₂)) (rename-* ρ N)
rename-* ρ ((ƛ M)   · N) rewrite sym (rename-subst-commute {N = M *}{M = N *}{ρ = ρ})
                               | rename-* (ext ρ) M
                               | rename-* ρ N
                               = refl

exts-ts-commute : ∀ {n m} (σ : Subst n m)
  → exts (σ *ˢ) ≡ (exts σ) *ˢ
exts-ts-commute {n} σ = extensionality exts-ts-commute′
  where
    exts-ts-commute′ : (x : Fin (suc n))
      → (exts (σ *ˢ)) x ≡ ((exts σ) *ˢ) x
    exts-ts-commute′ zero    = refl
    exts-ts-commute′ (suc x) = rename-* suc (σ x)

app-*-join : ∀ {n} (M N : Term n)
  → M * · N * —↠ (M · N) *
app-*-join (# x)     N = # x · N * ∎
app-*-join (ƛ M)     N = (ƛ M *) · N * —→⟨ —→-β ⟩ subst (subst-zero (N *)) (M *) ∎
app-*-join (M₁ · M₂) N = (M₁ · M₂) * · N * ∎

subst-ts : ∀ {n m} (σ : Subst n m) (M : Term n)
  → subst (σ *ˢ) (M *) —↠ (subst σ M) *
subst-ts σ (# x) = σ x * ∎
subst-ts σ (ƛ M) rewrite exts-ts-commute σ = —↠-cong-ƛ (subst-ts (exts σ) M)
subst-ts σ (# x · N) = —↠-trans (—↠-congᵣ (subst-ts σ N))
                                (app-*-join (σ x) (subst σ N))
subst-ts σ (M₁ · M₂ · N) = —↠-cong (subst-ts σ (M₁ · M₂)) (subst-ts σ N)
subst-ts σ ((ƛ M) · N) rewrite sym (subst-commute {N = M *}{M = N *}{σ = σ *ˢ})
                             | exts-ts-commute σ
                             = sub-betas (subst-ts (exts σ) M) (subst-ts σ N)

subst-zero-ts : ∀ {n} {N : Term n}
  → subst-zero (N *) ≡ (subst-zero N) *ˢ
subst-zero-ts = extensionality (λ { zero → refl ; (suc x) → refl })

lemma3-4 : ∀ {n} (M : Term (suc n)) (N : Term n)
  → M * [ N * ] —↠ (M [ N ]) *
lemma3-4 M N rewrite subst-zero-ts {N = N} = subst-ts (subst-zero N) M

lemma3-5 : ∀ {n} {M N : Term n}
  → M   —→ N
    ----------
  → M * —↠ N *
lemma3-5 {M = # x} ()
lemma3-5 {M = ƛ M}         (—→-ƛ  M—→M′)  = —↠-cong-ƛ (lemma3-5 M—→M′)
lemma3-5 {M = # _     · N} (—→-ξᵣ M₂—→M′) = —↠-congᵣ  (lemma3-5 M₂—→M′)
lemma3-5 {M = (ƛ M)   · N}  —→-β                = lemma3-4 M N
lemma3-5 {M = (ƛ M)   · N} (—→-ξₗ (—→-ƛ M—→M′)) = sub-betas (lemma3-5 M—→M′) (N * ∎)
lemma3-5 {M = (ƛ M)   · N} (—→-ξᵣ N—→N′)        = sub-betas (M * ∎) (lemma3-5 N—→N′)
lemma3-5 {M = M₁ · M₂ · _} (—→-ξᵣ N—→N′)                         = —↠-congᵣ (lemma3-5 N—→N′)
lemma3-5 {M = M₁ · M₂ · _} (—→-ξₗ {M′ = # x}       M₁M₂—→#x)     = —↠-congₗ (lemma3-5 M₁M₂—→#x)
lemma3-5 {M = M₁ · M₂ · _} (—→-ξₗ {M′ = M′₁ · M′₂} M₁M₂—→M′₁M′₂) = —↠-congₗ (lemma3-5 M₁M₂—→M′₁M′₂)
lemma3-5 {M = M₁ · M₂ · N} (—→-ξₗ {M′ = ƛ M′}      M₁M₂—→ƛM′)    =
  —↠-trans (—↠-congₗ (lemma3-5 M₁M₂—→ƛM′))
           ((ƛ M′ *) · N * —→⟨ —→-β ⟩ subst (subst-zero (N *)) (M′ *) ∎)

corollary3-6 : ∀ {n} {M N : Term n}
  → M   —↠ N
    ----------
  → M * —↠ N *
corollary3-6 (M ∎) = M * ∎
corollary3-6 (M —→⟨ M—→L ⟩ L—↠N) = —↠-trans (lemma3-5 M—→L) (corollary3-6 L—↠N)

corollary3-7 : ∀ {n} {M N : Term n} (m : ℕ)
  → M        —↠ N
    --------------------
  → M *⁽ m ⁾ —↠ N *⁽ m ⁾
corollary3-7 zero    M—↠N = M—↠N
corollary3-7 (suc m) M—↠N = corollary3-7 m (corollary3-6 M—↠N)

theorem3-8 : ∀ {n} {M N : Term n} {m : ℕ}
  → M —↠⁽ m ⁾ N
    -------------
  → N —↠ M *⁽ m ⁾
theorem3-8 {m = zero}  (M ∎) = M ∎
theorem3-8 {m = suc m} (M —→⁽⁾⟨ M—→L ⟩ L—↠ᵐN) =
  —↠-trans (theorem3-8 L—↠ᵐN) (corollary3-7 m (lemma3-3 M—→L))

unnamed-named : ∀ {n} {M N : Term n}
  →         M —↠      N
    --------------------
  → ∃[ m ] (M —↠⁽ m ⁾ N)
unnamed-named (M ∎) = zero , (M ∎)
unnamed-named (M —→⟨ M—→L ⟩ L—↠N) with unnamed-named L—↠N
... | m′ , L—↠ᵐ′N = suc m′ , (M —→⁽⁾⟨ M—→L ⟩ L—↠ᵐ′N)

lift-* : ∀ {n} (M : Term n) (m : ℕ)
  → M —↠ M *⁽ m ⁾
lift-* M zero    = M ∎
lift-* M (suc m) = —↠-trans lemma3-2 (lift-* (M *) m)

complete-* : ∀ {k} (M : Term k) {n m : ℕ}
  → n ≤ m
    --------------------
  → M *⁽ n ⁾ —↠ M *⁽ m ⁾
complete-* M {m = m} z≤n = lift-* M m
complete-* M (s≤s k) = complete-* (M *) k

theorem3-9 : ∀ {n} {M A B : Term n}
  →         M —↠ A → M —↠ B
    ------------------------
  → ∃[ N ] (A —↠ N × B —↠ N)
theorem3-9 {M = M} M—↠A M—↠B =
    let n , M—↠ⁿA = unnamed-named M—↠A
        m , M—↠ᵐB = unnamed-named M—↠B
        A—↠M*ⁿ = theorem3-8 M—↠ⁿA
        B—↠M*ᵐ = theorem3-8 M—↠ᵐB
     in [ (λ n≤m →
            let M*ⁿ—↠M*ᵐ : M *⁽ n ⁾ —↠ M *⁽ m ⁾
                M*ⁿ—↠M*ᵐ = complete-* M n≤m
             in M *⁽ m ⁾ , —↠-trans A—↠M*ⁿ M*ⁿ—↠M*ᵐ , B—↠M*ᵐ)
        , (λ m≤n →
            let M*ᵐ—↠M*ⁿ : M *⁽ m ⁾ —↠ M *⁽ n ⁾
                M*ᵐ—↠M*ⁿ = complete-* M m≤n
             in M *⁽ n ⁾ , A—↠M*ⁿ , —↠-trans B—↠M*ᵐ M*ᵐ—↠M*ⁿ)
        ] (≤-total n m)

max_stars_repo_name: iwilare/church-rosser

max_issues_repo_name: iwilare/church-rosser

max_forks_repo_name: iwilare/church-rosser


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

open import HoTT

module groups.Image where

module _ {i j k} {G : Group i} {H : Group j}
  {K : Group k} (φ : H →ᴳ K) (ψ : G →ᴳ H) where

  abstract
    im-sub-im-∘ : is-surjᴳ ψ → im-propᴳ φ ⊆ᴳ im-propᴳ (φ ∘ᴳ ψ)
    im-sub-im-∘ ψ-is-surj k = Trunc-rec Trunc-level
      (λ{(h , φh=k) → Trunc-rec Trunc-level
        (λ{(g , ψg=h) → [ g , ap (GroupHom.f φ) ψg=h ∙ φh=k ]})
        (ψ-is-surj h)})

    im-∘-sub-im : im-propᴳ (φ ∘ᴳ ψ) ⊆ᴳ im-propᴳ φ
    im-∘-sub-im k = Trunc-rec Trunc-level
      (λ{(g , φψg=k) → [ GroupHom.f ψ g , φψg=k ]})

  im-iso-im-pre∘ : is-surjᴳ ψ → Im φ ≃ᴳ Im (φ ∘ᴳ ψ)
  im-iso-im-pre∘ ψ-is-surj = Subgroup-emap-r
    (im-propᴳ φ) (im-propᴳ (φ ∘ᴳ ψ))
    (im-sub-im-∘ ψ-is-surj) im-∘-sub-im

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Everything

module Test.ProblemWithLevelZero where

module _ (𝔓 : Ø₀) where

  open Substitunction 𝔓
  open Term 𝔓

  fails : ∀ {m n} (f : Substitunction m n) → Substitunction m n
  fails f = transitivity f ε -- FIXME

  refl-works : ∀ {m} → Substitunction m m
  refl-works = ε

  solution-1o solution-1a solution-2o solution-2a :
    ∀ {m n} (f : Substitunction m n) → Substitunction m n

  solution-1o f = transitivity {𝔒 = ¶} f ε
  solution-1a f = transitivity[ Substitunction ] f ε
  solution-2o f = transitivity {𝔒 = Ø₀} f ε
  solution-2a f = transitivity[ Function ] f ε

  transitivity-hole : ∀ {m n} (f : Substitunction m n) → Substitunction m n
  transitivity-hole f =
    transitivity
      ⦃ {!!!} -- FIXME does not resolve instance
        ⦄
      f
      {!!}


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

module Cubical.HITs.Bouquet where

open import Cubical.HITs.Bouquet.Base public
open import Cubical.HITs.Bouquet.FundamentalGroupProof public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Issue224 where

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A → Maybe A

data D (A : Set) : Maybe A → Set where
  d₁ : (x : A) → D A (just x)
  d₂ : ∀ {x} → D A x → D A x

data S : ∀ {A x} → D A x → Set₁ where
  s : ∀ {A x} {d : D A x} → S d → S (d₂ d)

foo : {A : Set} → S (d₂ (d₁ (nothing {A}))) → Set₁
foo (s _) = Set

-- Bug.agda:19,6-9
-- Panic: Pattern match failure in do expression at
-- src/full/Agda/TypeChecking/Rules/LHS/Unify.hs:331:2-5
-- when checking that the pattern s _ has type S (d₂ (d₁ nothing))

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Issue133 where

data Nat : Set where
  zz : Nat
  ss : Nat → Nat

data _==_ {X : Set}(x : X) : X → Set where
  refl : x == x

data Zero : Set where

data Eq? (x : Nat) : Nat → Set where
  same : Eq? x x
  diff : {y : Nat} → (x == y → Zero) → Eq? x y

-- This failed before due to absurd lambda checking not getting
-- postponed.
ioo : {y : Nat} → Eq? zz (ss y)
ioo {y} = diff λ ()

foo : {y : Nat} → zz == ss y → Zero
foo ()

goo : {y : Nat} → zz == ss y → Zero
goo = λ ()

hoo : {y : Nat}{X : Set} → ((zz == ss y → Zero) → X) → X
hoo boo = boo λ ()


text:
-- Andreas, 2017-01-18, issue #2408

-- DLubs were not serialized, thus, there was a problem with
-- level dependent on irrelevant values.

{-# OPTIONS --show-irrelevant #-}

-- {-# OPTIONS -v tc:70 #-}

open import Agda.Primitive

postulate
  A : Set
  l : .(a : A) → Level
  F : .(a : A) → Set (l a)

-- checked type signature
--   F : .(a : A) → Set (l a)
--   of sort  dLub Set (λ a → Set (lsuc (l a)))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module hott.functions where

open import hott.core.universe
open import hott.core.equality

-- Composition of functions.
_∘_ : ∀ {ℓ₀ ℓ₁ ℓ₂ : Level} → {A : Type ℓ₀} {B : Type ℓ₁} {C : Type ℓ₂}
    → (B → C) → (A → B) → A → C
f ∘ g = λ x → f (g x)

-- The identity function.
id : ∀{ℓ} {A : Type ℓ} → A → A
id x = x

-- Change the order of arguments in a bivariate function.
flip : {a b c : Level}{A : Type a}{B : Type b}{C : Type c}
     → (A → B → C) → (B → A → C)
flip f b a = f a b

-- We want compostion to have very high precedence.
infixr 100 _∘_

-- The constant function.
constant : ∀ {ℓ₀ ℓ₁}{A : Type ℓ₀}{B : Type ℓ₁} → A → B → A
constant a b = a

-- Alternate syntax for dependent function type.
Π : ∀{ℓ₀ ℓ₁}{A : Type ℓ₀}(B : A → Type ℓ₁) → Type (ℓ₀ ⊔ ℓ₁)
Π {_}{_}{A} B = (a : A) → B(a)

-- One should use f ~ g to mean that f and g are homotopic.
_~_   : ∀{ℓ₀ ℓ₁}{A : Type ℓ₀}{B : Type ℓ₁} (f g : A → B) → Type (ℓ₁ ⊔ ℓ₀)
f ~ g = Π  λ x → f x ≡ g x

infixr 1   _~_

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
-- Non-indexed (plain) monads in form of Kleisli triple, presented in point-free style.

module Control.Monad.KleisliTriple where

open import Function using (id) renaming (_∘′_ to _∘_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Axiom.FunctionExtensionality
open import Control.Functor

record IsKleisliTriple (M : Set → Set) : Set₁ where

  -- Methods.

  field
    return : ∀ {A  } → A → M A
    bind′  : ∀ {A B} → (A → M B) → M A → M B

  -- Laws.

  field

    bind′-β : ∀ {A B} {k : A → M B} →

      bind′ k ∘ return ≡ k

    bind′-η : ∀ {A} →

      bind′ {A = A} return ≡ id

    bind′-∘ : ∀ {A B C} {k : A → M B} {l : B → M C} →

      bind′ (bind′ l ∘ k) ≡ bind′ l ∘ bind′ k

  -- Notations for bind′.

  -- Postfix category-theoretical notation.
  _✶ = bind′

  -- Infix Haskell notation.
  infixl 6 _=<<_
  _=<<_ = bind′

  -- Kleisli composition.

  infixl 6 _<=<_

  _<=<_ : ∀ {A B C : Set} (l : B → M C) (k : A → M B) → (A → M C)
  l <=< k = bind′ l ∘ k

  -- Functoriality.

  isFunctor : IsFunctor M
  isFunctor = record
    { ops  = record { map = map  }
    ; laws = record { map-id = bind′-η ; map-∘ = sym (map-∘-sym _ _) }
    }
    where
      map : ∀ {A B} → (A → B) → M A → M B
      map f = bind′ (return ∘ f)

      map-∘-sym : ∀ {A B C} (f : A → B) (g : B → C) → map g ∘ map f ≡ map (g ∘ f)
      map-∘-sym f g = begin
        map g ∘ map f                            ≡⟨⟩
        bind′ (return ∘ g) ∘ bind′ (return ∘ f)  ≡⟨ sym bind′-∘ ⟩
        bind′ (bind′ (return ∘ g) ∘ return ∘ f)  ≡⟨ cong (λ z → bind′ (z ∘ f)) bind′-β ⟩
        bind′ (return ∘ g ∘ f)                   ≡⟨⟩
        map (g ∘ f)                              ∎

  open IsFunctor isFunctor public

-- Monads in Kleisli Triple presentation.

record KleisliTriple : Set₁ where
  field
    M  : Set → Set
    M! : IsKleisliTriple M

  open IsKleisliTriple M! public

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An either-or-both data type
------------------------------------------------------------------------

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

module Data.These where

open import Level
open import Data.Sum.Base using (_⊎_; [_,_]′)
open import Function

data These {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  this  : A     → These A B
  that  :     B → These A B
  these : A → B → These A B

module _ {a b} {A : Set a} {B : Set b} where

  fromSum : A ⊎ B → These A B
  fromSum = [ this , that ]′

-- map

map : ∀ {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : Set b₁} {B₂ : Set b₂}
      (f : A₁ → A₂) (g : B₁ → B₂) → These A₁ B₁ → These A₂ B₂
map f g (this a)    = this (f a)
map f g (that b)    = that (g b)
map f g (these a b) = these (f a) (g b)

map₁ : ∀ {a₁ a₂ b} {A₁ : Set a₁} {A₂ : Set a₂} {B : Set b}
       (f : A₁ → A₂) → These A₁ B → These A₂ B
map₁ f = map f id

map₂ : ∀ {a b₁ b₂} {A : Set a} {B₁ : Set b₁} {B₂ : Set b₂}
       (g : B₁ → B₂) → These A B₁ → These A B₂
map₂ = map id

module _ {a b} {A : Set a} {B : Set b} where

-- fold

  fold : ∀ {c} {C : Set c} → (A → C) → (B → C) → (A → B → C) → These A B → C
  fold l r lr (this a)    = l a
  fold l r lr (that b)    = r b
  fold l r lr (these a b) = lr a b

-- swap

  swap : These A B → These B A
  swap = fold that this (flip these)

-- align

module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where

  alignWith : ∀ {e f} {E : Set e} {F : Set f} →
    (These A C → E) → (These B D → F) → These A B → These C D → These E F
  alignWith f g (this a)    (this c)    = this (f (these a c))
  alignWith f g (this a)    (that d)    = these (f (this a)) (g (that d))
  alignWith f g (this a)    (these c d) = these (f (these a c)) (g (that d))
  alignWith f g (that b)    (this c)    = these (f (that c)) (g (this b))
  alignWith f g (that b)    (that d)    = that (g (these b d))
  alignWith f g (that b)    (these c d) = these (f (that c)) (g (these b d))
  alignWith f g (these a b) (this c)    = these (f (these a c)) (g (this b))
  alignWith f g (these a b) (that d)    = these (f (this a)) (g (these b d))
  alignWith f g (these a b) (these c d) = these (f (these a c)) (g (these b d))

  align : These A B → These C D → These (These A C) (These B D)
  align = alignWith id id

module _ {a} {A : Set a} where

-- Projections.

  leftMost : These A A → A
  leftMost = fold id id const

  rightMost : These A A → A
  rightMost = fold id id (flip const)

  mergeThese : (A → A → A) → These A A → A
  mergeThese = fold id id


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Nullification.Properties where

open import Cubical.Foundations.Everything
open isPathSplitEquiv
open import Cubical.Modalities.Everything
open Modality
open import Cubical.HITs.Localization renaming (rec to Localize-rec)
open import Cubical.Data.Unit

open import Cubical.HITs.Nullification.Base

rec : ∀ {ℓ ℓ' ℓ''} {S : Type ℓ} {A : Type ℓ'} {B : Type ℓ''}
      → (nB : isNull S B) → (A → B) → Null S A → B
rec nB g ∣ x ∣ = g x
rec nB g (hub f) = fst (sec nB) (λ s → rec nB g (f s))
rec nB g (spoke f s i) = snd (sec nB) (λ s → rec nB g (f s)) i s
rec nB g (≡hub {x} {y} p i) = fst (secCong nB (rec nB g x) (rec nB g y)) (λ i s → rec nB g (p s i)) i
rec nB g (≡spoke {x} {y} p s i j) = snd (secCong nB (rec nB g x) (rec nB g y)) (λ i s → rec nB g (p s i)) i j s

toPathP⁻ : ∀ {ℓ} (A : I → Type ℓ) {x : A i0} {y : A i1} → x ≡ transport⁻ (λ i → A i) y → PathP A x y
toPathP⁻ A p i = toPathP {A = λ i → A (~ i)} (sym p) (~ i)

toPathP⁻-sq : ∀ {ℓ} {A : Type ℓ} (x : A) → Square (toPathP⁻ (λ _ → A) (λ _ → transport refl x)) refl
                                                  (transportRefl x) refl
toPathP⁻-sq x j i = hcomp (λ l → λ { (i = i0) → transportRefl x j
                                   ; (i = i1) → x ; (j = i1) → x })
                          (transportRefl x (i ∨ j))

module _ {ℓ ℓ' ℓ''} {S : Type ℓ} {A : Type ℓ'} {B : Null S A → Type ℓ''} where

  private
    secCongDep' : ∀ (nB : (x : Null S A) → isNull S (B x)) {x y : Null S A} (p : x ≡ y)
                  → (∀ (bx : B x) (by : B y) → hasSection (cong₂ (λ x (b : B x) (_ : S) → b) p))
    secCongDep' nB p = secCongDep (λ _ → const) p (λ a → secCong (nB a))

  elim : (nB : (x : Null S A) → isNull S (B x)) → ((a : A) → B ∣ a ∣) → (x : Null S A) → B x
  elim nB g ∣ x ∣ = g x
  elim nB g (hub f)
    = fst (sec (nB (hub f)))
          (λ s → transport (λ i → B (spoke f s (~ i))) (elim nB g (f s)))

  elim nB g (spoke f s i)
    = toPathP⁻ (λ i → B (spoke f s i))
               (funExt⁻ ( snd (sec (nB (hub f)))
                              (λ s → transport (λ i → B (spoke f s (~ i))) (elim nB g (f s))) ) s) i

  elim nB g (≡hub {x} {y} p i)
    = hcomp (λ k → λ { (i = i0) → transportRefl (elim nB g x) k
                     ; (i = i1) → transportRefl (elim nB g y) k })
            (fst (secCongDep' nB (≡hub p) (transport refl (elim nB g x)) (transport refl (elim nB g y)))
                 (λ i s → transport (λ j → B (≡spoke p s (~ j) i)) (elim nB g (p s i))) i)

  elim nB g (≡spoke {x} {y} p s j i)
    = hcomp (λ k → λ { (i = i0) → toPathP⁻-sq (elim nB g x) k j
                     ; (i = i1) → toPathP⁻-sq (elim nB g y) k j
                     ; (j = i1) → elim nB g (p s i) })
            (q₂ j i)

    where q₁ : Path (PathP (λ i → B (≡hub p i)) (transport refl (elim nB g x)) (transport refl (elim nB g y)))
                    (fst (secCongDep' nB (≡hub p) (transport refl (elim nB g x)) (transport refl (elim nB g y)))
                         (λ i s → transport (λ j → B (≡spoke p s (~ j) i)) (elim nB g (p s i))))
                    (λ i → transport (λ j → B (≡spoke p s (~ j) i)) (elim nB g (p s i)))
          q₁ j i = snd (secCongDep' nB (≡hub p) (transport refl (elim nB g x)) (transport refl (elim nB g y)))
                       (λ i s → transport (λ j → B (≡spoke p s (~ j) i)) (elim nB g (p s i))) j i s

          q₂ : PathP (λ j → PathP (λ i → B (≡spoke p s j i)) (toPathP⁻ (λ _ → B x) (λ _ → transport refl (elim nB g x)) j)
                                                             (toPathP⁻ (λ _ → B y) (λ _ → transport refl (elim nB g y)) j))
                     (fst (secCongDep' nB (≡hub p) (transport refl (elim nB g x)) (transport refl (elim nB g y)))
                        (λ i s → transport (λ j → B (≡spoke p s (~ j) i)) (elim nB g (p s i))))
                     (λ i → elim nB g (p s i))
          q₂ j i = toPathP⁻ (λ j → B (≡spoke p s j i)) (λ j → q₁ j i) j

-- nullification is a modality

NullModality : ∀ {ℓ} (S : Type ℓ) → Modality ℓ
isModal       (NullModality S) = isNull S
isModalIsProp (NullModality S) = isPropIsPathSplitEquiv _
◯             (NullModality S) = Null S
◯-isModal     (NullModality S) = isNull-Null
η             (NullModality S) = ∣_∣
◯-elim        (NullModality S) = elim
◯-elim-β      (NullModality S) = λ _ _ _ → refl
◯-=-isModal   (NullModality S) x y = fromIsEquiv _ e
  where e : isEquiv (λ (p : x ≡ y) → const {B = S} p)
        e = transport (λ i → isEquiv {B = funExtPath {A = S} {f = const x} {g = const y} (~ i)}
                                     (λ p → ua-gluePath funExtEquiv {x = const p} {y = cong const p} refl (~ i)))
                      (isEquivCong (_ , toIsEquiv _ isNull-Null))

idemNull : ∀ {ℓ} (S A : Type ℓ) → isNull S A → A ≃ Null S A
idemNull S A nA = ∣_∣ , isModalToIsEquiv (NullModality S) nA

-- nullification is localization at a map (S → 1)

module Null-iso-Localize {ℓ ℓ'} (S : Type ℓ) (A : Type ℓ') where

  to : Null S A → Localize {A = Unit} (λ _ → const {B = S} tt) A
  to ∣ x ∣ = ∣ x ∣
  to (hub f) = ext tt (to ∘ f) tt
  to (spoke f s i) = isExt tt (to ∘ f) s i
  to (≡hub {x} {y} p i) = ≡ext tt (const (to x)) (const (to y)) (cong to ∘ p) tt i
  to (≡spoke {x} {y} p s i j) = ≡isExt tt (const (to x)) (const (to y)) (cong to ∘ p) s i j

  from : Localize {A = Unit} (λ _ → const {B = S} tt) A → Null S A
  from ∣ x ∣ = ∣ x ∣
  from (ext tt f tt) = hub (from ∘ f)
  from (isExt tt f s i) = spoke (from ∘ f) s i
  from (≡ext tt g h p tt i) = ≡hub {x = from (g tt)} {from (h tt)} (cong from ∘ p) i
  from (≡isExt tt g h p s i j) = ≡spoke {x = from (g tt)} {from (h tt)} (cong from ∘ p) s i j

  to-from : ∀ (x : Localize {A = Unit} (λ _ → const {B = S} tt) A) → to (from x) ≡ x
  to-from ∣ x ∣ k = ∣ x ∣
  to-from (ext tt f tt) k = ext tt (λ s → to-from (f s) k) tt
  to-from (isExt tt f s i) k = isExt tt (λ s → to-from (f s) k) s i
  to-from (≡ext tt g h p tt i) k = ≡ext tt (λ _ → to-from (g tt) k) (λ _ → to-from (h tt) k) (λ s j → to-from (p s j) k) tt i
  to-from (≡isExt tt g h p s i j) k = ≡isExt tt (λ _ → to-from (g tt) k) (λ _ → to-from (h tt) k) (λ s j → to-from (p s j) k) s i j

  from-to : ∀ (x : Null S A) → from (to x) ≡ x
  from-to ∣ x ∣ k = ∣ x ∣
  from-to (hub f) k = hub (λ s → from-to (f s) k)
  from-to (spoke f s i) k = spoke (λ s → from-to (f s) k) s i
  from-to (≡hub {x} {y} p i) k = ≡hub {x = from-to x k} {from-to y k} (λ s j → from-to (p s j) k) i
  from-to (≡spoke {x} {y} p s i j) k = ≡spoke {x = from-to x k} {from-to y k} (λ s j → from-to (p s j) k) s i j

  isom : Iso (Null S A) (Localize {A = Unit} (λ _ → const {B = S} tt) A)
  isom = iso to from to-from from-to

Null≃Localize : ∀ {ℓ ℓ'} (S : Type ℓ) (A : Type ℓ') → Null S A ≃ Localize (λ _ → const tt) A
Null≃Localize S A = isoToEquiv (Null-iso-Localize.isom S A)

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.HITs.DunceCap.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

open import Cubical.HITs.S1 using (S¹; base; decodeEncode)
import Cubical.HITs.S1 as S¹

open import Cubical.HITs.MappingCones
open import Cubical.HITs.DunceCap.Base

-- DunceCone is contractible (easy)

Disk : Type₀
Disk = Cone (idfun S¹)

isContr-Disk : isContr Disk
fst isContr-Disk = hub
snd isContr-Disk (inj x)     i = spoke x i
snd isContr-Disk hub         i = hub
snd isContr-Disk (spoke x j) i = spoke x (i ∧ j)

dunceMap≡id : dunceMap ≡ idfun S¹
dunceMap≡id i base = base
dunceMap≡id i (S¹.loop j) = p i j
  where p : S¹.loop ⁻¹ ∙∙ S¹.loop ∙∙ S¹.loop ≡ S¹.loop
        p = sym (decodeEncode base (S¹.loop ⁻¹ ∙∙ S¹.loop ∙∙ S¹.loop)) ∙ sym (lUnit S¹.loop)

isContr-DunceCone : isContr DunceCone
isContr-DunceCone = subst isContr (cong Cone (sym dunceMap≡id)) isContr-Disk

-- Dunce is contractible (harder)

contrDunce : (d : Dunce) → d ≡ base
contrDunce base k = loop k
contrDunce (loop i) k = surf k i
contrDunce (surf i j) k
  = hcomp (λ l → λ { (i = i0) → surf k j
                   ; (i = i1) → cube l
                   ; (j = i0) → cube l
                   ; (j = i1) → cube l
                   ; (k = i0) → surf i j
                   ; (k = i1) → base })
          (surf (k ∨ i) j)
  where cube : I → Dunce
        cube l = hfill (λ i → λ { (k = i0) → loop i
                                ; (k = i1) → base
                                ; (l = i0) → loop (k ∨ i)
                                ; (l = i1) → surf k i })
                       (inS (loop k)) i

isContr-Dunce : isContr Dunce
fst isContr-Dunce = base
snd isContr-Dunce = sym ∘ contrDunce

Dunce≡DunceCone : Dunce ≡ DunceCone
Dunce≡DunceCone = ua (isContr→Equiv isContr-Dunce isContr-DunceCone)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Definition.Typed.Consequences.Syntactic where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Escape
open import Definition.LogicalRelation.Fundamental
open import Definition.Typed.Consequences.Injectivity

open import Tools.Product

-- the `with` syntax does not work

-- Syntactic validity of type equality.
syntacticEq : ∀ {A B rA Γ} → Γ ⊢ A ≡ B ^ rA → Γ ⊢ A ^ rA × Γ ⊢ B ^ rA
syntacticEq {A} {B} {rA} {Γ} A≡B =
  let X = fundamentalEq A≡B
      [Γ] = proj₁ X
      [A] = proj₁ (proj₂ X)
      [B] = proj₁ (proj₂ (proj₂ X))
  in escapeᵛ [Γ] [A] , escapeᵛ [Γ] [B]

-- Syntactic validity of terms.
syntacticTerm : ∀ {t A rA Γ} → Γ ⊢ t ∷ A ^ rA → Γ ⊢ A ^ rA
syntacticTerm t =
  let X = fundamentalTerm t
      [Γ] = proj₁ X
      [A] = proj₁ (proj₂ X)
      [t] = proj₂ (proj₂ X)
   in  escapeᵛ [Γ] [A]

-- Syntactic validity of term equality.
syntacticEqTerm : ∀ {t u A rA Γ} → Γ ⊢ t ≡ u ∷ A ^ rA → Γ ⊢ A ^ rA × (Γ ⊢ t ∷ A ^ rA × Γ ⊢ u ∷ A ^ rA)
syntacticEqTerm t≡u with fundamentalTermEq t≡u
syntacticEqTerm t≡u | [Γ] , modelsTermEq [A] [t] [u] [t≡u] =
  escapeᵛ [Γ] [A] , escapeTermᵛ [Γ] [A] [t] , escapeTermᵛ [Γ] [A] [u]

-- Syntactic validity of type reductions.
syntacticRed : ∀ {A B rA Γ} → Γ ⊢ A ⇒* B ^ rA → Γ ⊢ A ^ rA × Γ ⊢ B ^ rA
syntacticRed D =
  let X = fundamentalEq (subset* D)
      [Γ] = proj₁ X
      [A] = proj₁ (proj₂ X)
      [B] = proj₁ (proj₂ (proj₂ X))
  in escapeᵛ [Γ] [A] , escapeᵛ [Γ] [B]

-- Syntactic validity of term reductions.
syntacticRedTerm : ∀ {t u A Γ l} → Γ ⊢ t ⇒* u ∷ A ^ l → Γ ⊢ A ^ [ ! , l ] × (Γ ⊢ t ∷ A ^ [ ! , l ] × Γ ⊢ u ∷ A ^ [ ! , l ])
syntacticRedTerm d with fundamentalTermEq (subset*Term d)
syntacticRedTerm d | [Γ] , modelsTermEq [A] [t] [u] [t≡u] =
  escapeᵛ [Γ] [A] , escapeTermᵛ [Γ] [A] [t] , escapeTermᵛ [Γ] [A] [u]

-- Syntactic validity of Π-types.
syntacticΠ : ∀ {Γ F G rF lF lG rΠ lΠ} → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ rΠ , ι lΠ ] → Γ ⊢ F ^ [ rF , ι lF ] × Γ ∙ F ^ [ rF , ι lF ] ⊢ G ^ [ rΠ , ι lG ]
syntacticΠ ΠFG with injectivity (refl ΠFG)
syntacticΠ ΠFG | F≡F , rF≡rF , lF≡lF , lG≡lG , G≡G = proj₁ (syntacticEq F≡F) , proj₁ (syntacticEq G≡G)


text:
-- Andreas, 2012-03-15, example by Ulf
-- {-# OPTIONS -v tc.meta:20 #-}
module Issue479 where

import Common.Level
open import Common.Equality

data ⊥ : Set where
data Bool : Set where true false : Bool

X       : Bool
X=true  : X ≡ true
X≠false : X ≡ false → ⊥
X = _
X≠false ()
X=true = refl

-- The emptyness check for X ≡ false should be postponed until
-- X has been solved to true.


text:
-- Andreas, 2017-10-02, issue #2785, reported by ...

-- {-# OPTIONS -v scope.extendedLambda:100 #-}

{-# OPTIONS --allow-unsolved-metas #-}

foo : _
foo = {!foo λ {x y → foo}!}  -- C-c C-r

-- Upon refine (C-c C-r), error was:
--
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs:721

-- Now: unsolved metas and constraints.


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to All
------------------------------------------------------------------------

module Data.List.All.Properties where

open import Data.Bool
open import Data.Bool.Properties
open import Data.Empty
open import Data.List as List
import Data.List.Any as Any; open Any.Membership-≡
open import Data.List.All as All using (All; []; _∷_)
open import Data.List.Any using (Any; here; there)
open import Data.Product as Prod
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; module Equivalence)
open import Function.Inverse using (_↔_)
open import Function.Surjection using (_↠_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_)

-- Functions can be shifted between the predicate and the list.

All-map : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
            {f : A → B} {xs} →
          All (P ∘ f) xs → All P (List.map f xs)
All-map []       = []
All-map (p ∷ ps) = p ∷ All-map ps

map-All : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
            {f : A → B} {xs} →
          All P (List.map f xs) → All (P ∘ f) xs
map-All {xs = []}    []       = []
map-All {xs = _ ∷ _} (p ∷ ps) = p ∷ map-All ps

-- A variant of All.map.

gmap : ∀ {a b p q}
         {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q}
         {f : A → B} →
       P ⋐ Q ∘ f → All P ⋐ All Q ∘ List.map f
gmap g = All-map ∘ All.map g

-- All and all are related via T.

All-all : ∀ {a} {A : Set a} (p : A → Bool) {xs} →
          All (T ∘ p) xs → T (all p xs)
All-all p []         = _
All-all p (px ∷ pxs) = Equivalence.from T-∧ ⟨$⟩ (px , All-all p pxs)

all-All : ∀ {a} {A : Set a} (p : A → Bool) xs →
          T (all p xs) → All (T ∘ p) xs
all-All p []       _     = []
all-All p (x ∷ xs) px∷xs with Equivalence.to (T-∧ {p x}) ⟨$⟩ px∷xs
all-All p (x ∷ xs) px∷xs | (px , pxs) = px ∷ all-All p xs pxs

-- All is anti-monotone.

anti-mono : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} →
            xs ⊆ ys → All P ys → All P xs
anti-mono xs⊆ys pys = All.tabulate (All.lookup pys ∘ xs⊆ys)

-- all is anti-monotone.

all-anti-mono : ∀ {a} {A : Set a} (p : A → Bool) {xs ys} →
                xs ⊆ ys → T (all p ys) → T (all p xs)
all-anti-mono p xs⊆ys = All-all p ∘ anti-mono xs⊆ys ∘ all-All p _

-- All P (xs ++ ys) is isomorphic to All P xs and All P ys.

private

  ++⁺ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys : List A} →
        All P xs → All P ys → All P (xs ++ ys)
  ++⁺ []         pys = pys
  ++⁺ (px ∷ pxs) pys = px ∷ ++⁺ pxs pys

  ++⁻ : ∀ {a p} {A : Set a} {P : A → Set p} (xs : List A) {ys} →
        All P (xs ++ ys) → All P xs × All P ys
  ++⁻ []       p          = [] , p
  ++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map (_∷_ px) id $ ++⁻ _ pxs

  ++⁺∘++⁻ : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys}
            (p : All P (xs ++ ys)) → uncurry′ ++⁺ (++⁻ xs p) ≡ p
  ++⁺∘++⁻ []       p          = P.refl
  ++⁺∘++⁻ (x ∷ xs) (px ∷ pxs) = P.cong (_∷_ px) $ ++⁺∘++⁻ xs pxs

  ++⁻∘++⁺ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys}
            (p : All P xs × All P ys) → ++⁻ xs (uncurry ++⁺ p) ≡ p
  ++⁻∘++⁺ ([]       , pys) = P.refl
  ++⁻∘++⁺ (px ∷ pxs , pys) rewrite ++⁻∘++⁺ (pxs , pys) = P.refl

++↔ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} →
      (All P xs × All P ys) ↔ All P (xs ++ ys)
++↔ {P = P} {xs = xs} = record
  { to         = P.→-to-⟶ $ uncurry ++⁺
  ; from       = P.→-to-⟶ $ ++⁻ xs
  ; inverse-of = record
    { left-inverse-of  = ++⁻∘++⁺
    ; right-inverse-of = ++⁺∘++⁻ xs
    }
  }

-- Three lemmas relating Any, All and negation.

¬Any↠All¬ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
            ¬ Any P xs ↠ All (¬_ ∘ P) xs
¬Any↠All¬ {P = P} = record
  { to         = P.→-to-⟶ (to _)
  ; surjective = record
    { from             = P.→-to-⟶ from
    ; right-inverse-of = to∘from
    }
  }
  where
  to : ∀ xs → ¬ Any P xs → All (¬_ ∘ P) xs
  to []       ¬p = []
  to (x ∷ xs) ¬p = ¬p ∘ here ∷ to xs (¬p ∘ there)

  from : ∀ {xs} → All (¬_ ∘ P) xs → ¬ Any P xs
  from []        ()
  from (¬p ∷ _)  (here  p) = ¬p p
  from (_  ∷ ¬p) (there p) = from ¬p p

  to∘from : ∀ {xs} (¬p : All (¬_ ∘ P) xs) → to xs (from ¬p) ≡ ¬p
  to∘from []         = P.refl
  to∘from (¬p ∷ ¬ps) = P.cong₂ _∷_ P.refl (to∘from ¬ps)

  -- If equality of functions were extensional, then the surjection
  -- could be strengthened to a bijection.

  from∘to : P.Extensionality _ _ →
            ∀ xs → (¬p : ¬ Any P xs) → from (to xs ¬p) ≡ ¬p
  from∘to ext []       ¬p = ext λ ()
  from∘to ext (x ∷ xs) ¬p = ext λ
    { (here p)  → P.refl
    ; (there p) → P.cong (λ f → f p) $ from∘to ext xs (¬p ∘ there)
    }

Any¬→¬All : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
            Any (¬_ ∘ P) xs → ¬ All P xs
Any¬→¬All (here  ¬p) = ¬p           ∘ All.head
Any¬→¬All (there ¬p) = Any¬→¬All ¬p ∘ All.tail

Any¬⇔¬All : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
            Decidable P → Any (¬_ ∘ P) xs ⇔ ¬ All P xs
Any¬⇔¬All {P = P} dec = record
  { to   = P.→-to-⟶ Any¬→¬All
  ; from = P.→-to-⟶ (from _)
  }
  where
  from : ∀ xs → ¬ All P xs → Any (¬_ ∘ P) xs
  from []       ¬∀ = ⊥-elim (¬∀ [])
  from (x ∷ xs) ¬∀ with dec x
  ... | yes p = there (from xs (¬∀ ∘ _∷_ p))
  ... | no ¬p = here ¬p

  -- If equality of functions were extensional, then the logical
  -- equivalence could be strengthened to a surjection.

  to∘from : P.Extensionality _ _ →
            ∀ {xs} (¬∀ : ¬ All P xs) → Any¬→¬All (from xs ¬∀) ≡ ¬∀
  to∘from ext ¬∀ = ext (⊥-elim ∘ ¬∀)


text:
open import slots.imports
open import slots.defs

module slots.bruteforce {cfg : config}(g : game cfg) where

open config cfg
open game g

total : ℕ
total = V.foldl _ (λ i r → i * L.length r) 1 reels

lineWin : Line → Win/Bet
lineWin [] = 0
lineWin (f₀ ∷ fs) = lineWin′ w ws fs where
  winLine = V.lookup f₀ winTable
  w = V.head winLine
  ws = V.tail winLine

  lineWin′ : ∀ {n} →
    Win/Bet → Vec Win/Bet n → Vec Fruit n → Win/Bet
  lineWin′ w [] [] = w
  lineWin′ w (w′ ∷ ws) (f ∷ fs) with f₀ F.≟ f
  ... | yes p = lineWin′ w′ ws fs
  ... | no ¬p = w

allLines : List Line
allLines = V.foldr (List ∘ Vec Fruit)
  (λ r → L.concatMap λ l → L.map (_∷ l) r)
  ([] ∷ []) reels

win : ℕ
win = L.sum ∘ L.map lineWin $ allLines

rtp : ℕ × ℕ
rtp = win , total

max_stars_repo_name: semenov-vladyslav/slots-agda

max_issues_repo_name: semenov-vladyslav/slots-agda

max_forks_repo_name: semenov-vladyslav/slots-agda


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

module ConcretePermutationProperties where

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; module ≡-Reasoning; proof-irrelevance)

--

-- open import FinVecProperties using (∘̂-assoc; ∘̂-lid; ∘̂-rid)
open import ConcretePermutation
------------------------------------------------------------------------------
-- Properties of vectors where are only used to prove some properties
-- of concrete permutations -> do not export them.
private
  open import Data.Nat using (ℕ)
  open import Data.Fin using (Fin)
  open import Data.Vec using (Vec)
  open import Data.Vec.Properties using (lookup-allFin)
  open import Proofs using (finext; lookupassoc; _!!_)

  ∘̂-assoc : {m₁ m₂ m₃ m₄ : ℕ} →
           (a : Vec (Fin m₂) m₁) (b : Vec (Fin m₃) m₂) (c : Vec (Fin m₄) m₃) →
           a ∘̂ (b ∘̂ c) ≡ (a ∘̂ b) ∘̂ c
  ∘̂-assoc a b c = finext (lookupassoc a b c)

  ∘̂-rid : {m n : ℕ} → (π : Vec (Fin m) n) → π ∘̂ 1C ≡ π
  ∘̂-rid π = trans (finext (λ i → lookup-allFin (π !! i))) (cauchyext π)

  ∘̂-lid : {m n : ℕ} → (π : Vec (Fin m) n) → 1C ∘̂ π ≡ π
  ∘̂-lid π = trans (finext (λ i → cong (_!!_ π) (lookup-allFin i))) (cauchyext π)

------------------------------------------------------------------------------
-- Properties of concrete permutations that are needed to show that
-- this is also a symmetric rig groupoid

-- If the forward components are equal, then so are the backward ones

πᵒ≡ : ∀ {m n} → (π₁ π₂ : CPerm m n) → (CPerm.π π₁ ≡ CPerm.π π₂) →
      (CPerm.πᵒ π₁ ≡ CPerm.πᵒ π₂)
πᵒ≡ {n} (cp π πᵒ αp βp) (cp .π πᵒ₁ αp₁ βp₁) refl =
  begin (
    πᵒ                  ≡⟨ sym (∘̂-rid πᵒ) ⟩
    πᵒ ∘̂ 1C          ≡⟨  cong (_∘̂_ πᵒ) (sym αp₁)  ⟩
    πᵒ ∘̂ (π ∘̂ πᵒ₁)      ≡⟨ ∘̂-assoc πᵒ π πᵒ₁ ⟩
    (πᵒ ∘̂ π) ∘̂ πᵒ₁      ≡⟨ cong (λ x → x ∘̂ πᵒ₁) βp ⟩
    1C ∘̂ πᵒ₁            ≡⟨ ∘̂-lid πᵒ₁ ⟩
    πᵒ₁ ∎)
  where open ≡-Reasoning

-- If the forward components are equal, then so are the entire
-- concrete permutations

p≡ : ∀ {m n} → {π₁ π₂ : CPerm m n} → (CPerm.π π₁ ≡ CPerm.π π₂) → π₁ ≡ π₂
p≡ {m} {n} {cp π πᵒ αp βp} {cp .π πᵒ₁ αp₁ βp₁} refl with
  πᵒ≡ (cp π πᵒ αp βp) (cp π πᵒ₁ αp₁ βp₁) refl
p≡ {m} {n} {cp π πᵒ αp βp} {cp .π .πᵒ αp₁ βp₁} refl | refl
  with proof-irrelevance αp αp₁ | proof-irrelevance βp βp₁
p≡ {m} {n} {cp π πᵒ αp βp} {cp .π .πᵒ .αp .βp} refl | refl | refl | refl = refl

------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- An implementation of the Thue-Morse sequence
------------------------------------------------------------------------

-- This module is a variant of ThueMorse. The difference is that, in
-- this module, the cast operation takes an inequality instead of an
-- equality, and that this module does not contain any correctness
-- proofs.

module ThueMorseLeq where

open import Codata.Musical.Notation
open import Codata.Musical.Stream using (Stream; _≈_)
open Codata.Musical.Stream.Stream
open import Data.Bool using (Bool; not); open Data.Bool.Bool
open import Data.Nat using (ℕ); open Data.Nat.ℕ
open import Data.Vec using (Vec; _∷ʳ_); open Data.Vec.Vec

------------------------------------------------------------------------
-- Chunks

-- A value of type Chunks describes how a stream is generated. Note
-- that an infinite sequence of empty chunks is not allowed.

data Chunks : Set where
  -- Start the next chunk.
  next : (m :   Chunks) → Chunks
  -- Cons an element to the current chunk.
  cons : (m : ∞ Chunks) → Chunks

-- Inequality of chunks.

infix 4 _≥C_

data _≥C_ : Chunks → Chunks → Set where
  next  : ∀ {m m′} (m≥m′ :      m ≥C   m′ ) → next m ≥C next m′
  cons  : ∀ {m m′} (m≥m′ : ∞ (♭ m ≥C ♭ m′)) → cons m ≥C cons m′
  consˡ : ∀ {m m′} (m≥m′ :    ♭ m ≥C   m′ ) → cons m ≥C      m′

------------------------------------------------------------------------
-- Chunk transformers

tailC : Chunks → Chunks
tailC (next m) = next (tailC m)
tailC (cons m) = ♭ m

mutual

  evensC : Chunks → Chunks
  evensC (next m) = next (evensC m)
  evensC (cons m) = cons (♯ oddsC (♭ m))

  oddsC : Chunks → Chunks
  oddsC (next m) = next (oddsC m)
  oddsC (cons m) = evensC (♭ m)

infixr 5 _⋎C_

-- Note that care is taken to create as few and large chunks as
-- possible (see also _⋎W_).

_⋎C_ : Chunks → Chunks → Chunks
next m ⋎C next m′ = next (m ⋎C      m′)   -- Two chunks in, one out.
next m ⋎C cons m′ = next (m ⋎C cons m′)
cons m ⋎C      m′ = cons (♯ (m′ ⋎C ♭ m))

------------------------------------------------------------------------
-- Stream programs

-- StreamP m A encodes programs which generate streams with chunk
-- sizes given by m.

infixr 5 _∷_ _⋎_

data StreamP : Chunks → Set → Set₁ where
  [_]     : ∀ {m A} (xs : ∞ (StreamP m A)) → StreamP (next m) A
  _∷_     : ∀ {m A} (x : A) (xs : StreamP (♭ m) A) → StreamP (cons m) A
  tail    : ∀ {m A} (xs : StreamP m A) → StreamP (tailC m) A
  evens   : ∀ {m A} (xs : StreamP m A) → StreamP (evensC m) A
  odds    : ∀ {m A} (xs : StreamP m A) → StreamP (oddsC m) A
  _⋎_     : ∀ {m m′ A} (xs : StreamP m A) (ys : StreamP m′ A) →
            StreamP (m ⋎C m′) A
  map     : ∀ {m A B} (f : A → B) (xs : StreamP m A) → StreamP m B
  cast    : ∀ {m m′ A} (ok : m ≥C m′) (xs : StreamP m A) → StreamP m′ A

data StreamW : Chunks → Set → Set₁ where
  [_] : ∀ {m A} (xs : StreamP m A) → StreamW (next m) A
  _∷_ : ∀ {m A} (x : A) (xs : StreamW (♭ m) A) → StreamW (cons m) A

program : ∀ {m A} → StreamW m A → StreamP m A
program [ xs ]   = [ ♯ xs ]
program (x ∷ xs) = x ∷ program xs

tailW : ∀ {m A} → StreamW m A → StreamW (tailC m) A
tailW [ xs ]   = [ tail xs ]
tailW (x ∷ xs) = xs

mutual

  evensW : ∀ {m A} → StreamW m A → StreamW (evensC m) A
  evensW [ xs ]   = [ evens xs ]
  evensW (x ∷ xs) = x ∷ oddsW xs

  oddsW : ∀ {m A} → StreamW m A → StreamW (oddsC m) A
  oddsW [ xs ]   = [ odds xs ]
  oddsW (x ∷ xs) = evensW xs

infixr 5 _⋎W_

-- Note: Uses swapping of arguments.

_⋎W_ : ∀ {m m′ A} → StreamW m A → StreamW m′ A → StreamW (m ⋎C m′) A
[ xs ]   ⋎W [ ys ]   = [ xs ⋎ ys ]
[ xs ]   ⋎W (y ∷ ys) = [ xs ⋎ program (y ∷ ys) ]
(x ∷ xs) ⋎W ys       = x ∷ ys ⋎W xs

mapW : ∀ {m A B} → (A → B) → StreamW m A → StreamW m B
mapW f [ xs ]   = [ map f xs ]
mapW f (x ∷ xs) = f x ∷ mapW f xs

module Cast where

  infixr 6 _+_
  infixr 5 _++_

  _+_ : ℕ → Chunks → Chunks
  zero  + m = m
  suc n + m = cons (♯ (n + m))

  _++_ : ∀ {A n m} → Vec A n → StreamP m A → StreamP (n + m) A
  []       ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

  +ˡ : ∀ {m m′} n → m ≥C m′ → n + m ≥C m′
  +ˡ zero    m≥m′ = m≥m′
  +ˡ (suc n) m≥m′ = consˡ (+ˡ n m≥m′)

  castW : ∀ {n m m′ A} → m ≥C m′ → Vec A n → StreamW m A → StreamW m′ A
  castW {n} (next  m≥m′) xs       [ ys ]   = [ cast (+ˡ n m≥m′) (xs ++ ys) ]
  castW     (cons  m≥m′) []       (y ∷ ys) = y ∷ castW (♭ m≥m′) []        ys
  castW     (cons  m≥m′) (x ∷ xs) (y ∷ ys) = x ∷ castW (♭ m≥m′) (xs ∷ʳ y) ys
  castW     (consˡ m≥m′) xs       (y ∷ ys) = castW m≥m′ (xs ∷ʳ y) ys

whnf : ∀ {m A} → StreamP m A → StreamW m A
whnf [ xs ]         = [ ♭ xs ]
whnf (x ∷ xs)       = x ∷ whnf xs
whnf (tail xs)      = tailW (whnf xs)
whnf (evens xs)     = evensW (whnf xs)
whnf (odds xs)      = oddsW (whnf xs)
whnf (xs ⋎ ys)      = whnf xs ⋎W whnf ys
whnf (map f xs)     = mapW f (whnf xs)
whnf (cast m≥m′ xs) = Cast.castW m≥m′ [] (whnf xs)

mutual

  ⟦_⟧W : ∀ {m A} → StreamW m A → Stream A
  ⟦ [ xs ] ⟧W = ⟦ xs ⟧P
  ⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧W

  ⟦_⟧P : ∀ {m A} → StreamP m A → Stream A
  ⟦ xs ⟧P = ⟦ whnf xs ⟧W

------------------------------------------------------------------------
-- The Thue-Morse sequence

[ccn]ω : Chunks
[ccn]ω = cons (♯ cons (♯ next [ccn]ω))

[cn]²[ccn]ω : Chunks
[cn]²[ccn]ω = cons (♯ next (cons (♯ next [ccn]ω)))

[cn]³[ccn]ω : Chunks
[cn]³[ccn]ω = cons (♯ next [cn]²[ccn]ω)

lemma₁ : oddsC [ccn]ω ⋎C [ccn]ω ≥C [ccn]ω
lemma₁ = cons (♯ cons (♯ next (cons (♯ cons (♯ next lemma₁)))))

lemma : evensC [cn]³[ccn]ω ⋎C tailC [cn]³[ccn]ω ≥C [cn]²[ccn]ω
lemma = cons (♯ next (cons (♯ next (cons (♯ cons (♯ next lemma₁))))))

thueMorse : StreamP [cn]³[ccn]ω Bool
thueMorse =
  false ∷ [ ♯ cast lemma (map not (evens thueMorse) ⋎ tail thueMorse) ]

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-# OPTIONS --warning=error #-}
module UnknownNameInFixityDecl where

infix 40 _+_
infixr 60 _*_


text:
module Structure.Relator.Function.Multi where

open import Data.Tuple.RaiseTypeᵣ
import      Data.Tuple.RaiseTypeᵣ.Functions as RaiseType
open import Function.Multi
import      Function.Multi.Functions as Multi
import      Lvl
import      Lvl.MultiFunctions as Lvl
open import Logic
open import Logic.Predicate
open import Logic.Predicate.Multi
open import Functional
open import Numeral.Natural
import      Structure.Function.Multi as Multi
open import Structure.Setoid
open import Type

private variable ℓ ℓₑ : Lvl.Level

module _ (n : ℕ) {ℓ𝓈}{ℓ₁ ℓ₂} {Xs : Types{n}(ℓ𝓈)}{Y : Type{ℓ₁}} where
  module Names where
    -- A relator is total when every LHS have at least one RHS in which the relation holds.
    Total : (Xs ⇉ (Y → Stmt{ℓ₂})) → Stmt
    Total(φ) = ∀₊(n)(Multi.compose(n) ∃ φ)

    module _ ⦃ equiv-Y : Equiv{ℓₑ}(Y) ⦄ where
      -- A relator is a function when every LHS have at least one RHS in which the relation holds.
      Function : ∀{ℓ𝓈ₑ} → (RaiseType.mapWithLvls(\X ℓₑ → Equiv{ℓₑ}(X)) Xs ℓ𝓈ₑ) ⇉ᵢₙₛₜ ((Xs ⇉ (Y → Type{ℓ₂})) → Stmt)
      Function = Multi.expl-to-inst(n) (Multi.compose(n) (_$₂_) (Multi.inst-to-expl(n) (Multi.Names.RelationReplacement(f ↦ g ↦ ∀{y₁ y₂} → f(y₁) → g(y₂) → (y₁ ≡ y₂))(n))))

  record Total(φ : Xs ⇉ (Y → Stmt{ℓ₂})) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ (Lvl.⨆ ℓ𝓈)} where
    constructor intro
    field proof : Names.Total(φ)

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:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.Rels where

open import Data.Product
open import Function
open import Level
open import Relation.Binary
open import Relation.Binary.Construct.Composition
open import Relation.Binary.PropositionalEquality

open import Categories.Category.Core

-- the category whose objects are sets and whose morphisms are binary relations.
Rels : ∀ o ℓ → Category (suc o) (suc (o ⊔ ℓ)) (o ⊔ ℓ)
Rels o ℓ = record
  { Obj = Set o
  ; _⇒_ = λ A B → REL A B (o ⊔ ℓ)
  ; _≈_ = λ _L_ _R_ → ∀ x y → (x L y → x R y) × (x R y → x L y)
  ; id = λ x y → Lift ℓ (x ≡ y)
  ; _∘_ = λ L R → R ; L
  ; assoc = λ x y →
    (λ { (b , fxb , c , gbc , hcy) → c , (b , fxb , gbc) , hcy }) ,
    (λ { (c , (b , fxb , gbc) , hcy) → b , fxb , c , gbc , hcy })
  ; sym-assoc = λ x y →
    (λ { (c , (b , fxb , gbc) , hcy) → b , fxb , c , gbc , hcy }) ,
    (λ { (b , fxb , c , gbc , hcy) → c , (b , fxb , gbc) , hcy })
  ; identityˡ = λ x y → (λ { (.y , fxy , lift refl) → fxy }) , λ fxy → y , fxy , lift refl
  ; identityʳ = λ x y → (λ { (.x , lift refl , fxy) → fxy }) , λ fxy → x , lift refl , fxy
  ; identity² = λ x y →
    (λ { (_ , lift refl , lift refl) → lift refl }) ,
    (λ { (lift refl) → _ , lift refl , lift refl })
  ; equiv = record
    { refl = λ _ _ → id , id
    ; sym = λ p x y → swap (p x y)
    ; trans = λ p q x y → zip (flip _∘′_) _∘′_ (p x y) (q x y)
    }
  ; ∘-resp-≈ = λ p q x y →
    (λ { (b , gxb , fby) → b , proj₁ (q x b) gxb , proj₁ (p b y) fby }) ,
    (λ { (b , ixb , hby) → b , proj₂ (q x b) ixb , proj₂ (p b y) hby })
  }


text:
module Imports.Issue5198 (Y : Set₁) where

record R : Set₂ where
  constructor mkR
  field
    A : Set₁


text:
module Formalization.SKICombinatorCalculus where

import      Lvl
import      Function
open import Functional using (_∘_)
open import Type
open import Structure.Relator.Properties
open import Syntax.Transitivity

data Term : Type{Lvl.𝟎} where
  S   : Term               -- Fusion
  K   : Term               -- Constant
  _·_ : Term → Term → Term
infixl 30 _·_

pattern B  = S · (K · S) · K                 -- Composition
pattern C  = S · (S · (K · B) · S) · (K · K) -- Swapped application
pattern I  = S · K · K                       -- Identity of operation
pattern SA = (S · I) · I                     -- Self application
pattern W  = S · S · (S · K)                 --
pattern Ω  = SA · SA                         --
pattern SW = S · (K · (S · I)) · K           -- Swapped operation
T = C
Z = B
-- Z = C · (C · (B · N · (S · I · I)) · Ω) · I

{- TODO: Is this possible?
term-fn-type : ∀{ℓ} → Term → Type{Lvl.𝐒(ℓ)}
term-fn-type {ℓ} S = ∀{X Y Z : Type{ℓ}} → (X → (Y → Z)) → (X → Y) → (X → Z)
term-fn-type {ℓ} K = ∀{X Y : Type{ℓ}} → Y → X → Y
term-fn-type {ℓ} (x · y) = {!term-fn-type {ℓ} x!}
-}

module Derivation where
  -- TODO: But there are no base cases?
  data deriv : Term → Type{Lvl.𝟎} where
    constant : ∀{α β γ ι} → deriv(α · ((K · β) · γ) · ι) → deriv(α · β · ι)
    fuse     : ∀{α β γ δ ι} → deriv(α · (((S · β) · γ) · δ) · ι) → deriv(α · ((β · δ) · (γ · δ)) · ι)

  _⇒_ : Term → Term → Type
  a ⇒ b = ∀{α ι} → deriv(α · a · ι) → deriv(α · b · ι)

  identity : ∀{β} → ((I · β) ⇒ β)
  identity = constant ∘ fuse

  -- composition : ∀{α ι a b c} → deriv(α · (B · a · b · c) · ι) → deriv(α · ((a · (b · c))) · ι)
  -- composition = {!!}

-- TODO: Is this really correct? Should be similar to deriv
data _⟶_ : Term → Term → Type{Lvl.𝟎} where -- TODO: Use reflexive-transitive closure instead
  constant : ∀{c t} → (((K · c) · t) ⟶ c)
  fuse     : ∀{a b c} → ((((S · a) · b) · c) ⟶ ((a · c) · (b · c)))

  comp     : ∀{a₁ a₂ b₁ b₂} → (a₁ ⟶ a₂) → (b₁ ⟶ b₂) → ((a₁ · b₁) ⟶ (a₂ · b₂))
  refl     : ∀{a} → (a ⟶ a)
  trans    : ∀{a b c} → (a ⟶ b) → (b ⟶ c) → (a ⟶ c)
infixl 29 _⟶_

instance
  [⟶]-reflexivity : Reflexivity(_⟶_)
  [⟶]-reflexivity = intro refl

instance
  [⟶]-transitivity : Transitivity(_⟶_)
  [⟶]-transitivity = intro trans

-- identity : ∀{t} → ((I · t) ⟶ t)
pattern identity = trans fuse constant

-- compₗ : ∀{a₁ a₂ b} → (a₁ ⟶ a₂) → ((a₁ · b) ⟶ (a₂ · b))
pattern compₗ p = comp p refl

-- compᵣ : ∀{a b₁ b₂} → (b₁ ⟶ b₂) → ((a · b₁) ⟶ (a · b₂))
pattern compᵣ p = comp refl p

composition : ∀{a b c} → ((B · a · b · c) ⟶ (a · (b · c)))
composition {a}{b}{c} =
  B · a · b · c                     🝖-[ refl ]
  ((S · (K · S) · K · a) · b) · c   🝖-[ compₗ (compₗ fuse) ]
  (((K · S · a) · (K · a)) · b) · c 🝖-[ compₗ (compₗ (compₗ constant)) ]
  ((S · (K · a)) · b) · c           🝖-[ fuse ]
  (K · a · c) · (b · c)             🝖-[ compₗ constant ]
  a · (b · c)                       🝖-end

swapped-application : ∀{a b c} → ((C · a · b · c) ⟶ ((a · c) · b))
swapped-application {a}{b}{c} =
  C · a · b · c                               🝖-[ refl ]
  S · (S · (K · B) · S) · (K · K) · a · b · c 🝖-[ compₗ (compₗ fuse) ]
  (S · (K · B) · S · a) · (K · K · a) · b · c 🝖-[ compₗ (compₗ (comp fuse constant)) ]
  (K · B · a · (S · a)) · K · b · c           🝖-[ compₗ (compₗ (compₗ (compₗ constant))) ]
  (B · (S · a)) · K · b · c                   🝖-[ compₗ composition ]
  (S · a) · (K · b) · c                       🝖-[ fuse ]
  (a · c) · (K · b · c)                       🝖-[ compᵣ constant ]
  (a · c) · b                                 🝖-end

apply-self : ∀{t} → ((SA · t) ⟶ (t · t))
apply-self = trans fuse (comp identity identity)

swapping : ∀{a b} → ((SW · a · b) ⟶ (b · a))
swapping {a}{b} =
  S · (K · (S · I)) · K · a · b   🝖-[ compₗ fuse ]
  (K · (S · I) · a) · (K · a) · b 🝖-[ compₗ (compₗ constant) ]
  (S · I) · (K · a) · b           🝖-[ fuse ]
  I · b · (K · a · b)             🝖-[ comp identity constant ]
  b · a                           🝖-end

module Boolean where
  TRUE  = K             -- True
  FALSE = S · K         -- False
  NOT   = FALSE · TRUE  -- Not (Negation)
  OR    = TRUE          -- Or (Disjunction)
  AND   = FALSE         -- And (Conjunction)

  IsTrue : Term → Type{Lvl.𝟎}
  IsTrue(a) = ∀{t f} → ((a · t · f) ⟶ t)

  IsFalse : Term → Type{Lvl.𝟎}
  IsFalse(a) = ∀{t f} → ((a · t · f) ⟶ f)

  reduce-true-is-true : ∀{t} → (t ⟶ TRUE) → IsTrue(t)
  reduce-true-is-true tT = (compₗ (compₗ tT)) 🝖 constant

  reduce-false-is-false : ∀{t} → (t ⟶ FALSE) → IsFalse(t)
  reduce-false-is-false tT = (compₗ (compₗ tT)) 🝖 identity

  true : IsTrue(TRUE)
  true = constant

  false : IsFalse(FALSE)
  false = identity

  not-true-is-false : ∀{t} → IsTrue(t) → IsFalse(t · NOT)
  not-true-is-false t-true = (compₗ t-true) 🝖 fuse 🝖 constant

  {-not-false-is-true : ∀{t} → IsFalse(t) → IsTrue(t · NOT)
  not-false-is-true {term} t-false {t}{f} =
    term · NOT · t · f         🝖-[ refl ]
    term · (S · K · K) · t · f 🝖-[ {!!} ]
    f · (S · K · K) · t · f 🝖-[ {!!} ]
    t                          🝖-end
  -}

  not-true : IsFalse(TRUE · NOT)
  not-true {t}{f} = not-true-is-false constant
    {-TRUE · NOT · t · f            🝖-[ refl ]
    TRUE · (FALSE · TRUE) · t · f 🝖-[ refl ]
    K · (S · K · K) · t · f       🝖-[ compₗ constant ]
    S · K · K · f                 🝖-[ fuse ]
    K · f · (K · f)               🝖-[ constant ]
    f                             🝖-end-}

  {-
  not-false : IsTrue(FALSE · NOT)
  not-false {t}{f} =
    FALSE · NOT · t · f            🝖-[ refl ]
    FALSE · (FALSE · TRUE) · t · f 🝖-[ refl ]
    S · K · (S · K · K) · t · f    🝖-[ compₗ fuse ]
    K · t · (S · K · K · t) · f    🝖-[ compₗ constant ]
    t · f                          🝖-[ {!!} ] -- TODO: ???
    t                              🝖-end
  -- not-false-is-true identity
  -}

  or-true-true : IsTrue(TRUE · OR · TRUE)
  or-true-true = reduce-true-is-true constant

  or-true-false : IsTrue(TRUE · OR · FALSE)
  or-true-false = reduce-true-is-true constant

  or-false-true : IsTrue(FALSE · OR · TRUE)
  or-false-true = reduce-true-is-true(fuse 🝖 constant)

  or-false-true2 : IsTrue(FALSE · OR · TRUE)
  or-false-true2 = reduce-true-is-true(fuse 🝖 constant)

  or-false-false : IsFalse(FALSE · OR · FALSE)
  or-false-false = reduce-false-is-false(fuse 🝖 constant)

  and-true-true : IsTrue(TRUE · TRUE · AND)
  and-true-true = reduce-true-is-true(constant)

  and-true-false : IsFalse(TRUE · FALSE · AND)
  and-true-false = reduce-false-is-false(constant)

  and-false-true : IsFalse(FALSE · TRUE · AND)
  and-false-true = reduce-false-is-false(identity)

  and-false-false : IsFalse(FALSE · FALSE · AND)
  and-false-false = reduce-false-is-false(fuse 🝖 constant)


text:
{-# OPTIONS --cubical #-}
module Cubical.Foundations.Equiv.Fiberwise where

open import Cubical.Core.Everything

open import Cubical.Foundations.Everything

module _ {a p q} {A : Type a} (P : A → Type p) (Q : A → Type q)
         (f : ∀ x → P x → Q x)
         where
  private
    total : (Σ A P) → (Σ A Q)
    total = (\ p → p .fst , f (p .fst) (p .snd))

  -- Thm 4.7.6
  fibers-total : ∀ {xv} → Iso (fiber total (xv)) (fiber (f (xv .fst)) (xv .snd))
  fibers-total {xv} = iso h g h-g g-h
   where
    h : ∀ {xv} → fiber total xv → fiber (f (xv .fst)) (xv .snd)
    h {xv} (p , eq) = J (\ xv eq → fiber (f (xv .fst)) (xv .snd)) ((p .snd) , refl) eq
    g : ∀ {xv} → fiber (f (xv .fst)) (xv .snd) → fiber total xv
    g {xv} (p , eq) = (xv .fst , p) , (\ i → _ , eq i)
    h-g : ∀ {xv} y → h {xv} (g {xv} y) ≡ y
    h-g {x , v} (p , eq) = J (λ _ eq₁ → h (g (p , eq₁)) ≡ (p , eq₁)) (JRefl (λ xv₁ eq₁ → fiber (f (xv₁ .fst)) (xv₁ .snd)) ((p , refl))) (eq)
    g-h : ∀ {xv} y → g {xv} (h {xv} y) ≡ y
    g-h {xv} ((a , p) , eq) = J (λ _ eq₁ → g (h ((a , p) , eq₁)) ≡ ((a , p) , eq₁))
                                (cong g (JRefl (λ xv₁ eq₁ → fiber (f (xv₁ .fst)) (xv₁ .snd)) (p , refl)))
                                eq
  -- half of Thm 4.7.7 (fiberwise equivalences)
  fiberEquiv : ([tf] : isEquiv total)
               → ∀ x → isEquiv (f x)
  fiberEquiv [tf] x .equiv-proof y = retractIsContr (fibers-total .Iso.inv) (fibers-total .Iso.fun) (fibers-total .Iso.rightInv)
                                                    ([tf] .equiv-proof (x , y))

module _ {ℓ : Level} {U : Type ℓ} {ℓr} (_~_ : U → U → Type ℓr)
         (idTo~ : ∀ {A B} → A ≡ B → A ~ B)
         (c : ∀ A → isContr (Σ U \ X → A ~ X))
       where

  isContrToUniv : ∀ {A B} → isEquiv (idTo~ {A} {B})
  isContrToUniv {A} {B}
    = fiberEquiv (λ z → A ≡ z) (λ z → A ~ z) (\ B → idTo~ {A} {B})
                 (λ { .equiv-proof y
                    → isContrSigma ((_ , refl) , (\ z → contrSingl (z .snd)))
                                   \ a → isContrPath (c A) _ _
                    })
                 B

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

open import HoTT

{- Useful lemmas for computing the effect of transporting a function
 - across an equivalence in the domain or codomain -}

module cohomology.FunctionOver where

{- transporting a function along an equivalcence or path in the domain -}
module _ {i} {j} {B : Type i} {C : Type j} (g : B → C) where

  domain-over-path : {A : Type i} (p : A == B)
    → g ∘ coe p == g [ (λ D → (D → C)) ↓ p ]
  domain-over-path idp = idp

  domain-over-equiv : {A : Type i} (e : A ≃ B)
    → g ∘ –> e == g [ (λ D → (D → C)) ↓ ua e ]
  domain-over-equiv e = ↓-app→cst-in $ λ q → ap g (↓-idf-ua-out e q)

module _ {i} {j} {A : Type i} {C : Type j} (f : A → C) where

  domain!-over-path : {B : Type i} (p : A == B)
    → f == f ∘ coe! p [ (λ D → (D → C)) ↓ p ]
  domain!-over-path idp = idp

  domain!-over-equiv : {B : Type i} (e : A ≃ B)
    → f == f ∘ <– e [ (λ D → (D → C)) ↓ ua e ]
  domain!-over-equiv e = ↓-app→cst-in $
    λ q → ap f (! (<–-inv-l e _) ∙ ap (<– e) (↓-idf-ua-out e q))

{- transporting a ptd function along a equivalence or path in the domain -}
module _ {i} {j} {Y : Ptd i} {Z : Ptd j} (g : fst (Y ⊙→ Z)) where

  domain-over-⊙path : {X : Ptd i} (p : fst X == fst Y)
    (q : coe p (snd X) == snd Y)
    → g ⊙∘ (coe p , q) == g [ (λ W → fst (W ⊙→ Z)) ↓ pair= p (↓-idf-in p q) ]
  domain-over-⊙path idp idp = idp

  domain-over-⊙equiv : {X : Ptd i} (e : fst X ≃ fst Y)
    (q : –> e (snd X) == snd Y)
    → g ⊙∘ ⊙–> e q == g [ (λ W → fst (W ⊙→ Z)) ↓ ⊙ua e q ]
  domain-over-⊙equiv {X = X} e q =
    ap (λ w → g ⊙∘ w) lemma ◃ domain-over-⊙path (ua e) (coe-β e (snd X) ∙ q)
    where
    lemma : Path {A = fst (X ⊙→ Y)}
       (⊙–> e q) (coe (ua e) , coe-β e (snd X) ∙ q)
    lemma = ! $ ⊙λ= (coe-β e) idp

module _ {i} {j} {X : Ptd i} {Z : Ptd j} (f : fst (X ⊙→ Z)) where

  domain!-over-⊙path : {Y : Ptd i} (p : fst X == fst Y)
    (q : coe p (snd X) == snd Y)
    → f == f ⊙∘ (coe! p , ap (coe! p) (! q) ∙ coe!-inv-l p (snd X))
      [ (λ W → fst (W ⊙→ Z)) ↓ pair= p (↓-idf-in p q) ]
  domain!-over-⊙path idp idp = idp

  domain!-over-⊙equiv : {Y : Ptd i} (e : fst X ≃ fst Y)
    (q : –> e (snd X) == snd Y)
    → f == f ⊙∘ (⊙<– e q) [ (λ W → fst (W ⊙→ Z)) ↓ ⊙ua e q ]
  domain!-over-⊙equiv {Y = Y} e q =
    (ap (λ w → f ⊙∘ w) (lemma e q) ∙ ! (⊙∘-assoc f _ (–> e , q))) ◃
    domain-over-⊙equiv
      (f ⊙∘ (<– e , ap (<– e) (! q) ∙ <–-inv-l e (snd X))) e q
    where
    lemma : {X Y : Ptd i}
      (e : fst X ≃ fst Y) (q : –> e (snd X) == snd Y)
      → ⊙idf X == ((<– e , ap (<– e) (! q) ∙ <–-inv-l e (snd X)) ⊙∘ (–> e , q))
    lemma {X = X} e idp = ! $ ⊙λ= (<–-inv-l e) (! (∙-unit-r _))

{- transporting a function along an equivalence or path in the codomain -}
module _ {i} {j} {A : Type i} {B : Type j} (f : A → B) where

  codomain-over-path : {C : Type j} (p : B == C)
    → f == coe p ∘ f [ (λ D → (A → D)) ↓ p ]
  codomain-over-path idp = idp

  codomain-over-equiv : {C : Type j} (e : B ≃ C)
    → f == –> e ∘ f [ (λ D → (A → D)) ↓ ua e ]
  codomain-over-equiv e = ↓-cst→app-in $ λ _ → ↓-idf-ua-in e idp

module _ {i} {j} {A : Type i} {C : Type j} (g : A → C) where

  codomain!-over-path : {B : Type j} (p : B == C)
    → coe! p ∘ g == g [ (λ D → (A → D)) ↓ p ]
  codomain!-over-path idp = idp

  codomain!-over-equiv : {B : Type j} (e : B ≃ C)
    → <– e ∘ g == g [ (λ D → (A → D)) ↓ ua e ]
  codomain!-over-equiv e = ↓-cst→app-in $ λ _ → ↓-idf-ua-in e (<–-inv-r e _)

{- transporting a ptd function along a equivalence or path in the codomain -}
module _ {i} {j} {X : Ptd i} {Y : Ptd j} (f : fst (X ⊙→ Y)) where

  codomain-over-⊙path : {Z : Ptd j} (p : fst Y == fst Z)
    (q : coe p (snd Y) == snd Z)
    → f == (coe p , q) ⊙∘ f [ (λ W → fst (X ⊙→ W)) ↓ pair= p (↓-idf-in p q) ]
  codomain-over-⊙path idp idp = pair= idp (! (∙-unit-r _ ∙ ap-idf (snd f)))

  codomain-over-⊙equiv : {Z : Ptd j} (e : fst Y ≃ fst Z)
    (q : –> e (snd Y) == snd Z)
    → f == (–> e , q) ⊙∘ f [ (λ W → fst (X ⊙→ W)) ↓ ⊙ua e q ]
  codomain-over-⊙equiv {Z = Z} e q =
    codomain-over-⊙path (ua e) (coe-β e (snd Y) ∙ q) ▹ ap (λ w → w ⊙∘ f) lemma
    where
    lemma : Path {A = fst (Y ⊙→ Z)}
      (coe (ua e) , coe-β e (snd Y) ∙ q) (–> e , q)
    lemma = ⊙λ= (coe-β e) idp

module _ {i} {j} {X : Ptd i} {Z : Ptd j} (g : fst (X ⊙→ Z)) where

  codomain!-over-⊙path : {Y : Ptd j} (p : fst Y == fst Z)
    (q : coe p (snd Y) == snd Z)
    → (coe! p , ap (coe! p) (! q) ∙ coe!-inv-l p (snd Y)) ⊙∘ g == g
      [ (λ W → fst (X ⊙→ W)) ↓ pair= p (↓-idf-in p q) ]
  codomain!-over-⊙path idp idp = pair= idp (∙-unit-r _ ∙ ap-idf (snd g))

  codomain!-over-⊙equiv : {Y : Ptd j} (e : fst Y ≃ fst Z)
    (q : –> e (snd Y) == snd Z)
    → (⊙<– e q) ⊙∘ g == g [ (λ W → fst (X ⊙→ W)) ↓ ⊙ua e q ]
  codomain!-over-⊙equiv {Y = Y} e q =
    codomain-over-⊙equiv
      ((<– e , ap (<– e) (! q) ∙ <–-inv-l e (snd Y)) ⊙∘ g) e q
    ▹ (! (⊙∘-assoc (–> e , q) _ g) ∙ ap (λ w → w ⊙∘ g) (lemma e q)
       ∙ ⊙∘-unit-l g)
    where
    lemma : {Y Z : Ptd j}
      (e : fst Y ≃ fst Z) (q : –> e (snd Y) == snd Z)
      → ((–> e , q) ⊙∘ (<– e , ap (<– e) (! q) ∙ <–-inv-l e (snd Y))) == ⊙idf Z
    lemma {Y = Y} e idp =
      ⊙λ= (<–-inv-r e) (ap (λ w → w ∙ idp) (<–-inv-adj e (snd Y)))

{- transporting a group homomorphism along an isomorphism -}

domain-over-iso : ∀ {i j} {G H : Group i} {K : Group j}
  (φ : G →ᴳ H) (ie : is-equiv (GroupHom.f φ)) (ψ : G →ᴳ K) (χ : H →ᴳ K)
  → GroupHom.f ψ == GroupHom.f χ
    [ (λ A → A → Group.El K) ↓ ua (GroupHom.f φ , ie) ]
  → ψ == χ [ (λ J → J →ᴳ K) ↓ group-ua (φ , ie) ]
domain-over-iso {K = K} φ ie ψ χ p = hom=-↓ _ _ $ ↓-ap-out _ Group.El _ $
  transport
    (λ q → GroupHom.f ψ == GroupHom.f χ [ (λ A → A → Group.El K) ↓ q ])
    (! (group-ua-el (φ , ie)))
    p

codomain-over-iso : ∀ {i j} {G : Group i} {H K : Group j}
  (φ : H →ᴳ K) (ie : is-equiv (GroupHom.f φ)) (ψ : G →ᴳ H) (χ : G →ᴳ K)
  → GroupHom.f ψ == GroupHom.f χ
    [ (λ A → Group.El G → A) ↓ ua (GroupHom.f φ , ie) ]
  → ψ == χ [ (λ J → G →ᴳ J) ↓ group-ua (φ , ie) ]
codomain-over-iso {G = G} φ ie ψ χ p = hom=-↓ _ _ $ ↓-ap-out _ Group.El _ $
  transport
    (λ q → GroupHom.f ψ == GroupHom.f χ [ (λ A → Group.El G → A) ↓ q ])
    (! (group-ua-el (φ , ie)))
    p

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
module Issue396b where

import Common.Irrelevance

data A : Set where

-- just an irrelevant field
record PrfA : Set where
  field
    .f : A

Foo : Set -> Set1
Foo R = (P : R → Set) → ((x : R) → P x → P x) →
                        (x y : R) → P x → P y
foo : Foo PrfA
foo P hyp x y = hyp x
-- Error was:
-- x != y of type ⊤
-- when checking that the expression hyp x has type P x → P y

record Top : Set where

-- only singleton components
record R : Set where
  field
    p1 : PrfA
    .p2 : A
    p3 : Top

bla : Foo R
bla P hyp x y = hyp x

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Maybe-related properties
------------------------------------------------------------------------

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

module Data.Maybe.Properties where

open import Algebra
import Algebra.Structures as Structures
import Algebra.FunctionProperties as FunctionProperties
open import Data.Maybe.Base
open import Data.Maybe.Relation.Unary.All using (All; just; nothing)
open import Data.Product using (_,_)
open import Function
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no)

------------------------------------------------------------------------
-- Equality

module _ {a} {A : Set a} where

  just-injective : ∀ {x y} → (Maybe A ∋ just x) ≡ just y → x ≡ y
  just-injective refl = refl

  ≡-dec : Decidable _≡_ → Decidable {A = Maybe A} _≡_
  ≡-dec _≟_ nothing  nothing  = yes refl
  ≡-dec _≟_ (just x) nothing  = no λ()
  ≡-dec _≟_ nothing  (just y) = no λ()
  ≡-dec _≟_ (just x) (just y) with x ≟ y
  ... | yes refl = yes refl
  ... | no  x≢y  = no (x≢y ∘ just-injective)

------------------------------------------------------------------------
-- map

  map-id : map id ≗ id {A = Maybe A}
  map-id (just x) = refl
  map-id nothing  = refl

  map-id₂ : ∀ {f : A → A} {mx} → All (λ x → f x ≡ x) mx → map f mx ≡ mx
  map-id₂ (just eq) = cong just eq
  map-id₂ nothing   = refl

module _ {a b} {A : Set a} {B : Set b} where

  map-<∣>-commute : ∀ (f : A → B) mx my →
    map f (mx <∣> my) ≡ map f mx <∣> map f my
  map-<∣>-commute f (just x) my = refl
  map-<∣>-commute f nothing  my = refl

  map-cong : {f g : A → B} → f ≗ g → map f ≗ map g
  map-cong f≗g (just x) = cong just (f≗g x)
  map-cong f≗g nothing  = refl

  map-cong₂ : ∀ {f g : A → B} {mx} →
    All (λ x → f x ≡ g x) mx → map f mx ≡ map g mx
  map-cong₂ (just eq) = cong just eq
  map-cong₂ nothing   = refl

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

  map-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
  map-compose (just x) = refl
  map-compose nothing  = refl

------------------------------------------------------------------------
-- maybe

module _ {a b} {A : Set a} {B : Set b} where

  maybe-map : ∀ {c} {C : Maybe B → Set c}
              (j : (x : B) → C (just x)) (n : C nothing) (f : A → B) ma →
              maybe {B = C} j n (map f ma) ≡ maybe {B = C ∘ map f} (j ∘ f) n ma
  maybe-map j n f (just x) = refl
  maybe-map j n f nothing  = refl

  maybe′-map : ∀ {c} {C : Set c} j (n : C) (f : A → B) ma →
               maybe′ j n (map f ma) ≡ maybe′ (j ∘′ f) n ma
  maybe′-map = maybe-map

------------------------------------------------------------------------
-- _<∣>_

module _ {a} {A : Set a} where

  open FunctionProperties {A = Maybe A} _≡_

  <∣>-assoc : Associative _<∣>_
  <∣>-assoc (just x) y z = refl
  <∣>-assoc nothing  y z = refl

  <∣>-identityˡ : LeftIdentity nothing _<∣>_
  <∣>-identityˡ (just x) = refl
  <∣>-identityˡ nothing  = refl

  <∣>-identityʳ : RightIdentity nothing _<∣>_
  <∣>-identityʳ (just x) = refl
  <∣>-identityʳ nothing  = refl

  <∣>-identity : Identity nothing _<∣>_
  <∣>-identity = <∣>-identityˡ , <∣>-identityʳ

module _ {a} (A : Set a) where

  open Structures {A = Maybe A} _≡_

  <∣>-isMagma : IsMagma _<∣>_
  <∣>-isMagma = record
    { isEquivalence = isEquivalence
    ; ∙-cong        = cong₂ _<∣>_
    }

  <∣>-isSemigroup : IsSemigroup _<∣>_
  <∣>-isSemigroup = record
    { isMagma = <∣>-isMagma
    ; assoc   = <∣>-assoc
    }

  <∣>-isMonoid : IsMonoid _<∣>_ nothing
  <∣>-isMonoid = record
    { isSemigroup = <∣>-isSemigroup
    ; identity    = <∣>-identity
    }

  <∣>-semigroup : Semigroup a a
  <∣>-semigroup = record
    { isSemigroup = <∣>-isSemigroup
    }

  <∣>-monoid : Monoid a a
  <∣>-monoid = record
    { isMonoid = <∣>-isMonoid
    }


text:
-- 2014-05-26 Andrea & Andreas, AIM XIX
-- Too eager pruning

module succeed.Issue1147 where

open import Common.Equality
open import Common.Product
open import Common.Prelude

postulate
  A : Set

if_then_else1_ : ∀ {A : Set1} → Bool → A → A → A
if true  then t else1 f = t
if false then t else1 f = f

test1 : let H : Set; H = _; M : Bool -> Set → Set; M = _ in {z : Set} → H ≡ (M true z) × M ≡ (\ b z → if b then A else1 z)
test1 = refl , refl

test2 : let H : Set; H = _; M : (Bool -> Bool) -> Set → Set; M = _ in {z : Set} → H ≡ (M (\ _ -> true) z) × M ≡ (\ b z → if b true then A else1 z)
test2 = refl , refl

test3 : let H : Set; H = _; M : (Bool × Bool) -> Set → Set; M = _ in {z : Set} {b : Bool} → H ≡ (M (true , b) z) × M ≡ (\ b z → if proj₁ b then A else1 z)
test3 = refl , refl

-- Also for defined functions

fun : Bool → Bool
fun true  = true
fun false = false

works4 : let H : Set; H = _; M : (Bool -> Bool) -> Set → Set; M = _ in {z : Set} → M ≡ (\ b z → if b true then A else1 z) × H ≡ (M fun z)
works4 = refl , refl

test4 : let H : Set; H = _; M : (Bool -> Bool) -> Set → Set; M = _ in {z : Set} → H ≡ (M fun z) × M ≡ (\ b z → if b true then A else1 z)
test4 = refl , refl

max_stars_repo_name: larrytheliquid/agda


text:
------------------------------------------------------------------------------
-- Well-founded relation on lists
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.FOTC.Data.List.WellFoundedRelationsSL {A : Set} where

open import Data.Product
open import Data.List hiding ( length )
open import Data.Nat

open import Induction.Nat
open import Induction.WellFounded

open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------------
-- We use our own version of the function length because we have
-- better reductions.
length : List A → ℕ
length []       = 0
length (x ∷ xs) = 1 + length xs

open module II = Induction.WellFounded.Inverse-image {_<_ = _<′_} length

-- Well-founded relation on lists based on their length.
LTL : List A → List A → Set
LTL xs ys = length xs <′ length ys

-- The relation LTL is well-founded (using the image inverse
-- combinator).
wfLTL : Well-founded LTL
wfLTL = II.well-founded <′-well-founded

-- Well-founded relation on lists based on their structure.
LTC : List A → List A → Set
LTC xs ys = Σ A (λ a → ys ≡ a ∷ xs)

LTC→LTL : ∀ {xs ys} → LTC xs ys → LTL xs ys
LTC→LTL (x , refl) = ≤′-refl

open module S = Induction.WellFounded.Subrelation {_<₁_ = LTC} LTC→LTL

-- The relation LTC is well-founded (using the subrelation combinator).
wfLTC : Well-founded LTC
wfLTC = S.well-founded wfLTL

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Issue486 where

record ⊤ : Set where
  constructor tt

record Pub (A : Set) : Set where
  field
    fi : A

abstract
  abs : ⊤
  abs = fi
    where open Pub record {fi = tt}